命題論理の自然演繹における諸定理 【12】選言的三段論法の証明

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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