（01）
ヒルベルトの演繹システムは、公理が多く、推論規則が少ないものです。そして、公理も、わけのわからない論理式となっています。例えば、
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
という論理式が公理として設定されています。つまり、この論理式を出発点として演繹を行って良い。ということです。多くの人は、この論理式の意味を飲みこめないでしょう。
（小島寛之、証明と論理に強くなる、2017年、１３６頁）
然るに、
（02）
次に、命題論理の自然演繹の「公理」です。面白いことに「公理」は一つもありません。ここに自然演繹の大きな特徴があります。「出発点とする公理が何もないのに、いったいどうやって演繹するんだ」という疑問が湧いてくるでしょう。
（小島寛之、証明と論理に強くなる、2017年、１４０頁）
（03）
自然演繹には「仮定の解消」（最初に仮定しておいて、あとでなかったことにする）という手続きがあり、それがなかなか理解しづらいことです。自然演繹は「仮定の解消」のおかげで公理なしに演繹システムとなり得ており、その意味で「仮定の解消」は自然演繹の本質だと言っても過言ではありません。
（小島寛之、証明と論理に強くなる、2017年、１４４頁）
然るに、
（04）
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
といふ「ヒルベルトの公理」に対する、「自然演繹」による「証明」は、次のやうになる。
（05）
（５）├ Ｐ→（Ｑ→Ｐ）
１ （１） Ｐ 仮定
１ （２） Ｐ∨～Ｑ １∨導入
３ （３） Ｐ Ａ
３ （４） ～Ｑ∨ Ｐ ３∨導入
５ （５） ～Ｑ Ａ
５ （６） ～Ｑ∨ Ｐ ５∨導入
１ （７） ～Ｑ∨ Ｐ ２３４５６∨除去
８ （８） Ｑ＆～Ｐ 仮定
９ （９） ～Ｑ Ａ
８ （ア） Ｑ ＆除去
８９ （イ） ～Ｑ＆ Ｑ ９ア＆導入
９ （ウ）～（Ｑ＆～Ｐ） ８イ背理法
エ （エ） Ｐ 仮定
８ （オ） ～Ｐ ８＆除去
８エ （カ） Ｐ＆～Ｐ エオ＆導入
エ （キ）～（Ｑ＆～Ｐ） ８カ背理法
１ （ク）～（Ｑ＆～Ｐ） ７９ウエキ∨除去
ケ （ケ） Ｑ 仮定
コ（コ） ～Ｐ 仮定
ケコ（サ） Ｑ＆～Ｐ ケコ＆導入
１ ケコ（シ）～（Ｑ＆～Ｐ）＆
（Ｑ＆～Ｐ） クサ＆導入
１ ケ （ス） ～～Ｐ コシ背理法
１ ケ （セ） Ｐ ス二重否定
１ （ソ） Ｑ→Ｐ ケセ条件法（仮定の解消）
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
然るに、
（06）
① Ｐ├ Ｐ
② Ｐ→ Ｐ
といふ「式」は、それぞれ、
① Ｐだから、Ｐである。
② Ｐならば、Ｐである。
といふ、「意味」である。
ｃｆ.
同一律（law of identity）
然るに、
（07）
① Ｐだから、Ｐである。
② Ｐならば、Ｐである。
に於いて、
① であれば、 Ｐである。が、
② であっても、Ｐである。とは、限らない。
従って、
（06）（07）により、
（08）
① Ｐだから、Ｐである。
② Ｐならば、Ｐである。
に於いて、
① ≠ ② であって、
①＝② ではない。
然るに、
（09）
① Ｐ├ Ｐ
② Ｐ→ Ｐ
に於いて、
① を、
② に、「書き換へ」ることを、「仮定の解消」といふ。
ｃｆ.
１（１）Ｐ 仮定
（２）Ｐ→Ｐ １１条件法
従って、
（10）
① Ｐ├（Ｑ→Ｐ）
② Ｐ→（Ｑ→Ｐ）
に於いて、
① を、
② に、「書き換へ」ることも、「仮定の解消」である。
然るに、
（05）により、
（11）
１ （１）Ｐ 仮定
１ （ソ） Ｑ→Ｐ ケセ条件法（仮定の解消）
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
であるものの、このことは、
① Ｐ├（Ｑ→Ｐ）：Ｐだから（ＱならばＰである。）
② Ｐ→（Ｑ→Ｐ）：Ｐならば（ＱならばＰである。）
に於いて、
① を、
② に、「書き換へ」ることに、相当する。
従って、
（01）（11）により、
（12）
① Ｐ├（Ｑ→Ｐ）：Ｐだから、ＱならばＰである。
といふ「式」の、「仮定を解消」した「結果」が、
② Ｐ→（Ｑ→Ｐ）：Ｐならば、ＱならばＰである。
といふ「ヒルベルトの公理」である。
然るに、
（13）
（ａ）
１ （１） Ｑ→ Ｐ 仮定
２ （２） Ｑ＆～Ｐ 仮定
２ （３） Ｑ ２＆Ｅ
１２ （４） Ｐ １３前件肯定
２ （５） ～Ｐ ２＆除去
１２ （６） Ｐ＆～Ｐ ４５＆導入
１ （７）～（Ｑ＆～Ｐ） ２６背理法
（ｂ）
１ （１）～（Ｑ＆～Ｐ） 仮定
２ （２） Ｑ 仮定
３（３） ～Ｐ 仮定
２３（４） Ｑ＆～Ｐ ２３＆導入
１２３（５）～（Ｑ＆～Ｐ）＆
（Ｑ＆～Ｐ） １４＆導入
１２ （６） ～～Ｐ ３５背理法
１２ （７） Ｐ ６二重否定
１ （８） Ｑ→ Ｐ ２７条件法
従って、
（13）により、
（14）
① ～（Ｑ→～Ｐ）＝ＱならばＰである。
② ～（Ｑ＆～Ｐ）＝ＱであってＰでない。といふことはない。
に於いて、
①＝② である。
然るに、
（15）
② ＱであってＰでない。といふことはない。
といふのであれば、
② Ｑでない。
といふ場合については、何も、言ってゐない。
従って、
（14）（15）により、
（16）
① ＱならばＰである。
といふのであれば、すなはち、
② ＱであってＰでない。といふことはない。
といふのであれば、
② Ｑでない。
といふ場合については、
② Ｐである。
といふことを、「否定」しない。
従って、
（14）（15）（16）により、
（17）
① ＱならばＰである。
といふ場合に、
① Ｑでない。
としても、
① Ｐでない。
といふことには、ならない。
従って、
（12）（17）により、
（18）
① Ｐ├ Ｑ→Ｐ（Ｐだから、ＱならばＰである。）
といふ「式」は、
① Ｐ├ Ｑ→Ｐ（Ｐだから、Ｑであっても、Ｑでなくとも、Ｐである。）
といふ風に、「読むこと」が出来る。
従って、
（01）（18）により、
（19）
② Ｐならば、ＱならばＰである。
といふ、「ヒルベルトの公理」は、
① Ｐだから、Ｑであっても、Ｑでなくとも、Ｐである。
としたら、
② Ｐならば、ＱならばＰである。
といふ「意味」に、解することが出来る。
（20）
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような9つの基本的規則だけを持つ。
１.仮定の規則 "The Rule of Assumption"
２.モーダスポネンス "Modus Ponendo Ponens"
３.二重否定の規則 "The Rule of Double Negation"
４.条件付き証明の規則 "The Rule of Conditional Proof"
５.＆-導入の規則 "The Rule of ＆-introduction"
６.＆-除去の規則 "The Rule of ＆-elimination"
７.∨-導入の規則 "The Rule of ∨-introduction"
８.∨-除去の規則 "The Rule of ∨-elimination"
９.背理法 "Reductio Ad Absurdum"
（ウィキペディア）
然るに、
（21）
ジョン・レモンが開発した体系 L には、
３.否定否定式（ＭＴＴ）
も、含まれてゐるため、実際には、「９つの基本的規則」ではなく、「１０個の基本規則（The 10 primitive rules）」とするのが、正しい。
然るに、
（21）
（ａ）
１ （１） Ｐ→ Ｑ Ａ
２ （２） ～Ｑ Ａ
３（３） Ｐ Ａ
１ ３（４） Ｑ １３ＭＰＰ
１２３（５）～Ｑ＆ Ｑ ２３＆Ｉ
１２ （６）～Ｐ ３５ＲＡＡ
１ （７）～Ｑ→～Ｐ ２６ＣＰ
（ｂ）
１ （１） ～Ｑ→～Ｐ Ａ
２ （２） Ｐ Ａ
３（３） ～Ｑ Ａ
１ ３（４） ～Ｐ １３ＭＰＰ
１２３（５） Ｐ＆～Ｐ ２４＆Ｉ
１２ （６）～～Ｑ ３５ＲＡＡ
１２ （７） Ｑ ６７ＤＮ
１ （８） Ｐ→ Ｑ ２７ＣＰ
（22）
（ａ）
１ （１） Ｐ→ Ｑ Ａ
２ （２） ～Ｑ Ａ
３（３） Ｐ Ａ
１２ （４）～Ｐ １２ＭＴＴ
１２３（５）～Ｐ＆ Ｐ ３４＆Ｉ
１２ （６）～Ｐ ３５ＲＡＡ
１ （７）～Ｑ→～Ｐ ２６ＣＰ
（ｂ）
１ （１） ～Ｑ→～Ｐ Ａ
２ （２） Ｐ Ａ
２ （３） ～～Ｐ ２ＤＮ
４（４） ～Ｑ Ａ
１２ （５）～～Ｑ １３ＭＴＴ
１２ （６） Ｑ ５ＤＮ
１２４（７） Ｑ＆～Ｑ ４６＆Ｉ
１２ （８）～～Ｑ ４７ＲＡＡ
１２ （９） Ｑ ８ＤＮ
１ （ア） Ｐ→ Ｑ ２９ＣＰ
従って、
（21）（22）により、
（23）
ＭＰＰは、ＭＴＴに、「置き換へ」ることが出来、
ＭＴＴは、ＭＰＰに、「置き換へ」ることが出来る。
従って、
（23）により、
（24）
ＭＴＴは原始的規則と解される必要はなく、他の規則から導出される規則としてえられる（E.J.レモン著、竹尾治一郎・浅野楢英 訳、論理学初歩、７８頁）し、ＭＰＰも、さうである。
然るに、
（25）
① 今日は水曜である。
② 今日は水曜であるか、明日は雨でない。
に於いて、
① が「本当（真）」ならば、
② も「本当（真）」である。
然るに、
（26）
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふ「推論」を、「∨-導入の規則」といふ。
然るに、
（27）
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」を、「日常に於いて行ふ」ことは、「普通は、無い」。
然るに、
（05）により、
（28）
（５）├ Ｐ→（Ｑ→Ｐ）
１ （１） Ｐ 仮定
１ （２） Ｐ∨～Ｑ １∨導入
３ （３） Ｐ Ａ
３ （４） ～Ｑ∨ Ｐ ３∨導入
５ （５） ～Ｑ Ａ
５ （６） ～Ｑ∨ Ｐ ５∨導入
１ （７） ～Ｑ∨ Ｐ ２３４５６∨除去
８ （８） Ｑ＆～Ｐ 仮定
９ （９） ～Ｑ Ａ
８ （ア） Ｑ ＆除去
８９ （イ） ～Ｑ＆ Ｑ ９ア＆導入
９ （ウ）～（Ｑ＆～Ｐ） ８イ背理法
エ （エ） Ｐ 仮定
８ （オ） ～Ｐ ８＆除去
８エ （カ） Ｐ＆～Ｐ エオ＆導入
エ （キ）～（Ｑ＆～Ｐ） ８カ背理法
１ （ク）～（Ｑ＆～Ｐ） ７９ウエキ∨除去
ケ （ケ） Ｑ 仮定
コ（コ） ～Ｐ 仮定
ケコ（サ） Ｑ＆～Ｐ ケコ＆導入
１ ケコ（シ）～（Ｑ＆～Ｐ）＆
（Ｑ＆～Ｐ） クサ＆導入
１ ケ （ス） ～～Ｐ コシ背理法
１ ケ （セ） Ｐ ス二重否定
１ （ソ） Ｑ→Ｐ ケセ条件法（仮定の解消）
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
であれば、
１ （２） Ｐ∨～Ｑ １∨導入
３ （４） ～Ｑ∨ Ｐ ３∨導入
５ （６） ～Ｑ∨ Ｐ ５∨導入
といふ「三つ」が、「∨-導入の規則」に、他ならない。
従って、
（01）（26）（28）により、
（29）
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふやうな、「∨-導入の規則」を、認めないのであれば、
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
といふ「結論」、すなはち、
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
といふ、ことになる。
従って、
（27）（28）（29）により、
（30）
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」は、「ナンセンス（無意味）」であるやうでゐて、それを認めない限り、
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
ヒルベルトの演繹システムは、公理が多く、推論規則が少ないものです。そして、公理も、わけのわからない論理式となっています。例えば、
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
という論理式が公理として設定されています。つまり、この論理式を出発点として演繹を行って良い。ということです。多くの人は、この論理式の意味を飲みこめないでしょう。
（小島寛之、証明と論理に強くなる、2017年、１３６頁）
然るに、
（02）
次に、命題論理の自然演繹の「公理」です。面白いことに「公理」は一つもありません。ここに自然演繹の大きな特徴があります。「出発点とする公理が何もないのに、いったいどうやって演繹するんだ」という疑問が湧いてくるでしょう。
（小島寛之、証明と論理に強くなる、2017年、１４０頁）
（03）
自然演繹には「仮定の解消」（最初に仮定しておいて、あとでなかったことにする）という手続きがあり、それがなかなか理解しづらいことです。自然演繹は「仮定の解消」のおかげで公理なしに演繹システムとなり得ており、その意味で「仮定の解消」は自然演繹の本質だと言っても過言ではありません。
（小島寛之、証明と論理に強くなる、2017年、１４４頁）
然るに、
（04）
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
といふ「ヒルベルトの公理」に対する、「自然演繹」による「証明」は、次のやうになる。
（05）
（５）├ Ｐ→（Ｑ→Ｐ）
１ （１） Ｐ 仮定
１ （２） Ｐ∨～Ｑ １∨導入
３ （３） Ｐ Ａ
３ （４） ～Ｑ∨ Ｐ ３∨導入
５ （５） ～Ｑ Ａ
５ （６） ～Ｑ∨ Ｐ ５∨導入
１ （７） ～Ｑ∨ Ｐ ２３４５６∨除去
８ （８） Ｑ＆～Ｐ 仮定
９ （９） ～Ｑ Ａ
８ （ア） Ｑ ＆除去
８９ （イ） ～Ｑ＆ Ｑ ９ア＆導入
９ （ウ）～（Ｑ＆～Ｐ） ８イ背理法
エ （エ） Ｐ 仮定
８ （オ） ～Ｐ ８＆除去
８エ （カ） Ｐ＆～Ｐ エオ＆導入
エ （キ）～（Ｑ＆～Ｐ） ８カ背理法
１ （ク）～（Ｑ＆～Ｐ） ７９ウエキ∨除去
ケ （ケ） Ｑ 仮定
コ（コ） ～Ｐ 仮定
ケコ（サ） Ｑ＆～Ｐ ケコ＆導入
１ ケコ（シ）～（Ｑ＆～Ｐ）＆
（Ｑ＆～Ｐ） クサ＆導入
１ ケ （ス） ～～Ｐ コシ背理法
１ ケ （セ） Ｐ ス二重否定
１ （ソ） Ｑ→Ｐ ケセ条件法（仮定の解消）
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
然るに、
（06）
① Ｐ├ Ｐ
② Ｐ→ Ｐ
といふ「式」は、それぞれ、
① Ｐだから、Ｐである。
② Ｐならば、Ｐである。
といふ、「意味」である。
ｃｆ.
同一律（law of identity）
然るに、
（07）
① Ｐだから、Ｐである。
② Ｐならば、Ｐである。
に於いて、
① であれば、 Ｐである。が、
② であっても、Ｐである。とは、限らない。
従って、
（06）（07）により、
（08）
① Ｐだから、Ｐである。
② Ｐならば、Ｐである。
に於いて、
① ≠ ② であって、
①＝② ではない。
然るに、
（09）
① Ｐ├ Ｐ
② Ｐ→ Ｐ
に於いて、
① を、
② に、「書き換へ」ることを、「仮定の解消」といふ。
ｃｆ.
１（１）Ｐ 仮定
（２）Ｐ→Ｐ １１条件法
従って、
（10）
① Ｐ├（Ｑ→Ｐ）
② Ｐ→（Ｑ→Ｐ）
に於いて、
① を、
② に、「書き換へ」ることも、「仮定の解消」である。
然るに、
（05）により、
（11）
１ （１）Ｐ 仮定
１ （ソ） Ｑ→Ｐ ケセ条件法（仮定の解消）
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
であるものの、このことは、
① Ｐ├（Ｑ→Ｐ）：Ｐだから（ＱならばＰである。）
② Ｐ→（Ｑ→Ｐ）：Ｐならば（ＱならばＰである。）
に於いて、
① を、
② に、「書き換へ」ることに、相当する。
従って、
（01）（11）により、
（12）
① Ｐ├（Ｑ→Ｐ）：Ｐだから、ＱならばＰである。
といふ「式」の、「仮定を解消」した「結果」が、
② Ｐ→（Ｑ→Ｐ）：Ｐならば、ＱならばＰである。
といふ「ヒルベルトの公理」である。
然るに、
（13）
（ａ）
１ （１） Ｑ→ Ｐ 仮定
２ （２） Ｑ＆～Ｐ 仮定
２ （３） Ｑ ２＆Ｅ
１２ （４） Ｐ １３前件肯定
２ （５） ～Ｐ ２＆除去
１２ （６） Ｐ＆～Ｐ ４５＆導入
１ （７）～（Ｑ＆～Ｐ） ２６背理法
（ｂ）
１ （１）～（Ｑ＆～Ｐ） 仮定
２ （２） Ｑ 仮定
３（３） ～Ｐ 仮定
２３（４） Ｑ＆～Ｐ ２３＆導入
１２３（５）～（Ｑ＆～Ｐ）＆
（Ｑ＆～Ｐ） １４＆導入
１２ （６） ～～Ｐ ３５背理法
１２ （７） Ｐ ６二重否定
１ （８） Ｑ→ Ｐ ２７条件法
従って、
（13）により、
（14）
① ～（Ｑ→～Ｐ）＝ＱならばＰである。
② ～（Ｑ＆～Ｐ）＝ＱであってＰでない。といふことはない。
に於いて、
①＝② である。
然るに、
（15）
② ＱであってＰでない。といふことはない。
といふのであれば、
② Ｑでない。
といふ場合については、何も、言ってゐない。
従って、
（14）（15）により、
（16）
① ＱならばＰである。
といふのであれば、すなはち、
② ＱであってＰでない。といふことはない。
といふのであれば、
② Ｑでない。
といふ場合については、
② Ｐである。
といふことを、「否定」しない。
従って、
（14）（15）（16）により、
（17）
① ＱならばＰである。
といふ場合に、
① Ｑでない。
としても、
① Ｐでない。
といふことには、ならない。
従って、
（12）（17）により、
（18）
① Ｐ├ Ｑ→Ｐ（Ｐだから、ＱならばＰである。）
といふ「式」は、
① Ｐ├ Ｑ→Ｐ（Ｐだから、Ｑであっても、Ｑでなくとも、Ｐである。）
といふ風に、「読むこと」が出来る。
従って、
（01）（18）により、
（19）
② Ｐならば、ＱならばＰである。
といふ、「ヒルベルトの公理」は、
① Ｐだから、Ｑであっても、Ｑでなくとも、Ｐである。
としたら、
② Ｐならば、ＱならばＰである。
といふ「意味」に、解することが出来る。
（20）
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような9つの基本的規則だけを持つ。
１.仮定の規則 "The Rule of Assumption"
２.モーダスポネンス "Modus Ponendo Ponens"
３.二重否定の規則 "The Rule of Double Negation"
４.条件付き証明の規則 "The Rule of Conditional Proof"
５.＆-導入の規則 "The Rule of ＆-introduction"
６.＆-除去の規則 "The Rule of ＆-elimination"
７.∨-導入の規則 "The Rule of ∨-introduction"
８.∨-除去の規則 "The Rule of ∨-elimination"
９.背理法 "Reductio Ad Absurdum"
（ウィキペディア）
然るに、
（21）
ジョン・レモンが開発した体系 L には、
３.否定否定式（ＭＴＴ）
も、含まれてゐるため、実際には、「９つの基本的規則」ではなく、「１０個の基本規則（The 10 primitive rules）」とするのが、正しい。
然るに、
（21）
（ａ）
１ （１） Ｐ→ Ｑ Ａ
２ （２） ～Ｑ Ａ
３（３） Ｐ Ａ
１ ３（４） Ｑ １３ＭＰＰ
１２３（５）～Ｑ＆ Ｑ ２３＆Ｉ
１２ （６）～Ｐ ３５ＲＡＡ
１ （７）～Ｑ→～Ｐ ２６ＣＰ
（ｂ）
１ （１） ～Ｑ→～Ｐ Ａ
２ （２） Ｐ Ａ
３（３） ～Ｑ Ａ
１ ３（４） ～Ｐ １３ＭＰＰ
１２３（５） Ｐ＆～Ｐ ２４＆Ｉ
１２ （６）～～Ｑ ３５ＲＡＡ
１２ （７） Ｑ ６７ＤＮ
１ （８） Ｐ→ Ｑ ２７ＣＰ
（22）
（ａ）
１ （１） Ｐ→ Ｑ Ａ
２ （２） ～Ｑ Ａ
３（３） Ｐ Ａ
１２ （４）～Ｐ １２ＭＴＴ
１２３（５）～Ｐ＆ Ｐ ３４＆Ｉ
１２ （６）～Ｐ ３５ＲＡＡ
１ （７）～Ｑ→～Ｐ ２６ＣＰ
（ｂ）
１ （１） ～Ｑ→～Ｐ Ａ
２ （２） Ｐ Ａ
２ （３） ～～Ｐ ２ＤＮ
４（４） ～Ｑ Ａ
１２ （５）～～Ｑ １３ＭＴＴ
１２ （６） Ｑ ５ＤＮ
１２４（７） Ｑ＆～Ｑ ４６＆Ｉ
１２ （８）～～Ｑ ４７ＲＡＡ
１２ （９） Ｑ ８ＤＮ
１ （ア） Ｐ→ Ｑ ２９ＣＰ
従って、
（21）（22）により、
（23）
ＭＰＰは、ＭＴＴに、「置き換へ」ることが出来、
ＭＴＴは、ＭＰＰに、「置き換へ」ることが出来る。
従って、
（23）により、
（24）
ＭＴＴは原始的規則と解される必要はなく、他の規則から導出される規則としてえられる（E.J.レモン著、竹尾治一郎・浅野楢英 訳、論理学初歩、７８頁）し、ＭＰＰも、さうである。
然るに、
（25）
① 今日は水曜である。
② 今日は水曜であるか、明日は雨でない。
に於いて、
① が「本当（真）」ならば、
② も「本当（真）」である。
然るに、
（26）
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふ「推論」を、「∨-導入の規則」といふ。
然るに、
（27）
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」を、「日常に於いて行ふ」ことは、「普通は、無い」。
然るに、
（05）により、
（28）
（５）├ Ｐ→（Ｑ→Ｐ）
１ （１） Ｐ 仮定
１ （２） Ｐ∨～Ｑ １∨導入
３ （３） Ｐ Ａ
３ （４） ～Ｑ∨ Ｐ ３∨導入
５ （５） ～Ｑ Ａ
５ （６） ～Ｑ∨ Ｐ ５∨導入
１ （７） ～Ｑ∨ Ｐ ２３４５６∨除去
８ （８） Ｑ＆～Ｐ 仮定
９ （９） ～Ｑ Ａ
８ （ア） Ｑ ＆除去
８９ （イ） ～Ｑ＆ Ｑ ９ア＆導入
９ （ウ）～（Ｑ＆～Ｐ） ８イ背理法
エ （エ） Ｐ 仮定
８ （オ） ～Ｐ ８＆除去
８エ （カ） Ｐ＆～Ｐ エオ＆導入
エ （キ）～（Ｑ＆～Ｐ） ８カ背理法
１ （ク）～（Ｑ＆～Ｐ） ７９ウエキ∨除去
ケ （ケ） Ｑ 仮定
コ（コ） ～Ｐ 仮定
ケコ（サ） Ｑ＆～Ｐ ケコ＆導入
１ ケコ（シ）～（Ｑ＆～Ｐ）＆
（Ｑ＆～Ｐ） クサ＆導入
１ ケ （ス） ～～Ｐ コシ背理法
１ ケ （セ） Ｐ ス二重否定
１ （ソ） Ｑ→Ｐ ケセ条件法（仮定の解消）
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
であれば、
１ （２） Ｐ∨～Ｑ １∨導入
３ （４） ～Ｑ∨ Ｐ ３∨導入
５ （６） ～Ｑ∨ Ｐ ５∨導入
といふ「三つ」が、「∨-導入の規則」に、他ならない。
従って、
（01）（26）（28）により、
（29）
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふやうな、「∨-導入の規則」を、認めないのであれば、
（タ）Ｐ→（Ｑ→Ｐ） １ソ条件法（仮定の解消）
といふ「結論」、すなはち、
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
といふ、ことになる。
従って、
（27）（28）（29）により、
（30）
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」は、「ナンセンス（無意味）」であるやうでゐて、それを認めない限り、
Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。