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

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

　( A∧(B∨C) ) ⇒ ( (A∧B)∨(A∧C) )　　　　

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

【証明1-1】( A∧(B∨C) ) ⇒ ( (A∧B)∨(A∧C) )

　命題論理の形式的体系「自然演繹」に準拠した操作　　
　　　端的には、
　　　　・仮定の書き出し　
　　　　・推論規則「∧除去則」による書き換え　　
　　　　・推論規則「∧導入則」による書き換え　
　　　　・推論規則「∨導入則」による書き換え
　　　　・推論規則「∨除去則」による書き換え　　　
　　　　・推論規則「⇒導入則」による書き換え　
　のみで、
　論理式「( A∧(B∨C) ) ⇒ ( (A∧B)∨(A∧C) )」が得られる　　
　ことを示す。[前原p.121]

　→step01
　→step02
　→step03
　→step04
　→step05
　→step06
　→step07

　→分配律に戻る
　→自然演繹の定理：トピック一覧

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

・論理式「A∧(B∨C)」を仮定1として書き出す。

	仮定1　 A∧(B∨C)

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

　　・推論規則「∧除去則」にしたがって、
　　　　仮定1「A∧(B∨C)」を「B∨C」へ　
　　　　仮定1「A∧(B∨C)」を「A」へ
　　　書き換える。
　　・推論規則「∧除去則」により、
　　　書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
　　　書き換え後の「B∨C」「A」は、それぞれ、仮定1「A∧(B∨C)」のもとにある。
　　・これで、推論規則「∧除去則」による書き換えによって、
　　　仮定1「A∧(B∨C)」から、
　　　「仮定1『A∧(B∨C)』のもとで『B∨C』」
　　　「仮定1『A∧(B∨C)』のもとで『A』」
　　　が導出されたことになる。

	仮定1 A∧(B∨C)
		(∧除去)
	B∨C

	仮定1 A∧(B∨C)
		(∧除去)
	A


	【文献】　・前原『記号論理入門』7章§1.4(pp.121-2):( A∧(B∨C) )⇔( (A∧B)∨(A∧C) ) 　・野矢『論理学』1-2-3-LP-命題論理の諸定理-定理12(1-a)(1-b)(2-a)(2-b)(p.70);付録-定理12(1-a)(1-b)(2-a)(2-b)(pp.220-22):二項目とも両方向。　・van Dalen,Logic and Structure(3rd ed.) 1.6(pp.50-51) 　・林『数理論理学』例1.10(p.32)

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

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

	仮定1　 A∧(B∨C)
		(∧除去)
	B∨C

仮定1　 A∧(B∨C)
	(∧除去)	仮定2
A		B

仮定1　 A∧(B∨C)
	(∧除去)	仮定3
A		C

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

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

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

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

	仮定1　 A∧(B∨C)
		(∧除去)
	B∨C

仮定1　 A∧(B∨C)
	(∧除去)	仮定2
A		B
			（∧導入）
A∧B

仮定1　 A∧(B∨C)
	(∧除去)	仮定3
A		C

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

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

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

	仮定1　 A∧(B∨C)
		(∧除去)
	B∨C

仮定1　 A∧(B∨C)
	(∧除去)	仮定2
A		B
			（∧導入）
A∧B

仮定1　 A∧(B∨C)
	∧除去則	仮定3
A		C
			（∧導入）
A∧C

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

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

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

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

	仮定1　 A∧(B∨C)
		(∧除去)
	B∨C

仮定1　 A∧(B∨C)
	(∧除去)	仮定2
A		B
			（∧導入）
A∧B
			（∨導入）
(A∧B)∨(A∧C)

仮定1　 A∧(B∨C)
	(∧除去)	仮定3
A		C
			（∧導入）
A∧C

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

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

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

	仮定1　 A∧(B∨C)
		(∧除去)
	B∨C

仮定1　 A∧(B∨C)
	(∧除去)	仮定2
A		B
			（∧導入）
A∧B
			（∨導入）
(A∧B)∨(A∧C)

仮定1　 A∧(B∨C)
	(∧除去)	仮定3
A		C
			（∧導入）
A∧C
			（∨導入）
(A∧B)∨(A∧C)

　→　自然演繹における分配律1-1証明冒頭
　→　自然演繹の定理：分配律
　→　自然演繹の定理：トピック一覧
　→　論理記号：トピック一覧　
　→　総目次　　

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

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

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

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

	仮定1　 A∧(B∨C)
		(∧除去)
	B∨C

仮定1　 A∧(B∨C)
	(∧除去)	[仮定2]
A		[B]
			（∧導入）
A∧B
			（∨導入）
(A∧B)∨(A∧C)

仮定1　 A∧(B∨C)
	(∧除去)	[仮定3]
A		[C]
			（∧導入）
A∧C
			（∨導入）
(A∧B)∨(A∧C)

(∨除去) 仮定2仮定3を解消

(A∧B)∨(A∧C)

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

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

	[仮定1]　 A∧(B∨C)
		(∧除去)
	B∨C

[仮定1]　 [A∧(B∨C)]
	(∧除去)	[仮定2]
A		[B]
			（∧導入）
A∧B
			（∨導入）
(A∧B)∨(A∧C)

[仮定1]　 [A∧(B∨C)]
	(∧除去)	[仮定3]
A		[C]
			（∧導入）
A∧C
			（∨導入）
(A∧B)∨(A∧C)

(∨除去) 仮定2仮定3を解消

(A∧B)∨(A∧C)

(⇒導入)仮定1を解消

( A∧(B∨C) ) ⇒ ( (A∧B)∨(A∧C) )

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

【証明1-1】( A∧(B∨C) ) ⇒ ( (A∧B)∨(A∧C) )

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

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

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

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

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