命題論理の自然演繹における諸定理 【8】分配律1-2　の証明

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

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

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

　　・推論規則「∨導入則」にしたがって、
　　　「仮定1『A∧B』のもとで『B』」を
　　　「B∨C」へ書き換える。

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

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

　　・推論規則「∨導入則」にしたがって、
　　　「仮定2『A∧C』のもとで『C』」を
　　　「B∨C」へ書き換える。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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