命題論理の自然演繹における諸定理:⇒の言い換えの証明(1-2)　[数学についてのwebノート]

命題論理の自然演繹における諸定理【25】⇒の言い換え　の証明(1-2)

【証明】(￢A∨B) ⇒ ( A⇒B ) [前原p.184]

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

　→　⇒の言い換え
　→　自然演繹の定理一覧

[step1]

	仮定1　　　A	仮定2 　　￢B

[step2]

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


	【文献】　・前原『記号論理入門』6章§4(pp.114-115):( A ⇒ B ) ⇔ ( ￢A∨B ) 　　・野矢『論理学』1-2-3-LP-命題論理の諸定理-定理10(a)(b)(p.70);付録-定理10(a)(b)(pp.219-220):二項目とも両方向。

　　　
*　「A⇒B」の言い換え表現一覧　　

[step3]

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

[step4]

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

[step5]

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

[step6]

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

[step7]

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

[step8]

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

[step9]

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

　→　⇒の言い換え
　→　自然演繹の定理一覧　
　→　論理記号一覧　
　→　総目次　　

　　

[step10]

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

[step11]

	[仮定1]　　　[A]	[仮定2] 　　[￢B]
			(∧導入)
	A∧￢B
			(∧除去)	仮定3
	A			￢A
					(￢除去)		仮定4	仮定5
		⋏					A	B
				(￢導入)仮定2を解消
		￢￢B
				(二重否定除去律)
		B
				(⇒導入)仮定1を解消
		A ⇒ B

[step12]

	[仮定1]　　　[A]	[仮定2] 　　[￢B]
			(∧導入)
	A∧￢B
			(∧除去)	仮定3
	A			￢A
					(￢除去)		仮定4	仮定5
		⋏					A	B
				(￢導入)仮定2を解消					(∧導入)
		￢￢B					A∧￢B
				(二重否定除去律)
		B
				(⇒導入)仮定1を解消
		A ⇒ B

[step13]

	[仮定1]　　　[A]	[仮定2] 　　[￢B]
			(∧導入)
	A∧￢B
			(∧除去)	仮定3
	A			￢A
					(￢除去)		仮定4	仮定5
		⋏					A	B
				(￢導入)仮定2を解消					(∧導入)
		￢￢B					A∧B
				(二重否定除去律)					(∧除去)
		B					B
				(⇒導入)仮定1を解消
		A ⇒ B

　→　⇒の言い換え
　→　自然演繹の定理一覧
　→　論理記号一覧　
　→　総目次　　

　　

[step14]

	[仮定1]　　　[A]	[仮定2] 　　[￢B]
			(∧導入)
	A∧￢B
			(∧除去)	仮定3
	A			￢A
					(￢除去)		[仮定4]	仮定5
		⋏					[A]	B
				(￢導入)仮定2を解消					(∧導入)
		￢￢B					A∧B
				(二重否定除去律)					(∧除去)
		B					B
				(⇒導入)仮定1を解消					(⇒導入)仮定4を解消
		A ⇒ B					A ⇒ B

[step15]

		[仮定1]　　　[A]	[仮定2] 　　[￢B]
				(∧導入)
		A∧￢B
				(∧除去)	仮定3
		A			￢A
						(￢除去)		[仮定4]	仮定5
			⋏					[A]	B
					(￢導入)仮定2を解消					(∧導入)
			￢￢B					A∧B
					(二重否定除去律)					(∧除去)
			B					B
	仮定6				(⇒導入)仮定1を解消					(⇒導入)仮定4を解消
	￢A∨B		A ⇒ B					A ⇒ B

[step16]

		[仮定1]　　　[A]	[仮定2] 　　[￢B]
				(∧導入)
		A∧￢B
				(∧除去)	[仮定3]
		A			[￢A]
						(￢除去)		[仮定4]	[仮定5]
			⋏					[A]	[B]
					(￢導入)仮定2を解消					(∧導入)
			￢￢B					A∧B
					(二重否定除去律)					(∧除去)
			B					B
	仮定6				(⇒導入)仮定1を解消					(⇒導入)仮定4を解消
	￢A∨B		A ⇒ B					A ⇒ B
										(∨除去)仮定3,仮定5を解消
			A ⇒ B

　→　⇒の言い換え
　→　自然演繹の定理一覧
　→　論理記号一覧　
　→　総目次　　

[step17]

		[仮定1]　　　[A]	[仮定2] 　　[￢B]
				(∧導入)
		A∧￢B
				(∧除去)	[仮定3]
		A			[￢A]
						(￢除去)		[仮定4]	[仮定5]
			⋏					[A]	[B]
					(￢導入)仮定2を解消					(∧導入)
			￢￢B					A∧B
					(二重否定除去律)					(∧除去)
			B					B
	[仮定6]				(⇒導入)仮定1を解消					(⇒導入)仮定4を解消
	[￢A∨B]		A ⇒ B					A ⇒ B
										(∨除去)仮定3,仮定5を解消
			A ⇒ B
										(⇒導入)仮定6を解消
			( ￢A∨B ) ⇒ ( A ⇒ B )