抽象化の技法

第一回　4月14日　いろいろな帰納法　情報系の数学入門　2章　
　　　　　　　　　数学的帰納法の復習、累積帰納法　　構造帰納法 2.6[1]　

第二回 4月21日 重みをつけた帰納法2.6[5]、計算帰納法2.6[6]、 述語 （第３章 3.6[1]）

第三回 4月28日 述語論理の式、文章の記号化、出現、有効範囲、束縛、自由 （3.6[2], [3], [4]）

レポート！

課題 １ 任意の（命題論理の）論理式 A について、"not"と"and"だけから作られる
論理式 B で恒に v(A)=v(B) となるものがあることを示せ。
（論理式の構成に関する構造帰納法を適用する。A の構成における
最後の論理結合子についての場合わけによる。 情報系の数学入門・第２章、2.6[1] 82ページ参照）
課題　２ 「皆が何か動物を好きなわけではない」を、述語論理の記号で表せ。
（述語記号は自分で適当に設定してよい。）
課題　３　(exists x)(forall y)leq(x,y)
（ただし、leq(x,y)は"x は y 以下である"を表す。）
　　　 この論理式が正しい数学の集合と正しくない集合をそれぞれ与えよ。
　　　正しくないほうは、反例をあげよ。
課題　４　命題論理の体系Pの公理（Ax7）(A=>B)=>((A=>notB)=>notA) が恒真である
ことを示せ。（情報系の数学入門・第３章 3.4[1]）

４年生以上で、就職活動で出席困難な人は、申し出てください。（具体的に
欠席理由を求めます。）
以上

何をどう示すのか？（かっこの中のコメントの解説）
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
答え 構造帰納法を使うのは、Aの構造にしたがって、Bを定義
（構成）できることを示すことです。Aが変数の場合はそのまま、
Aが論理記号を使って作られている場合は、その論理記号と帰納法の
仮定からnotとandに書き換えられることを示します。
そのように書き換えても真理値が変わらないことは、テキ
ストや 講義にあった命題を使っていいのです。いちいち真理値の計算
を する必要はありません。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

論理式 A と B の X と Y は、命題変数を変えたほうがいいので しょうか？
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
答え いいえ、命題変数は同じにしてください。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

「A の構成における最後の論理結合子についての場合わけに よる。」とはどういう事なのか。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
答え 最初の質問の答えでも触れましたが、たとえばAが F and G の形
ならば、FとG に関する帰納法の仮定を使えばそのままですね。
もしAが F or G ならば、or はBの中に現れては困るので、and とnotで
書き換えなければなりません。
このように論理結合子によって扱いがちがう、ということです。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

＊休講、補講のお知らせ
休講：6月9日 一回あいた分、レポートの勉強しておいてくださいね。
補講：7月10日（土）3時間目 ５１２教室
不便な時間でごめんなさい。皆さんの都合のよい時間はこれくらいなのです。
なるべく質問と演習の時間にします。質問をもってきてください。

良く理解している人もいましたが、全体として、論理式という一番
基本的なことが理解できていなかった。解答を
ここ におきますから、よく読んで理解してください。
レポートや試験は、成績をつける目的だけではありません。その勉強をする
ことによって、理解を深めまた理解できていないことは何か、を自覚できる
ように、という目的もあります。そこで理解を深めるために、次の方針をとります。

＊＊後期のレポート（１月初めに提出、詳細は後で）では前期の内容も含めて、
総合報告を書いてもらいます。（ほかに技術的な問題もだします。）そのために
４０点満点ではなく６０点満点にして、前期との調節をします。（後期の期末試験は
予定通り６０点）総合点が満点を越える人は満点で打ちきります。
なお、LaTexで証明図を書くには次のファイルを自分のところにコピーすればできます。
/NF/local/Solaris2J/lib/tex/macros/proof.sty
とても便利なマクロです。

１　述語論理の体系 NK および NJ について論述せよ。（A4約３枚）

２　自然数論 PA について論述せよ。（A4約１枚）

注 （以上１と２について、書き方は自由です。主張したいことが読者に伝わるように書いてください。
提出する前に友人などに読んでもらうことを勧めます。

３ 〔1〕論理式 (A==>(B==>A and B)) の(NJにおける）証明 Q を作成せよ。
　 〔2〕証明 Q にCurry-Howard 対応する F_0 のプログラム e を書け。
〔3〕P が論理式 A の証明のとき、Q と P を使って B==>(A and B) の証明 R を書け。
〔4〕R に対応するプログラム p を書け。

４　次の論理式の証明を、分解の木を参考にして、作成せよ：
(*) (forall)xP(x) or (exists)y(notP(y))

＊注： レポートは前回と同じくLaTexで書いてください。ただし証明の作成は
手書きでもいいです。前にお知らせしたproof.styを使うときれいに書けます。 興味があったら試してみてください。

２はかんたんなスキーマを書くこと。
例　　「二つの入力値の最初の要素を取り出す写像の定義を書け」：
　　project1(x,y)=xとなる写像projectの定義。任意の集合XとYからXへの 写像の型をもつ。

３は、一年間の講義の中で、あなたが得意とする事柄について、数行で書く。
内容は何でもいいですが、読む人が理解しやすくて納得するように書いてください。
あらかじめ書いてみて、覚えてきてください。

試験終了後に１と２の解答を載せます。

では
I enjoyed having you in my class and Good Luck on the finals!