命題論理の自然演繹における諸定理 【4】二重否定律　law of double negationの証明

・推論規則「二重否定除去則」にしたがって、「¬(¬A)」を「A」へ 書き換える。
・推論規則「二重否定除去則」により、
　　　書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
　　　 書き換え後の「A」は、仮定1「¬(¬A)」のもとにある。

・これで、推論規則「二重否定除去則」による書き換えで、
　　仮定1「¬(¬A)」から、
　　「仮定1『¬(¬A)』のもとで『A』」 が、
　　導出されたことになる。

[step3]自然演繹で認められた操作(3)推論規則による書き換え

・推論規則「⇒導入則」にしたがって、「仮定1『¬(¬A)』のもとでの『A』」 を「¬(¬A) ⇒ A」へ書き換える。
・推論規則「⇒導入則」の規定にしたがうと、
　　　「¬(¬A) ⇒ A」への書き換え後に引き継がれる仮定は、
　　　書き換え前の仮定「¬(¬A)」から、仮定「¬(¬A)」を差し引いた分だけとなる から、　　　
　　　「¬(¬A) ⇒ A」への書き換え後に仮定はすべて差し引かれてなくなってしまい、
　　　　仮定なしの「¬(¬A) ⇒ A」が得られる。
・これで、推論規則「⇒導入則」による書き換えで、
　　「仮定1『¬(¬A)』のもとで『A』」 から、
　　仮定なしの「¬(¬A) ⇒ A」が導出されたことになる。

【証明:二重否定導入】A ⇒ ¬(¬A)

[step1]自然演繹で認められた操作(2)仮定の書き出し

[step2]自然演繹で認められた操作(3)推論規則による書き換え

・推論規則「¬除去則」にしたがって、「A」「¬A」を「⋏(矛盾)」へ書き換える。
・推論規則「¬除去則」の規定により、
　　　書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
　　　 書き換え後の「⋏(矛盾)」は、仮定1「A」仮定 2「¬A」のもとにある。

・これで、推論規則「¬除去則」による書き換えで、
　　仮定1「A」仮定2「¬A」 から、
　　「仮定1『A』仮定2『¬A』 のもとで『⋏(矛盾)』」が、
　　導出されたことになる。

[step3]自然演繹で認められた操作(3)推論規則による書き換え

・推論規則「¬導入則」にしたがって、「仮定1『A』仮定 2『¬A』のもとでの『⋏(矛盾)』」を「¬(¬A)」へ書き換える。
　推論規則「¬導入則」の規定にしたがうと、
　　　「¬(¬A)」への書き換え後に引き継が れる仮定は、
　　　書き換え前の仮定「A」「¬A」 から、仮定「¬A」を差し引い た分だけとなるから、　　　
　　　「¬(¬A)」への書き換え後に引き継が れる仮定は、「A」だけ。

・これで、推論規則「¬導入則」による書き換えで、
　　「仮定1『A』仮定2『¬A』 のもとでの『⋏(矛盾)』」から、
　　「仮定1『A』のもとで『¬(¬A)』」が、
　　導出されたことになる。

[step4]自然演繹で認められた操作(3)推論規則による書き換え