命題論理の自然演繹における諸定理 【14】前件肯定式 Modus Ponens(MP)の証明

A,Bに、どのような論理式(命題変数単体に限らない)をいれても、

　( A∧(A⇒B) ) ⇒ B

は、

【命題論理における自然演繹】の定理。

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

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

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

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

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

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

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

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

[step4]　自然演繹で認められた操作(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」が導出されたことになる。