論理的思考法/演繹的推論

提供: Internet Web School

2020年11月28日 (土) 11:16時点における版 (ソースを表示) Moderator (トーク | 投稿記録) ←前の差分		2020年11月28日 (土) 11:41時点における版 (ソースを表示) Moderator (トーク | 投稿記録) 次の差分→
73 行:		73 行:
-		+	[[ファイル:MIZ1.jpg]]
-		+
-	now	+
-	let	+
-	Humankind be finite set,	+
-	Tokyoite be Subset of  Humankind,	+
-	Numberofhair be  Function of Tokyoite,NAT ;	+
-		+
-		+
-	assume  LM1:	+
-	card (Tokyoite) = 12*10|^6;	+
-	assume  LM2:	+
-	for x be object	+
-	st x in Tokyoite	+
-	holds Numberofhair.x <= 10|^6;	+
-		+
-		+
-	LM0:	+
-	10|^6 + 1 < 12*10|^6	+
-	proof	+
-	0 < 10|^6 by PREPOWER:6;	+
-	then	+
-	P2: 1*10|^6 < 11* 10|^6 by XREAL_1:68;	+
-	P3: 1 <  10 & 2 <= 6;	+
-	then	+
-	10 < 10 |^6 by PREPOWER:13;	+
-	then	+
-	1 < 10 |^6 by XXREAL_0:2,P3;	+
-	then	+
-	1 < 11*10|^6 by P2,XXREAL_0:2;	+
-	then	+
-	P4: 1*10|^6 + 1 < 1*10|^6 + 11*10|^6 by XREAL_1:8;	+
-	1*10|^6 + 11*10|^6 = (1+11)*10|^6  ;	+
-	hence thesis by P4;	+
-	end;	+
-		+
-		+
-	LM3:	+
-	card (rng Numberofhair) <= 10|^6+1	+
-	proof	+
-	now let y be  object ;	+
-	assume	+
-	y in  rng Numberofhair;	+
-	then	+
-	consider  x be object	+
-	such that	+
-	A1: x in Tokyoite & y=Numberofhair.x  by FUNCT_2:11;	+
-	Numberofhair.x <= 10|^6 by A1,LM2;	+
-	then	+
-	Numberofhair.x < 10|^6+1 by NAT_1:16,XXREAL_0:2;	+
-	then	+
-	Numberofhair.x  in Segm (10|^6+1) by NAT_1:44,A1;	+
-	hence	+
-	y in Segm (10|^6+1) by A1;	+
-	end;	+
-	then	+
-	A2: rng Numberofhair	+
-	c= Segm (10|^6+1) by TARSKI:def 3;	+
-	then	+
-	card rng Numberofhair <= card Segm (10|^6+1) by NAT_1:43;	+
-	then	+
-	card rng Numberofhair <= card (10|^6+1) by ORDINAL1:def 17;	+
-	hence	+
-	card rng Numberofhair <= (10|^6+1)  ;	+
-	end;	+
-		+
-	LM4:	+
-	card (rng (Numberofhair))	+
-	< card  (Tokyoite)	+
-	proof	+
-	reconsider N1= card (rng (Numberofhair))	+
-	as Element of NAT ;	+
-	reconsider N2= card (Tokyoite)	+
-	as Element of NAT ;	+
-	A1: N1<=(10|^6+1) & N2=12*10|^6 by LM1,LM3;	+
-	then	+
-	N1 < N2 by A1,XXREAL_0:2,LM0;	+
-	hence thesis ;	+
-	end;	+
-		+
-		+
-	EX:	+
-	ex x,y be object	+
-	st x in Tokyoite	+
-	& y in Tokyoite	+
-	& x <> y	+
-	& Numberofhair.x = Numberofhair.y	+
-		+
-	proof	+
-	assume	+
-	A1:	+
-	not	+
-	(  ex x,y be object	+
-	st x in Tokyoite	+
-	& y in Tokyoite	+
-	& x <> y	+
-	& Numberofhair.x = Numberofhair.y ) ;	+
-		+
-	then	+
-	A2:  for x,y be object	+
-	st x in Tokyoite	+
-	& y in Tokyoite	+
-	& x <> y	+
-	holds	+
-	Numberofhair.x <> Numberofhair.y  ;	+
-		+
-	A3: dom Numberofhair = Tokyoite by FUNCT_2:def 1;	+
-	then	+
-	for x,y be object st x in dom Numberofhair	+
-	& y in dom Numberofhair	+
-	& Numberofhair.x = Numberofhair.y	+
-	holds x = y by A2;	+
-	then	+
-	Numberofhair is oneqto-one by FUNCT_1:def 4;	+
-	then	+
-	card  (dom Numberofhair) = card (rng Numberofhair)	+
-	by CARD_1:70;	+
-	then	+
-	card  (Tokyoite) = card (rng (Numberofhair))	+
-	by A3;	+
-	hence contradiction by LM4;	+
-	end;	+
-	end;	+

---

2020年11月28日 (土) 11:41時点における版

演繹的推論は論理的思考の根幹である.

簡単な例を挙げる。

• (1)人間の髪の毛の本数は100万本以下である.
• (2)東京都民の人口は1200万人である.

これらの命題が正しければ

• (3)東京都民のうち少なくとも2人は髪の毛の本数は同じである.

この命題の正しさを示すには背理法による.

命題(3)の否定が成り立つものとする。

命題(3)は厳密に書くと

　「東京都民A,Bがいて,A,Bは同一人物でなくかつA,Bの髪の毛の本数は同じ」

である．

このこの命題の否定は

• (4)任意の東京都民A,Bについて,A,Bが同一人物でなければ　A,Bの髪の毛の本数は等しくない．

である.

ここでは(4)が正しいと仮定している．

東京都民一人一人にその人自身の髪の毛の本数によって背番号を振ることを考える. 例え ば毛の本数が0本の人には背番号0を，1000本の人には背番号1000を振る。

都民全員に付与した背番号は(4)の仮定により誰一人として同じものはなく, 一人一人に唯一の背番号が振られる.

「(1)人間の髪の毛の本数は100万本以下である.」が正しいとしているから 振られる番号は0番から100万まででの100万+1通りである.

都民全員に付与した背番号はそれぞれに唯一であるから 都民全員の数は100万人+１人である.

しかしこれは「(2)東京都民の人口は1200万人である.」に矛盾する.

この矛盾は 命題「東京都民のうち少なくとも2人は髪の毛の本数は同じである.」

の否定が成り立つとしたことによっている.

従って東京都民のうち少なくとも2人は髪の毛の本数は同じである.」が正しい.

上記の　命題(1),(2)が正しければ命題(3)が正しいことを論証した過程は 論理の連鎖に依っている.命題(3)を否定した命題が正しいとして論理の連鎖を つくり,矛盾を導すことによって命題(3)の正しさを証明した.

演繹推論はこのように,正しいもとして与えられた命題から厳密な論理を 繰り返し適用することによって新たな命題を結論として導き出す.

この過程は,その論証の過程に出てくる命題やそれに施す論理的な推論を 計算機によって処理できる記述で書けば,計算機によってその正しさを検証できる.

実際以下は定理証明支援系のMizarによって上記の推論を記述したものである.