「Ｅ.Ｊ.レモンの方法（命題論理の自然演繹法）」について。

（01）
演習9.4 以下の命題論理式について、トートロジーならばその証明図を示し、トートロジーでないならば、反例を与えよ。
（１）Ｐ→Ｐ→Ｑ
（２）（～Ｐ→Ｑ）→Ｐ∨Ｑ
（2019年度、数理論理学、講義資料９、青戸等人、知能情報システムプログラム）
（02）
（１）Ｐ→Ｐ→Ｑ
であるならば、
（ａ）（Ｐ→Ｐ）→Ｑ
（ｂ）　Ｐ→（Ｐ→Ｑ）
のいづれかである。
然るに、
（03）
Ｐ＝１
Ｑ＝０
であるならば、
（ａ）（１→１）→０
（ｂ）　１→（１→０）
は、両方とも、「０（偽）」である。
従って、
（01）（02）（03）により、
（04）
（１）Ｐ→Ｐ→Ｑ
は、トートロジーではない。
然るに、
（05）
（ⅱ）
１　　　　（１）　　　～Ｐ→　Ｑ　　　Ａ
　２　　　（２）　　　～Ｐ＆～Ｑ　　　Ａ
　２　　　（３）　　　～Ｐ　　　　　　２＆Ｅ
１２　　　（４）　　　　　　　Ｑ　　　２３ＭＰＰ
　２　　　（５）　　　　　　～Ｑ　　　２＆Ｅ
１２　　　（６）　　　　Ｑ＆～Ｑ　　　４５＆Ｉ
１　　　　（７）　～（～Ｐ＆～Ｑ）　　２６ＲＡＡ
　　８　　（８）　～（　Ｐ∨　Ｑ）　　Ａ
　　　９　（９）　　　　Ｐ　　　　　　Ａ
　　　９　（ア）　　　　Ｐ∨　Ｑ　　　９∨Ｉ
　　８９　（イ）　～（　Ｐ∨　Ｑ）＆　
　　　　　　　　　　（　Ｐ∨　Ｑ）　　８ア＆Ｉ
　　８　　（ウ）　　　～Ｐ　　　　　　９イＲＡＡ
　　　　エ（エ）　　　　　　　Ｑ　　　Ａ
　　　　エ（オ）　　　　Ｐ∨　Ｑ　　　エ∨Ｉ
　　８　エ（カ）　～（　Ｐ∨　Ｑ）＆
　　　　　　　　　　（　Ｐ∨　Ｑ）　　８オ＆Ｉ
　　８　　（キ）　　　　　～　Ｑ　　　エカＲＡＡ
　　８　　（ク）　　　～Ｐ＆～Ｑ　　　ウキ＆Ｉ
１　８　　（ケ）　～（～Ｐ＆～Ｑ）＆
　　　　　　　　　　（～Ｐ＆～Ｑ）　　７ク＆Ｉ
１　　　　（コ）～～（　Ｐ∨　Ｑ）　　８ケＲＡＡ
１　　　　（サ）　　　　Ｐ∨　Ｑ　　　コＤＮ
従って、
（01）（05）により、
（06）
（２）（～Ｐ→Ｑ）→Ｐ∨Ｑ
は、トートロジーである。
従って、
（01）（04）（06）により、
（07）
演習9.4 以下の命題論理式について、トートロジーならばその証明図を示し、トートロジーでないならば、反例を与えよ。
（１）Ｐ→Ｐ→Ｑ
（２）（～Ｐ→Ｑ）→Ｐ∨Ｑ
答え9.4
（１）はトートロジー　ではない。
（２）はトートロジー　である。
然るに、
（08）

然るに、
（08）により、
（09）
（解答）（２）の「証明図」は、「私はまだ学んでゐない（未之学也）」ため、「私には読めない。」
然るに、
（10）
証明の各行の左側に、仮定の数字を挙げる方法は、伝統的な方法にくらべて遥かに明瞭であるとわたしには思われる。
The device of listing assumptions by number on the left of each line seems to me much clearer than more traditional approaches.
（E.j.レモン 著、竹尾治一郎・楢英 訳、1973年、序ⅲと、原文）
然るに、
（11）
１　　　　（１）　　　～Ｐ→　Ｑ　　　Ａ
　２　　　（２）　　　～Ｐ＆～Ｑ　　　Ａ
　２　　　（３）　　　～Ｐ　　　　　　２＆Ｅ
１２　　　（４）　　　　　　　Ｑ　　　２３ＭＰＰ
　２　　　（５）　　　　　　～Ｑ　　　２＆Ｅ
１２　　　（６）　　　　Ｑ＆～Ｑ　　　４５＆Ｉ
１　　　　（７）　～（～Ｐ＆～Ｑ）　　２６ＲＡＡ
が「意味する所」は、
１ 　で、　「ＰでないならばＱである。」と仮定し、
　２ で　　「Ｐでなくて、Ｑでもない。」と仮定したところ。
１２ が　　「矛盾（Ｑ＆～Ｑ）」を「証明」したため、
　２ が、　「否定」されて、２が、「左側（仮定のプール）」から除かれて、残ってゐる、
１ により、「Ｐでなくて、Ｑでもない。」といふことはない。といふ「結論」を得た。
といふ「意味」であって、「かうした記述」は、「私にとっても、極めて、明瞭である。」
加へて、
（12）
１　　　　（１）　　　～Ｐ→　Ｑ　　　Ａ
　２　　　（２）　　　～Ｐ＆～Ｑ　　　Ａ
　２　　　（３）　　　～Ｐ　　　　　　２＆Ｅ
１２　　　（４）　　　　　　　Ｑ　　　２３ＭＰＰ
　２　　　（５）　　　　　　～Ｑ　　　２＆Ｅ
１２　　　（６）　　　　Ｑ＆～Ｑ　　　４５＆Ｉ
１　　　　（７）　～（～Ｐ＆～Ｑ）　　２６ＲＡＡ
　　８　　（８）　～（　Ｐ∨　Ｑ）　　Ａ
　　　９　（９）　　　　Ｐ　　　　　　Ａ
　　　９　（ア）　　　　Ｐ∨　Ｑ　　　９∨Ｉ
　　８９　（イ）　～（　Ｐ∨　Ｑ）＆　
　　　　　　　　　　（　Ｐ∨　Ｑ）　　８ア＆Ｉ
　　８　　（ウ）　　　～Ｐ　　　　　　９イＲＡＡ
　　　　エ（エ）　　　　　　　Ｑ　　　Ａ
　　　　エ（オ）　　　　Ｐ∨　Ｑ　　　エ∨Ｉ
　　８　エ（カ）　～（　Ｐ∨　Ｑ）＆
　　　　　　　　　　（　Ｐ∨　Ｑ）　　８オ＆Ｉ
　　８　　（キ）　　　　　～　Ｑ　　　エカＲＡＡ
　　８　　（ク）　　　～Ｐ＆～Ｑ　　　ウキ＆Ｉ
１　８　　（ケ）　～（～Ｐ＆～Ｑ）＆
　　　　　　　　　　（～Ｐ＆～Ｑ）　　７ク＆Ｉ
１　　　　（コ）～～（　Ｐ∨　Ｑ）　　８ケＲＡＡ
１　　　　（サ）　　　　Ｐ∨　Ｑ　　　コＤＮ
といふ「計算」は、現にさうしてゐるやうに、「メモ帳（Windowsに付属）」で書けるものの、

といふ「計算」は、「Ｗｏｒｄ（マイクロソフト）」でも（、少なくとも私には）書けない。
従って、
（12）により、
（13）
「証明の各行の左側に、仮定の数字を挙げる方法（The device of listing assumptions by number on the left of each line）」は、
「Windows PC があれば、誰にでも、それを練習し、その結果を、ＰＣのストレージに、保存することが出来る」。
従って、
（10）～（13）により、
（14）
「証明の各行の左側に、仮定の数字を挙げる方法は、伝統的な方法（ゲンツェンの方法）にくらべて遥かに明瞭であるとわたしにも思われる」し、その上、
「Windows PC があれば、誰にでも、好きなだけそれを練習し、その結果を、ＰＣのストレージに、保存することが出来る」が故に、
「証明の各行の左側に、仮定の数字を挙げる方法」は、「大変、優れてゐる」と、私自身は思ってゐる。
令和０２年０５月１０日、毛利太。