一番最後の問題（Session33 Exercise 4、not not not A ＝ not A を示す）は時間切れだったけど、帰りの電車の中で解けたので、忘れないうちに書いときます。
- A ⊆ not not A は既に示されている。
- 1 の A に not A を代入して、not A ⊆ not not not A
- 1 の A に not not A を代入して、not not A ⊆ not not not not A
- 1, 3 より A ⊆ not not not not A
- 4 と modus ponens より A ∧ not not not A ⊆ false
- 5 と modus ponens より not not not A ⊆ not A
- 2, 6 より not not not A ＝ not A
あ、6で ∧ が可換であることを勝手に使ってます。
あと、not A ＝ A ⇒ false より、modus ponens を適用すれば X ⊆ not A から X ∧ A ⊆ false （あるいはその逆）が得られることに注意。modus ponens の定義はテキストに従ったもので、ここでは curry / uncurry の操作。一般の modus ponens とちょっとイメージは違うかも。（Heyting代数の implication (⇒) の定義と等価。）
