命題論理の自然演繹における諸定理【10】ド・モルガンの法則　の証明(1)

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

【証明】( ￢(A∧B) ) ⇒ (￢A)∨(￢B)

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

　→ step01 / step02 / step03 / step04 / step05
　→ step06 / step07 / step08 / step09 / step10
　→ step11 / step12 / step13 / step14 / step15

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

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

	仮定1　　　A	仮定2 　　B

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

　　・推論規則「∧導入則」にしたがって、
　　　　仮定1「A」仮定2「B」
　　　を
　　　　「A∧B」
　　　へ書き換える。

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

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

仮定1　　　　A	仮定2 　　B
		(∧導入)
A∧B


	【文献】　・野矢『論理学』1-2-3-LP-命題論理の諸定理-定理9(1-a)(1-b)(2-a)(2-b)(p.70);付録-定理9(1-a)(1-b)(2-a)(2-b)(pp.218-9):二項目とも両方向。　・戸田山『論理学をつくる』練習問題69(p.230);9.3.1-9.3.2(pp.233-5)練習問題71(1)(p.235): 　・前原『記号論理入門』6章§1問(pp.107-8)( ￢(A∨B) )⇔ (￢A)∧(￢B) ;解答(p.184)( ￢(A∧B) )⇔ (￢A)∨(￢B) 　・van Dalen,Logic and Structure(3rd ed.) 1.6(p.52) 　・高崎金久『数理論理学入門』VII.2.2基本的な恒真式・演繹関係を形式的に確かめること[例4][例5];3.1排中律に依存する定理と依存しない定理

[step3]

仮定1　　　　A	仮定2 　　B
		∧導入	仮定3
A∧B			￢(A∧B)

[step4]

仮定1　　　A	仮定2 　　B
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏

[step5]

[仮定1]　　　[A]	仮定2 　　B
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A

[step6]

[仮定1]　　　[A]	仮定2 　　B
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A
				∨導入則
(￢A)∨(￢B)

[step7]

[仮定1]　　　[A]	仮定2 　　B
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A
				∨導入則	仮定4
(￢A)∨(￢B)					￢((￢A)∨(￢B))

[step8]

[仮定1]　　　[A]	仮定2 　　B
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A
				∨導入則	仮定4
(￢A)∨(￢B)					￢((￢A)∨(￢B))
						￢除去
⋏

[step9]

[仮定1]　　　[A]	[仮定2] 　　[B]
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A
				∨導入則	仮定4
(￢A)∨(￢B)					￢((￢A)∨(￢B))
						￢除去
⋏
						￢導入仮定2を解消
￢B

　→　ド・モルガン則
　→　自然演繹の定理一覧
　→　論理記号一覧　
　→　総目次　　

[step10]

[仮定1]　　　[A]	[仮定2] 　　[B]
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A
				∨導入則	仮定4
(￢A)∨(￢B)					￢((￢A)∨(￢B))
						￢除去
⋏
						￢導入仮定2を解消
￢B
						∨導入則
(￢A)∨(￢B)

[step11]

[仮定1]　　　[A]	[仮定2] 　　[B]
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A
				∨導入則	仮定4
(￢A)∨(￢B)					￢((￢A)∨(￢B))
						￢除去
⋏
						￢導入仮定2を解消
￢B
						∨導入則	仮定4
(￢A)∨(￢B)							￢((￢A)∨(￢B))

[step12]

[仮定1]　　　[A]	[仮定2] 　　[B]
		∧導入	仮定3
A∧B			￢(A∧B)
				￢除去
⋏
				￢導入仮定1を解消
￢A
				∨導入則	仮定4
(￢A)∨(￢B)					￢((￢A)∨(￢B))
						￢除去
⋏
						￢導入仮定2を解消
￢B
						∨導入則	仮定4
(￢A)∨(￢B)							￢((￢A)∨(￢B))
								￢除去
⋏