論理的思考法/演習問題

提供: Internet Web School

(版間での差分)
 
(間の2版分が非表示)
1 行: 1 行:
'''演繹推論'''　
'''演繹推論'''　
-
以下の記述は何を証明している解読すること
+
以下の記述は何を証明しているか解読すること
 +
 
 +
<pre>
 +
environ
 +
 
 +
vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
 +
      RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4,
 +
      TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0,
 +
      UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
 +
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS,
 +
      XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1,
 +
      FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1,
 +
      TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
 +
constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1,
 +
      BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1;
 +
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0,
 +
      XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1,
 +
      XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY,
 +
      XREAL_0, RVSUM_1;
 +
requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
 +
definitions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0,
 +
    PRE_POLY,FINSET_1,CARD_1;
 +
theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1,
 +
      INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1,
 +
      FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1,
 +
      FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2,
 +
      FINSET_1,PARTFUN1, PRE_POLY, CARD_1;
 +
schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1;
 +
 
 +
begin
 +
 
 +
 
 +
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;
 +
 
 +
</pre>
-
[[ファイル:MIZ1.jpg|800px]]
 

2020年12月3日 (木) 09:21 時点における最新版

演繹推論　

以下の記述は何を証明しているか解読すること 

environ

 vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
      RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4,
      TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0,
      UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS,
      XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1,
      TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
 constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1,
      BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0,
      XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1,
      XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY,
      XREAL_0, RVSUM_1;
 requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
 definitions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0, 
    PRE_POLY,FINSET_1,CARD_1;
 theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1,
      INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1,
      FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1,
      FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2,
      FINSET_1,PARTFUN1, PRE_POLY, CARD_1;
 schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1;

begin


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%BF%92%E5%95%8F%E9%A1%8C」より作成
個人用ツール