「二重否定律（ＤＮ）」は「公理」である？

（01）
１　（１）　Ｐ　　　　Ａ
　２（２）　　　～Ｐ　Ａ
１２（３）　Ｐ＆～Ｐ　１２＆Ｉ
１　（４）　　～～Ｐ　２３ＲＡＡ
　　（５）Ｐ→～～Ｐ　１４ＣＰ
従って、
（01）により、
（02）
Ｐ→～～Ｐ≡Ｐならば、Ｐでない、ではない。
は、「定理（Theorem）」である。
（03）
１　（１）　～（Ｐ∨～Ｐ）　　Ａ
　２（２）　　　Ｐ　　　　　　Ａ
　２（３）　　　Ｐ∨～Ｐ　　　２∨Ｉ
１２（４）　～（Ｐ∨～Ｐ）＆
　　　　　　　（Ｐ∨～Ｐ）　　１３＆Ｉ
１　（５）　　～Ｐ　　　　　　２４ＲＡＡ
１　（６）　　　Ｐ∨～Ｐ　　　５∨Ｉ
１　（７）　～（Ｐ∨～Ｐ）＆　
　　　　　　　（Ｐ∨～Ｐ）　　６１＆Ｉ
　　（８）～～（Ｐ∨～Ｐ）　　１７ＲＡＡ
　　（９）　　　Ｐ∨～Ｐ　　　８ＤＮ
従って、
（03）により、
（04）
Ｐ∨～Ｐ≡Ｐであるか、Ｐでない。
すなはち、「排中律」は、「定理（Theorem）」である。
然るに、
（05）
　　（１）　Ｐ→～～Ｐ　ＴＩ（定理導入の規則）
　　（２）～Ｐ∨～～Ｐ　１含意の定義
３　（３）～Ｐ　　　　　Ａ
３　（４）～～Ｐ∨～Ｐ　３∨Ｉ
　５（５）　　　～～Ｐ　Ａ
　５（６）～～Ｐ∨～Ｐ　５∨Ｉ
　　（７）～～Ｐ∨～Ｐ　２３４５６ＥＥ
　　（８）　　Ｐ∨～Ｐ　ＴＩ（定理導入の規則）
然るに、
（06）
Ｐ∨～Ｐ≡Ｐであるか、Ｐでない。
が「排中律」であるならば、
～Ｐ∨Ｐ≡Ｐであるか、Ｐでない。
も「排中律」であるに、違ひない。
然るに、
（07）
～Ｐ∨Ｐ≡Ｐであるか、Ｐでない。
に於いて、
Ｐ＝～Ｐ
といふ「代入（Substitutione）」を行ふと、
～～Ｐ∨～Ｐ
である。
従って、
（05）（06）（07）により、
（08）
⑦ ～～Ｐ∨～Ｐ
⑧     Ｐ∨～Ｐ
に於いて、
⑦ は「排中律」であるし、
⑧ も「排中律」であるに、違ひない。
従って、
（08）により、
（09）
「排中律」が、「一つしか無い」とするならば、
⑦ ～～Ｐ∨～Ｐ
⑧     Ｐ∨～Ｐ
に於いて、
⑦＝⑧ である。
然るに、
（10）
「全体が等しければ、部分も等しい。」
従って、
（09）（10）により、
（11）
⑦ ～～Ｐ∨～Ｐ
⑧     Ｐ∨～Ｐ
に於いて、
⑦＝⑧ であるが故に、
⑦ ～～Ｐ
⑧     Ｐ
に於いても、
⑦＝⑧ である。
然るに、
（03）により、
（12）
　　（８）～～（Ｐ∨～Ｐ）　　１７ＲＡＡ
　　（９）　　　Ｐ∨～Ｐ　　　８ＤＮ
に於いて、「ＤＮ（二重否定律）」が使はれてゐる。
然るに、
（13）
Ｐ→～～Ｐ≡Ｐならば、Ｐでない、ではない。
といふ「定理（Theorem）」に続いて、私が、「証明」したかったのは、その「逆」である、
～～Ｐ→Ｐ≡Ｐでない、ではない。ならば、Ｐである。
が「定理（Theorem）」である。といふことである。
従って、
（12）（13）により、
（14）
「証明」したいことがらを「証明」する過程で、
「証明」したいことがらを「使ってゐる」ので、「反則」である。
加へて、
（15）
「全体が等しければ、部分も等しい。」
といふのは、多分、「本当」であるが、「自然演繹（Natural deduction）」の本に、「そのやうなこと」は書かれてゐない。
従って、
（01）～（15）により、
（16）
私には、
Ｐ→～～Ｐ≡Ｐならば、Ｐでない、ではない。
といふ「定理（Theorem）」は「証明」出来ても、
～～Ｐ→Ｐ≡Ｐでない、ではない。ならば、Ｐである。
が「定理（Theorem）」であることを、「証明」出来ない。
然るに、
（17）
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような１０個の基本的規則だけを持つ。
３.二重否定の規則 "The Rule of Double Negation"（DN）
（ウィキペディア改）
然るに、
（18）
「Ｐ→～～Ｐ＆～～Ｐ→Ｐ」と書けば、
３.二重否定の規則 "The Rule of Double Negation"（DN）
は、「論理式」である。
従って、
（17）（18）により、
（19）
自然演繹論理のあるバージョンには、「公理」が存在しない。
とは言ふものの、
「Ｐ→～～Ｐ＆～～Ｐ→Ｐ（二重否定の規則）」といふ「規則（Rule）」 は、ほとんど、
「Ｐ→～～Ｐ＆～～Ｐ→Ｐ（二重否定の公理）」といふ「公理（Axiom）」と、変はらない。
令和０２年０１月１６日、毛利太。