論理的思考法/演繹的推論
提供: Internet Web School
| 73 行: | 73 行: | ||
| - | + | ||
now | now | ||
| 196 行: | 196 行: | ||
end; | end; | ||
end; | end; | ||
| - | |||
| - | |||
2020年11月28日 (土) 11:16時点における版
演繹的推論は論理的思考の根幹である.
簡単な例を挙げる。
- (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によって上記の推論を記述したものである.
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;
