bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

Conceptual Mathematics 最後の問題

一番最後の問題(Session33 Exercise 4、not not not A = not A を示す)は時間切れだったけど、帰りの電車の中で解けたので、忘れないうちに書いときます。

  1. A ⊆ not not A は既に示されている。
  2. 1 の A に not A を代入して、not A ⊆ not not not A
  3. 1 の A に not not A を代入して、not not A ⊆ not not not not A
  4. 1, 3 より A ⊆ not not not not A
  5. 4 と modus ponens より A ∧ not not not A ⊆ false
  6. 5 と modus ponens より not not not A ⊆ not A
  7. 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 (⇒) の定義と等価。)

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。