（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）」と呼ぶに、相応しい。