「（E.J.レモンの）自然演繹の規則」と「公理系ＰＬ」。

（01）
標準的な命題論理に対して健全で完全な公理系はいろいろなものが作れます。一つの具体例を示してみましょう。
　公理系ＰＬ
公理１　（Ｐ∨Ｐ）→Ｐ
公理２　　Ｐ→（Ｐ∨Ｑ）
公理３　（Ｐ∨Ｑ）→（Ｑ∨Ｐ）
公理４　（Ｐ→Ｑ）→（（Ｐ∨Ｒ）→（Ｑ∨Ｒ））
推論規則　Ｐ→Ｑ と Ｐ から Ｑ を導いてもよい。
定義１　　Ｐ＆Ｑ は ～（～Ｐ∨～Ｑ）の略記である。
定義２　　Ｐ→Ｑ は ～Ｐ∨Ｑ の略記である。
（矢野茂樹、まったくゼロからの論理学、2020年、１６７頁改）
然るに、
（02）
１　　（１）　Ｐ∨Ｐ　　　　Ａ
　２　（２）　Ｐ　　　　　　Ａ
　　３（３）　　　Ｐ　　　　Ａ
１　　（４）　Ｐ　　　　　　１２２３３∨Ｅ
　　　（５）（Ｐ∨Ｐ）→Ｐ　１４ＣＰ
従って、
（01）（02）により、
（03）
「公理系ＰＬ（公理１）」が「恒真式（トートロジー）」であることを、
「仮定の規則（Ａ）」と「∨‐除去（∨Ｅ）」と「条件的証明（ＣＰ）」で、「証明」出来る。
（04）
１（１）Ｐ　　　　　　　Ａ
１（２）Ｐ∨Ｑ　　　　　１∨Ｉ
　（３）Ｐ→（Ｐ∨Ｑ）　１２ＣＰ
従って、
（01）（04）により、
（05）
「公理系ＰＬ（公理２）」が「恒真式（トートロジー）」であることを、
「仮定の規則（Ａ）」と「∨‐導入（∨Ｉ）」と「条件的証明（ＣＰ）」で、「証明」出来る。
（06）
１　　（１）　Ｐ∨Ｑ　　　　　　　　Ａ
　２　（２）　Ｐ　　　　　　　　　　Ａ
　２　（３）　Ｑ∨Ｐ　　　　　　　　２∨Ｉ
　　４（４）　　　Ｑ　　　　　　　　Ａ
　　４（５）　Ｑ∨Ｐ　　　　　　　　４∨Ｉ
１　　（６）　　　　　　　Ｑ∨Ｐ　　１２３４５∨Ｅ
　　　（７）（Ｐ∨Ｑ）→（Ｑ∨Ｐ）　１６ＣＰ
従って、
（01）（06）により、
（07）
「公理系ＰＬ（公理３）」が「恒真式（トートロジー）」であることを、
「仮定の規則（Ａ）」と「∨‐導入（∨Ｉ）」と「∨‐除去（∨Ｅ）」と「条件的証明（ＣＰ）」で、「証明」出来る。
（08）
１　　　（１）　Ｐ→Ｑ　　　　　　　　　　　　　　　　Ａ
　２　　（２）　Ｐ∨Ｒ　　　　　　　　　　　　　　　　Ａ
　　３　（３）　Ｐ　　　　　　　　　　　　　　　　　　Ａ
１　３　（４）　　　Ｑ　　　　　　　　　　　　　　　　１３ＭＰＰ
１　３　（５）　Ｑ∨Ｒ　　　　　　　　　　　　　　　　４∨Ｉ
　　　６（６）　　　Ｒ　　　　　　　　　　　　　　　　Ａ
　　　６（７）　Ｑ∨Ｒ　　　　　　　　　　　　　　　　６∨Ｉ
１２　　（８）　Ｑ∨Ｒ　　　　　　　　　　　　　　　　２３５６７∨Ｅ
１　　　（９）（Ｐ∨Ｒ）→（Ｑ∨Ｒ）　　　　　　　　　２８ＣＰ
　　　　（ア）（Ｐ→Ｑ）→（（Ｐ∨Ｒ）→（Ｑ∨Ｒ））　１９ＣＰ
従って、
（01）（08）により、
（09）
「公理系ＰＬ（公理４）」が「恒真式（トートロジー）」であることを、
「仮定の規則（Ａ）」と「肯定肯定式（ＭＰＰ）」と「∨‐導入（∨Ｉ）」と「∨‐除去（∨Ｅ）」と「条件的証明（ＣＰ）」で、「証明」出来る。
然るに、
（10）
（ⅰ）
１　（１）Ｐ→（Ｑ→Ｒ）　Ａ
　２（２）Ｐ＆Ｑ　　　　　Ａ
　２（３）Ｐ　　　　　　　２＆Ｅ
１２（４）　　　Ｑ→Ｒ　　１３ＭＰＰ
　２（５）　　　Ｑ　　　　２＆Ｅ
１２（６）　　　　　Ｒ　　４５ＭＰＰ
１　（７）　Ｐ＆Ｑ→Ｒ　　２６ＣＰ
（ⅱ）
１　　（１）　Ｐ＆Ｑ→Ｒ　　Ａ
　２　（２）　Ｐ　　　　　　Ａ
　　３（３）　　　Ｑ　　　　Ａ
　２３（４）　Ｐ＆Ｑ　　　　２３＆Ｉ
１２３（５）　　　　　Ｒ　　１４ＭＰＰ
１２　（６）　　　Ｑ→Ｒ　　３５ＣＰ
１　　（７）Ｐ→（Ｑ→Ｒ）　２６ＣＰ
従って、
（10）により、
（11）
① Ｐ→（Ｑ→Ｒ）
②（Ｐ＆Ｑ）→Ｒ
に於いて、
①＝② である。
然るに、
（12）
① Ｐ→（Ｑ→Ｒ）
②（Ｐ＆Ｑ）→Ｒ
に於いて、
Ｐ＝（Ａ→Ｂ）
Ｑ＝　Ａ
Ｒ＝　Ｂ
といふ「代入（Substitution）」を行ふと、
① （Ａ→Ｂ）→（Ａ→Ｂ）
②（（Ａ→Ｂ）＆Ａ）→Ｂ
然るに、
（13）
① Ａ→Ａ≡「ＡならばＡである。」
といふ「論理式」は、「同一律（トートロジー）」である。
従って、
（13）により、
（14）
①　（Ａ→Ｂ）→（Ａ→Ｂ）≡「（ＡならばＢである）ならば（ＡならばＢである）。」
であっても、「同一律（トートロジー）」である。
然るに、
（15）
②（（Ａ→Ｂ）＆Ａ）→Ｂ　≡「（（ＡならばＢである）であってＡ）であるならばＢである。」
は、「肯定肯定式（ＭＰＰ）」である。
従って、
（10）～（15）により、
（16）
①　（Ａ→Ｂ）→（Ａ→Ｂ）≡　「（ＡならばＢである）ならば（ＡならばＢである）。」
②（（Ａ→Ｂ）＆Ａ）→Ｂ　≡「（（ＡならばＢである）であってＡ）であるならばＢである。」
に於いて、
①＝② であって、尚且つ、
① は「恒真式（トートロジー）」であって、
② は「肯定肯定式（ＭＰＰ）」である。
従って、
（16）により、
（17）
「肯定肯定式（ＭＰＰ）」は、「恒真式（トートロジー）」である。
然るに、
（01）（16）（17）により、
（18）
「公理系ＰＬ（推論規則）」は、「肯定肯定式（ＭＰＰ）」である。
従って、
（01）（18）により、
（19）
「公理系ＰＬ（推論規則）」が「恒真式（トートロジー）」であることを、
「仮定の規則（Ａ）」と「＆‐除去（＆Ｅ）」と「肯定肯定式（ＭＰＰ）」と「条件的証明（ＣＰ）」と「＆‐導入（＆Ｉ）」で、「証明」出来る。
（20）
（ⅰ）
１　　　（１）　　　Ｐ＆　Ｑ　　　Ａ
　２　　（２）　　～Ｐ∨～Ｑ　　　Ａ
１　　　（３）　　　Ｐ　　　　　　１＆Ｅ
　　４　（４）　　～Ｐ　　　　　　Ａ
１　４　（５）　　　Ｐ＆～Ｐ　　　３４＆Ｉ
　　４　（６）　～（Ｐ＆　Ｑ）　　１５ＲＡＡ
１　　　（７）　　　　　　Ｑ　　　１＆Ｅ
　　　８（８）　　　　　～Ｑ　　　Ａ
１　　８（９）　　　Ｑ＆～Ｑ　　　７８＆Ｉ
　　　８（ア）　～（Ｐ＆　Ｑ）　　１９ＲＡＡ
　２　　（イ）　～（Ｐ＆　Ｑ）　　２４６８ア∨Ｅ
１２　　（ウ）　　（Ｐ＆　Ｑ）＆
１　　　（エ）～（～Ｐ∨～Ｑ）　　２ウＲＡＡ
（ⅱ）
１　　　（１）～（～Ｐ∨～Ｑ）　　Ａ
　２　　（２）　　～Ｐ　　　　　　Ａ
　２　　（３）　　～Ｐ∨～Ｑ　　　２∨Ｉ
１２　　（４）～（～Ｐ∨～Ｑ）＆
　　　　　　　　（～Ｐ∨～Ｑ）　　１３＆Ｉ
１　　　（５）　～～Ｐ　　　　　　２４ＲＡＡ
１　　　（６）　　　Ｐ　　　　　　５ＤＮ
　　７　（７）　　　　　～Ｑ　　　Ａ
　　７　（８）　　～Ｐ∨～Ｑ　　　７∨Ｉ
１　７　（９）～（～Ｐ∨～Ｑ）＆
　　　　　　　　（～Ｐ∨～Ｑ）　　１８＆Ｉ
１　　　（ア）　　　　～～Ｑ　　　７９ＲＡＡ
１　　　（イ）　　　　　　Ｑ　　　アＤＮ
１　　　（ウ）　　　Ｐ＆　Ｑ　　　６イ＆Ｉ
従って、
（20）により、
（21）
①       Ｐ＆  Ｑ
② ～（～Ｐ∨～Ｑ）
に於いて、
①＝② である。
従って、
（01）（20）（21）により、
（22）
「公理系ＰＬ（定義１）」は、
仮定の規則（Ａ）」と「＆‐除去（＆Ｅ）」と「＆‐導入（＆Ｉ）」と「背理法（ＲＡＡ）」と「∨‐除去（∨Ｅ）」と「∨‐導入（∨Ｉ）」と「二重否定（ＤＮ）」で、「証明」出来る。
然るに、
（23）
（ⅰ）
１　（１）　　Ｐ→　Ｑ　Ａ
　２（２）　　Ｐ＆～Ｑ　Ａ
　２（３）　　Ｐ　　　　２＆Ｅ
　２（４）　　　　～Ｑ　２＆Ｅ
１２（５）　　　　　Ｑ　１３ＭＰＰ
１２（６）　　～Ｑ＆Ｑ　４５＆Ｉ
１　（７）　　　～～Ｑ　４６ＲＡＡ
１　（８）　　　　　Ｑ　７ＤＮ
１　（９）　～Ｐ∨　Ｑ　８∨Ｉ
（ⅱ）
１　　　　　（１）　～Ｐ∨　Ｑ　　　Ａ
　２　　　　（２）　　Ｐ＆～Ｑ　　　Ａ
　　３　　　（３）　～Ｐ　　　　　　Ａ
　２　　　　（４）　　Ｐ　　　　　　２＆Ｅ
　２３　　　（５）　～Ｐ＆Ｐ　　　　３４＆Ｉ
　　３　　　（６）～（Ｐ＆～Ｑ）　　２５ＲＡＡ
　　　７　　（７）　　　　　Ｑ　　　Ａ
　２　　　　（８）　　　　～Ｑ　　　２＆Ｅ
　２　７　　（９）　　Ｑ＆～Ｑ　　　７８＆Ｉ
　　　７　　（ア）～（Ｐ＆～Ｑ）　　２９ＲＡＡ
１　　　　　（イ）～（Ｐ＆～Ｑ）　　２３６７ア∨Ｅ
　　　　ウ　（ウ）　　Ｐ　　　　　　Ａ
　　　　　エ（エ）　　　　～Ｑ　　　Ａ
　　　　ウエ（オ）　　Ｐ＆～Ｑ　　　ウエ＆Ｉ
１　　　ウエ（カ）～（Ｐ＆～Ｑ）＆
　　　　　　　　　　（Ｐ＆～Ｑ）　　イオ＆Ｉ
１　　　ウ　（キ）　　　～～Ｑ　　　エキＲＡＡ
１　　　ウ　（ク）　　　　　Ｑ　　　キＤＮ
１　　　　　（ケ）　　Ｐ→　Ｑ　　　ウクＣＰ
従って、
（23）により、
（24）
① 　Ｐ→Ｑ
② ～Ｐ∨Ｑ
に於いて、
①＝② である。
従って、
（01）（23）（24）により、
（25）
「公理系ＰＬ（定義２）」は、
「仮定の規則（Ａ）」と「＆‐除去（＆Ｅ）」と「肯定肯定式（ＭＰＰ）」と「＆‐導入（＆Ｉ）」と「背理法（ＲＡＡ）」と「二重否定（ＤＮ）」と「∨‐導入（∨Ｉ）」と「∨‐除去（∨Ｅ）」と「条件的証明（ＣＰ）」で、「証明」出来る。
従って、
（01）～（25）により、
（26）
　公理系ＰＬ
公理１　（Ｐ∨Ｐ）→Ｐ
公理２　　Ｐ→（Ｐ∨Ｑ）
公理３　（Ｐ∨Ｑ）→（Ｑ∨Ｐ）
公理４　（Ｐ→Ｑ）→（（Ｐ∨Ｒ）→（Ｑ∨Ｒ））
推論規則　Ｐ→Ｑ と Ｐ から Ｑ を導いてもよい。
定義１　　Ｐ＆Ｑ は ～（～Ｐ∨～Ｑ）の略記である。
定義２　　Ｐ→Ｑ は ～Ｐ∨Ｑ の略記である。
の全ては、『（E.J.レモンの）自然演繹の規則』で、「証明」出来る。
然るに、
（16）（17）（18）により、
（27）
もう一度、確認すると、
①　（Ａ→Ｂ）→（Ａ→Ｂ）≡　「（ＡならばＢである）ならば（ＡならばＢである）。」
②（（Ａ→Ｂ）＆Ａ）→Ｂ　≡「（（ＡならばＢである）であってＡ）であるならばＢである。」
に於いて、
①＝② であって、尚且つ、
① は「恒真式（トートロジー）」であって、
② は「肯定肯定式（ＭＰＰ）」　であって、
② は「公理系ＰＬ（推論規則）」である。
然るに、
（01）～（09）により、
（28）
公理１　（Ｐ∨Ｐ）→Ｐ
公理２　　Ｐ→（Ｐ∨Ｑ）
公理３　（Ｐ∨Ｑ）→（Ｑ∨Ｐ）
公理４　（Ｐ→Ｑ）→（（Ｐ∨Ｒ）→（Ｑ∨Ｒ））
は、全て、「恒真式（トートロジー）」であるし、
公理２　　Ｐ→（Ｐ∨Ｑ）
の場合は、『（E.J.レモンの）自然演繹の規則』でいふ所の、「∨‐導入の規則（∨Ｉ）」である。
従って、
（27）（28）により、
（29）
「公理（Axioms）」も、「規則（Rules）」も、結局は、「恒真式（tautology）」である。
然るに、
（30）
もし証明をやってみたいのであれば、もっと証明がやりやすい公理系として「自然演繹」と呼ばれる公理系がありますから、それをお薦めします。
（矢野茂樹、まったくゼロからの論理学、2020年、１７０頁）
然るに、
（31）
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系Ｌ は、証明の構文規則に関する「10個の基本的規則（Primitive rules）」だけを持つ。
（ウィキペディア改）
従って、
（29）（30）（31）
（32）
「自然演繹論理のあるバージョンには、公理が存在しない。」とは、言ふものの、「規則（Rules）」も、「公理（Axioms）」の「一種」である。
令和０２年０９月０９日、毛利太。