![[PukiWiki]](image/pukiwiki.png "[PukiWiki]")
t_uda (2010-10-23 (土) 20:51:29)
関連する第 5 章の導入部分と、第 6 章「自然演繹の体系」の 1, 2 節をやった。残りは問 6.1 の演習時間。(5) 以外は解答済み。
→ (5) の証明図: http://twitpic.com/307lub
t_uda (2010-10-28 (木) 00:13:10)
関連する LJ についてサラっと流した後、NJ と LJ の証明可能性同値の証明。Rem. NJ は直観主義論理の体系。
述語論理を含む NJ と、その問題演習をした。問題演習の過程で公理(∀I)と(∃E)を使えば ∃xA⊃∀xA が示せるのではないかと言う疑問が出た。
→ t_uda: 疑問解消。仮定の固有変数条件のため、そのような証明はできない。
t_uda (2010-11-10 (水) 21:25:46)
先週は文化の日で休み。2週間ぶり。
背理法を公理につけくわえた論理体系 NK について。問題演習は、3問未消化: 6.4 (3), 6.5 (1)-(2)
t_uda (2010-11-18 (木) 00:40:44)
NK での論理式の正規化（証明図の簡約）と関連定理について。
4問未消化: 問 6.4 (3), 章末 6.2 (2)-(3)
問 6.2 (2)「∃x∀y(P(x)⊃P(y))」の証明図
t_uda (2010-12-04 (土) 03:17:40)
λ計算の初歩の辺り。主に定義の確認。ちゃんと準備されていたので良い感じに進んだ。
後は関連する演習問題（今回は全て消化）。この手の証明問題は構造的帰納法を使います。
t_uda (2010-12-08 (水) 22:09:34)
私が担当。目標だった型付きλ計算を一気に終わらせた（本の最後まで終わらせた）。
今回は演習問題はやっていない（少ないし）。
次回から、次のテキスト "Proofs and Types" を使って型理論をもっと厳密にやる。
t_uda (2010-12-15 (水) 22:04:41)
2, 3 章を一応終わらせた。「正規＝冠頭標準形」の定理の系についての理解や、説明文の理解（日本語訳）などが不十分だった。
次回は 4 章。
t_uda (2011-01-12 (水) 22:58:48)
第 4 章で使う Church-Rosser の定理の証明をしてもらった（途中まで）。
次回は証明の修正の後、第 4 章に入る。
t_uda (2011-01-20 (木) 21:04:38)
Church-Rosser の定理を証明した。第 4 章は少し入った。
t_uda (2011-02-24 (木) 02:31:25)
第 4 章の 2 節までやった。次回、3 節 と 4 節を終わらせる予定。
