プログラム的な両刀論法の証明 by ddt³さん

プログラム的な両刀論法の証明 by ddt³さん

 

 

ddt³さんからコンピュータのプラグラム的解答をいただいたので、それを紹介します。

昔の最も単純なコンピュータのCPUは論理記号の「かつ（and)」、「または（or)」、「ない（not）」などの論理回路から構成されていたことから明らかなように、コンピュータと論理（計算）の間には切っても切れない深い関係がある。０（False）と１（True）の２進数を使うコンピュータの計算原理は、論理（計算）そのものだにゃ。

だから、ddt³さんのようなこうした回答があっても然るべきだと思う。

 

論理回路

https://goo.gl/4U6MQM

 

論理回路を実際に組み立て、電流を流すことによって、これを証明することだってできる。
マリオメーカー（って何だ(・・?）を使って証明することだってできるかもしれない(^^ゞ

 

 

---

 

＞

たとえば、これは次のような命題である。

　「ネムネコに遭遇すると、お前らはネコパンチをくらう」

　「ブラゲロ・マムシに遭遇すると、お前らは毒を吐かれる」

　「ネムネコに遭遇するか、プラゲロ・マムシに遭遇するかである」

ゆえに、

　「お前らはネコパンチを食らうか、毒を吐かれる」

＞

 

　じつはこれ、構文論的証明なんですよね(^^)。ここでの原始命題ａ，ｂ，ｃ，・・・は、ａ⇒ｂ：「ネムネコに遭遇すると、お前らはネコパンチをくらう」などですが、構文論で重要なのは個々の「原始命題の意味」ではなく、「論理の流れの意味」です。ただしこれは実際上の話で、理屈の上では構文論的証明は「意味」に関わる事無く機械的に行えます。以下で、 _ は継続行マーク， [・・・]はコメント行を表します。

 

(Main開始)

((ａ⇒ｂ)∧(ｃ⇒ｄ)∧(ａ∨ｃ))⇒(ｂ∨ｄ)を示す。

(ａ⇒ｂ)∧(ｃ⇒ｄ)∧(ａ∨ｃ)を仮定する。

 

　(ｓｕｂ-1呼び出し，ｓｕｂ名：補助仮定の方法)

　(引数：Ａを仮定してＢを導ければ、 _

　　　　 Ａ⇒Ｂは真。)

 

　　[(ａ⇒ｂ)∧(ｃ⇒ｄ)∧(ａ∨ｃ)を仮定した。]

 

　 (ｓｕｂ-2呼び出し，ｓｕｂ名：論理積の分解法則)

　　(引数：Ａ∧Ｂ∧Ｃ∧・・・が真なら、 _

Ａ，Ｂ，Ｃ，・・・は同時に真。）

　　(ｓｕｂ-2復帰)

 

　　(ａ⇒ｂ)，(ｃ⇒ｄ)，(ａ∨ｃ)は同時に真。

 

　　(ｓｕｂ-1呼び出し)ａを仮定する。

　　　[(ａ⇒ｂ)，(ｃ⇒ｄ)，(ａ∨ｃ)は同時に真。]

　　　ａと(ａ⇒ｂ)は同時に真。

 

　　　(ｓｕｂ-4呼び出し，ｓｕｂ名：三段論法)

　　　(引数：ＡとＡ⇒Ｂが同時に真なら、 _

Ｂは真。)

　　　(ｓｕｂ-4復帰)

 

　　　ｂは真。

　　　ｂ⇒(ｂ∨ｄ)は公理（要するに真）。

　　　(ｂ∨ｄ)は真（ｓｕｂ-4を呼び出して復帰）。

　　(ｓｕｂ-1復帰)

 

　　ａ⇒(ｂ∨ｄ)は真。

 

　　(ｓｕｂ-1呼び出し)ｃを仮定する。

　　　[(ａ⇒ｂ)，(ｃ⇒ｄ)，(ａ∨ｃ)は同時に真。]

　　　ｃと(ｃ⇒ｄ)は同時に真。

　　　ｄは真（ｓｕｂ-4を呼び出して復帰）。

　　　ｄ⇒(ｂ∨ｄ)は公理（要するに真）。

　　　(ｂ∨ｄ)は真（ｓｕｂ-4を呼び出して復帰）。

　　(ｓｕｂ-1復帰)

 

　　ｃ⇒(ｂ∨ｄ)は真。

 

　　[ａ⇒(ｂ∨ｄ)とｃ⇒(ｂ∨ｄ)は同時に真。]

 

　　(ｓｕｂ-5呼び出し，ｓｕｂ名：場合分けの方法)

　　(引数：Ａ⇒ＣとＢ⇒Ｃが同時に真なら、 _

(Ａ∨Ｂ)⇒Ｃは真。)

　　(ｓｕｂ-5復帰)

 

　　(ａ∨ｃ)⇒(ｂ∨ｄ)は真。

 

　　[(ａ⇒ｂ)，(ｃ⇒ｄ)，(ａ∨ｃ)は同時に真だった。]

　　(ａ∨ｃ)は真。

 

　　(ｂ∨ｄ)は真（ｓｕｂ-4を呼び出して復帰）。

　(ｓｕｂ-1復帰)

 

　[(ａ⇒ｂ)∧(ｃ⇒ｄ)∧(ａ∨ｃ)を仮定していた。]

　((ａ⇒ｂ)∧(ｃ⇒ｄ)∧(ａ∨ｃ))⇒(ｂ∨ｄ)は真。

(Main終了)

 

　・・・となります(^^;)。

　絶対に構文論的証明が、プログラミングの原型だと思えるんですよね(^^)。

 

（by ddt³さん）