「二重否定の除去」は、「自然演繹」で「演繹」出来る。

（01）
７　実際上、われわれの規則ＤＮはつぎの２つの規則が結合したものである。
（ⅰ）Ａから～～Ａを導出すること、そして、
（ⅱ）～～ＡからＡを導出すること、
（ⅰ）は他の原始的規則から導出されることを示せ（規則ＭＴＴ、すなわち連式５５、対する、これに対応する証明を参照せよ）。
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、８１頁）
（02）
〔解答〕
１　（１）　  Ｐ　　　　　Ａ
　２（２）　～Ｐ　　　　　Ａ
１２（３）　　Ｐ＆～Ｐ　　１２＆Ｉ
１　（４）～～Ｐ　　　　　２３ＲＡＡ
　　（５）　　Ｐ→～～Ｐ　１４ＣＰ
ｃｆ.
ただし、「E.J.レモン、論理学初歩」には、「練習問題の解答」は、載ってゐません。
従って、
（02）により、
（03）
１　（１）　  （Ｐ）　　　　　　　Ａ
　２（２）　（～Ｐ）　　　　　　　Ａ
１２（３）　　（Ｐ）＆（～Ｐ）　　１２＆Ｉ
１　（４）～（～Ｐ）　　　　　　　２３ＲＡＡ
　　（５）　　（Ｐ）→～（～Ｐ）　１４ＣＰ
然るに、
（04）
１　　（１）　　　　（Ｐ）　　　　　　　Ａ
　２　（２）　　　（～Ｐ）　　　　　　　Ａ
１２　（３）　　　　（Ｐ）＆（～Ｐ）　　１２＆Ｉ
１　　（４）　　～（～Ｐ）　　　　　　　２３ＲＡＡ
　　　（５）　　　　（Ｐ）→～（～Ｐ）　１４ＣＰ
　　６（６）　　　　　　　～～（～Ｐ）　Ａ
　　６（７）　　　（～Ｐ）　　　　　　　５６ＭＴＴ
　　　（８）　～～（～Ｐ）→  （～Ｐ）　６７ＣＰ
然るに、
（05）
系Ⅰ：任意の連式は、それがトートロジー的であるときまたそのときに限って導出可能である。
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、１１４頁）
従って、
（03）（04）（05）により、
（06）
①       （Ｐ）→～（～Ｐ）
② ～～（～Ｐ）→  （～Ｐ）
は、「恒真式（トートロジー）」である。
然るに、
（07）
①       （Ｐ）→～（～Ｐ）
といふ「式」は、
①       （Ｐ）→～～（Ｐ）
といふ「式」に、「等しい」。
従って、
（06）（07）により、
（08）
①       （Ｐ）→～～（Ｐ）
② ～～（～Ｐ）→  （～Ｐ）
といふ「式」は、「恒真式（トートロジー）」である。
然るに、
（09）
（Ｓ１）証明された定理の任意の代入例に対して、証明が見いだされうる。
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、６９頁）
１ 代入の規則
　一つの恒真式のなかの命題変項を他の命題変項、または論理式でおきかえることによって得られた式は同じく恒真式である。
（沢田允、現代論理学入門、1962年、１７３頁）
従って、
（08）（09）により、
（10）
①       （Ｐ）→～～（Ｐ）
② ～～（～Ｐ）→  （～Ｐ）
に於いて、
～Ｐ＝Ｐ
といふ「代入（Substitution）」を行へば、
①     （Ｐ）→～～（Ｐ）
② ～～（Ｐ）→　　（Ｐ）
といふ「式」は、「恒真式（トートロジー）」である。
従って、
（10）により、
（11）
①     Ｐ→～～Ｐ
② ～～Ｐ→　　Ｐ
といふ「式」は、「恒真式（トートロジー）」である。
然るに、
（01）により、
（12）
① 仮定（Ａ）
② 前件肯定（ＭＰＰ）
③ 後件否定（ＭＴＴ）
④ 二重否定（ＤＮ）
⑤ 条件法的証明（ＣＰ）
⑥ 連言導入（＆Ｉ）
⑦ 連言除去（＆Ｅ）
⑧ 選言導入（∨Ｉ）
⑨ 選言除去（∨Ｅ）
⑩ 背理法（ＲＡＡ）　　
といふ「１０個の規則」を、「原始的規則（10 primitive rules）」といふ。
従って、
（01）（11）（12）により、
（13）
実際上、われわれの規則「二重否定（ＤＮ）」はつぎの２つの規則が結合したものである。
（ⅰ）Ａから～～Ａを導出すること、そして、
（ⅱ）～～ＡからＡを導出すること、そして、
（ⅰ）は他の原始的規則（Ａ、＆Ｉ、ＲＡＡ、ＣＰ）」　　　から導出されることを示せるし、
（ⅱ）も他の原始的規則（Ａ、＆Ｉ、ＲＡＡ、ＣＰ、ＭＴＴ）から導出されることを示せる。
といふことが、分かった、ことになる。
従って、
（12）（13）により、
（14）
① 仮定（Ａ）
② 前件肯定（ＭＰＰ）
③ 後件否定（ＭＴＴ）
④ 二重否定（ＤＮ）
⑤ 条件法的証明（ＣＰ）
⑥ 連言導入（＆Ｉ）
⑦ 連言除去（＆Ｅ）
⑧ 選言導入（∨Ｉ）
⑨ 選言除去（∨Ｅ）
⑩ 背理法（ＲＡＡ）　
から、
④ 二重否定（ＤＮ）
を除いて、「原始的規則（9 primitive rules）」としても、「支障」は無い。
然るに、
（15）
"「Ｐではない」ではないならば、Ｐである"
つまり、否定を～で表すと「～～ＰならばＰ」だと言ってます。
……何か問題が?
けどこれ「二重否定の除去」といって、成り立つことが示せないんですよ。　　
（排中律、二重否定の除去、パースの法則 - Qiita）
従って、
（13）（14）（15）により、
（16）
けどこれ「二重否定の除去」といって、成り立つことが示せないんですよ。
といふことには、ならない。
然るに、
（17）
直観主義論理
出典: フリー百科事典『ウィキペディア（Wikipedia）』
証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。
然るに、
（18）
　―「排中律」の証明 ―
４４　├ Ｐ∨～Ｐ
１　（１）　～（Ｐ∨～Ｐ）　　Ａ
　２（２）　　　Ｐ　　　　　　Ａ
　２（３）　　　Ｐ∨～Ｐ　　　２∨Ｉ
１２（４）　～（Ｐ∨～Ｐ）＆
　　　　　　　（Ｐ∨～Ｐ）　　１３＆Ｉ
１　（５）　　～Ｐ　　　　　　２４ＲＡＡ
１　（６）　　　Ｐ∨～Ｐ　　　５∨Ｉ
１　（７）　～（Ｐ∨～Ｐ）＆
　　　　　　　（Ｐ∨～Ｐ）　　１６＆Ｉ
１　（８）～～（Ｐ∨～Ｐ）　　１７ＲＡＡ
　　（９）　　　Ｐ∨～Ｐ　　　８ＤＮ
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、６６頁）
従って、
（16）（17）（18）により、
（19）
「直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。」
といは言ふものの、
「自然演繹からすれば、排中律や二重否定除去は、固より、公理ではなく、規則から演繹される所の、定理に、過ぎない。」
令和０２年０２月０４日、毛利太。