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

A,Bに、どのような論理式(命題変数単体に限らない)をいれても、
　　　　( ¬B ⇒ ¬A ) 　⇒　(A⇒B) 　
は、【命題論理における自然演繹】の定理。

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

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

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

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

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

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

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

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

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

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

[step7] 自然演繹で認められた操作(1)公理の書き出し

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

　　・推論規則「∨除去則」にしたがって、
　　　　・公理の排中律「B∨¬B」
　　　　・仮定4「B」
　　　　・「仮定1『¬B』、仮定2『¬B ⇒ ¬A』、仮定3『A』のもとで、『B』」
　　　を「B」へ書き換える。

　　・推論規則「∨除去則」の規定により、
　　　　　《書き換え後に引き継がれる仮定》は、
　　　　　　　《「書き換え前の仮定」から『B』(仮定4),『¬B』(仮定1)を差し引いた分》だけ
　　　　　となるから、
　　　　　 書き換え後の「B」 は、仮定2「¬B ⇒ ¬A」 、仮定3「A」 のもとにある。

　　・これで、推論規則「∨除去則」による書き換えで、
　　　　・公理の排中律「B∨¬B」
　　　　・仮定4「B」
　　　　・「仮定1『¬B』、仮定2『¬B ⇒ ¬A』、仮定3『A』のもとで、『B』」
　　　から、
　　　「仮定2『¬B ⇒ ¬A』、仮定3『A』のもとで、『B』」
　　　が、導出されたことになる。

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

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

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

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

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