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

提供: Internet Web School

(版間での差分)
69 行: 69 行:
この過程は,その論証の過程に出てくる命題やそれに施す論理的な推論を
この過程は,その論証の過程に出てくる命題やそれに施す論理的な推論を
計算機によって処理できる記述で書けば,計算機によってその正しさを検証できる.
計算機によって処理できる記述で書けば,計算機によってその正しさを検証できる.
 +
 +
実際以下は定理証明支援系の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 one-to-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:06時点における版

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


簡単な例を挙げる。

  • (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 one-to-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;

「http://ja.iwschool.org/wiki/%E8%AB%96%E7%90%86%E7%9A%84%E6%80%9D%E8%80%83%E6%B3%95/%E6%BC%94%E7%B9%B9%E7%9A%84%E6%8E%A8%E8%AB%96」より作成
個人用ツール