命題論理の自然演繹における諸定理 【15】後件否定式 Modus Tollensの証明

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

　　・推論規則「∧除去則」にしたがって、
　　　　仮定1「¬B∧(A⇒B)」 を「A⇒B」 へ
　　　書き換える。

　　・推論規則「∧除去則」にしたがって、
　　　　仮定1「¬B∧(A⇒B)」 を「¬B」 へ　
　　　書き換える。

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

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

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

　論理式「A」 を仮定2として書き出す。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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