命題論理の自然演繹における諸定理 【11】対偶律　の証明(1)

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

・論理式「¬B」を仮定3として書き出す。

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

　　・推論規則「¬除去則」にしたがって、
　　　　　　・「仮定1『A』、仮定2「A⇒B」のもとで『B』」
　　　　　　・仮定3「¬B」
　　　を「⋏（矛盾）」 へ書き換える。

　　・推論規則「¬除去則」の規定により、
　　　書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
　　　 書き換え後の「⋏」は、仮定1「A」、仮定2「A⇒B」 、仮定3「¬B」のもとにある。

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

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

・推論規則「¬導入則」にしたがって、
　「仮定1『A』、仮定2『A⇒B』仮定3『¬B』のもとで『⋏（矛盾）』」を
　「¬A」へ書き換える。

　推論規則「¬導入則」の規定にしたがうと、
　　　「¬A」への書き換え後に引き継が れる仮定は、
　　　書き換え前の仮定「A」「A⇒B」「¬B」 から、仮定「A」を差し引い た分だけとなるから、　　　
　　　「¬A」への書き換え後に引き継が れる仮定は、仮定2「A⇒B」、仮定3「¬B」。

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

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

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

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

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

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

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