ヒルベルトの公理：Ｐならば（ＱならばＰである）。

（ａ）『返り点と括弧』については、『「括弧」の「順番」（https://kannbunn.blogspot.com/2018/01/blog-post.html）』他をお読み下さい。
（ｂ）『返り点』については、『「返り点」の「付け方」を教へます（https://kannbunn.blogspot.com/2018/01/blog-post_3.html）』他をお読み下さい。
（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"  （＆I）
６.＆-除去の規則      "The Rule of ＆-elimination"   （＆E）
７.∨-導入の規則      "The Rule of ∨-introduction"  （∨I）
８.∨-除去の規則      "The Rule of ∨-elimination"   （∨E）
９.背理法             "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）
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」は、「ナンセンス（無意味）」であるやうでゐて、それを認めない限り、
　　　　 Ｐ→（Ｑ→Ｐ）（Ｐならば（ＱならばＰ））
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
平成３０年０６月２１日、毛利太。