「ルカジェヴィッツの公理（Ⅰ）」は「極めて、自然」である。

（01）
仮定として、（１）Ｐである。
その上　　　（２）Ｑかも知れない。
従って、　　（〃）Ｐか、または、　Ｑである。
従って、　　（〃）Ｑか、または、　Ｐである。
従って、　　（３）Ｑでないならば、Ｐである。
従って、　　（４）Ｐであるならば（Ｑでないならば、Ｐである）。
といふ「推論」は、明らかに「妥当」である。
従って、
（01）により、
（02）
１（１）　　　　　　Ｐ　　Ａ
１（２）　　　　Ｑ∨Ｐ　　１∨Ｉ
１（３）　　　～Ｑ→Ｐ　　２含意の定義
　（４）Ｐ→（～Ｑ→Ｐ）　１３ＣＰ
といふ「自然演繹（Natural deduction）」は、「自然（Natural）」である。
然るに、
（03）
① Ｐ→（～Ｑ→Ｐ）
に於いて、
Ｑ＝～Ｑ
といふ「代入（Substitution）」を行ふと、
② Ｐ→（～～Ｑ→Ｐ）
従って、
（03）により、
（04）
「二重否定律（ＤＮ）」により、
① Ｐ→（～Ｑ→Ｐ）
に於いて、
Ｑ＝～Ｑ
といふ「代入（Substitution）」を行ふと、
② Ｐ→（　Ｑ→Ｐ）
といふ「ルカジェヴィッツの公理（Ⅰ）」になる。
従って、
（01）～（04）により、
（05）
仮定として、（１）Ｐである。
その上　　　（２）Ｑかも知れない。
従って、　　（〃）Ｐか、または、　Ｑである。
従って、　　（〃）Ｑか、または、　Ｐである。
従って、　　（３）Ｑでないならば、Ｐである。
従って、　　（４）Ｐであるならば（Ｑでないならば、Ｐである）。
といふ「推論」が、明らかに「妥当」であるが故に、
① Ｐ→（～Ｑ→Ｐ）
② Ｐ→（　Ｑ→Ｐ）
といふ「論理式」は、明らかに、「恒真式（トートロジー）」。
従って、
（05）により、
（06）
① Ｐ→（～Ｑ→Ｐ）≡Ｐならば（Ｑでないならば、Ｐである）。
② Ｐ→（　Ｑ→Ｐ）≡Ｐならば（Ｑであるならば、Ｐである）。
といふ「恒真式（トートロジー）」は、すなはち、
③ Ｐ→（　Ｑ→Ｐ）≡Ｐならば（Ｑであらうと、なからうと、Ｐである）。
といふ「恒真式（トートロジー）」は、「公理（axiom）」と呼ぶに、相応しい。
然るに、
（07）
実際の、「ルカジェヴィッツの公理（Ⅰ）」は、
② Ｐならば（Ｑであるならば、Ｐである）。
と「読まれる」のが「普通」であり、
③ Ｐならば（Ｑであらうと、なからうと、Ｐである）。
とは、「読まれない」。
従って、
（06）（07）により、
（08）
② Ｐ→（Ｑ→Ｐ）≡Ｐならば（Ｑであるならば、Ｐである）。
といふ「ルカジェヴィッツの公理（Ⅰ）」を、最初に知ったとき、私自身も、「戸惑ふ」ことになる。
然るに、
（09）
自然演繹
出典: フリー百科事典『ウィキペディア（Wikipedia）』
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような「９つの基本的規則」だけを持つ。
仮定の規則 "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"       　（ＲＡＡ）
然るに、
（10）
ウィキペディアの編集者も、本当は知ってゐる通り、実際には、ジョン・レモンが開発した体系 L は
仮定の規則 "The Rule of Assumption"               （Ａ）
モーダスポネンス   "Modus Ponendo Ponens"　　　　 （ＭＰＰ）
モーダストレンス　 "Modus tollendo tollens"       （ＭＴＴ）
二重否定の規則     "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"       　（ＲＡＡ）
といふ「１０個の原始的規則（10 primitive rules）」だけを持つ。
　ｃｆ.
　（ＭＴＴ）は（ＭＰＰ）から「導出」されるので、
　（ＭＴＴ）は、要らないはずである。といふのが、編集者の考へであるやうであるが、
　（ＭＰＰ）も（ＭＴＴ）から「導出」されるので、（ＭＰＰ）でなく、敢へて（ＭＴＴ）を「除く」のであれば、その「理由（合理性）」を
　説明しなければ、ならない。
　ｃｆ.
　（ａ）Ｐ→Ｑ，～Ｑ├ ～Ｐ
　１　　（１）　Ｐ→　Ｑ　Ａ
　　２　（２）　　　～Ｑ　Ａ
　　　３（３）　Ｐ　　　　Ａ
　１　３（４）　　　　Ｑ　１３ＭＰＰ
　１２３（５）　～Ｑ＆Ｑ　２３＆Ｉ
　１２　（６）～Ｐ　　　　３ＲＡＡ
　（ｂ）Ｐ→Ｑ，Ｐ├ Ｑ　
　１　　（１）　Ｐ→　Ｑ　Ａ
　　２　（２）　Ｐ　　　　Ａ
　　　３（３）　　　～Ｑ　Ａ
　１　３（４）～Ｐ　　　　１３ＭＴＴ
　１２３（５）Ｐ＆～Ｐ　　２４＆Ｉ
　１２　（６）　　～～Ｑ　３５ＲＡＡ
　１２　（７）　　　　Ｑ　６ＤＮ　　　
従って、
（02）（10）により、
（11）
１（１）　　　　　Ｐ　　Ａ
１（２）　　～Ｑ∨Ｐ　　１∨Ｉ
１（３）　　　Ｑ→Ｐ　　２含意の定義
　（４）Ｐ→（Ｑ→Ｐ）　１３ＣＰ
に於ける、
１（３）含意の定義（Ｄｆ.→）　
は、「１０個の原始的規則」の中には入ってゐない。
従って、
（11）により、
（12）
　（４）Ｐ→（Ｑ→Ｐ）　１３Ｃ
の「証明」は、実際には、次（13）のようになる。
（13）
　　― ルカジェヴィッツの公理（Ⅰ）―
１　　　　　（１）　　　　　　Ｐ　　　Ａ
１　　　　　（２）　　～Ｑ∨　Ｐ　　　Ａ
　３　　　　（３）　　　Ｑ＆～Ｐ　　　Ａ
　　４　　　（４）　　～Ｑ　　　　　　Ａ
　３　　　　（５）　　　Ｑ　　　　　　３＆Ｅ
　３４　　　（６）　　～Ｑ＆Ｑ　　　　４５＆Ｉ
　　４　　　（７）　～（Ｑ＆～Ｐ）　　３６ＲＡＡ
　　　８　　（８）　　　　　　Ｐ　　　Ａ
　３　　　　（９）　　　　　～Ｐ　　　３＆Ｅ
　３　８　　（ア）　　　Ｐ＆～Ｐ　　　８９＆Ｉ
　　　８　　（イ）　～（Ｑ＆～Ｐ）　　３アＲＡＡ
１　　　　　（ウ）　～（Ｑ＆～Ｐ）　　２４７８イ∨Ｅ
　　　　エ　（エ）　　　Ｑ　　　　　　Ａ
　　　　　オ（オ）　　　　　～Ｐ　　　Ａ
　　　　エオ（カ）　　　Ｑ＆～Ｐ　　　エオ＆Ｉ
１　　　エオ（キ）　～（Ｑ＆～Ｐ）＆
　　　　　　　　　　　（Ｑ＆～Ｐ）　　ウカ＆Ｉ
１　　　エ　（ク）　　　　～～Ｐ　　　オキＲＡＡ
１　　　エ　（ケ）　　　　　　Ｐ　　　クＤＮ
１　　　　　（コ）　　　Ｑ→　Ｐ　　　エケＣＰ（含意の定義を、計算の中で、証明した。）
　　　　　　（サ）Ｐ→（Ｑ→　Ｐ）　　１コＣＰ
然るに、
（14）
以上の「証明（13）」の中で、使はれてゐる「Ａ、＆Ｅ、＆Ｉ、ＲＡＡ、∨Ｅ、ＤＮ、ＣＰ」といふ「規則」は、全て「自然（Natural）」である。
従って、
（05）（06）（14）により、
（15）
③ Ｐ→（　Ｑ→Ｐ）≡Ｐならば（Ｑであらうと、なからうと、Ｐである）。
といふ「恒真式（トートロジー）」は、「公理（axiom）」と呼ぶに、相応しい。
令和０２年０７月１０日、毛利太。