Loading [MathJax]/jax/output/HTML-CSS/fonts/TeX/fontdata.js

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

提供: Internet Web School

(版間での差分)
(演繹定理)
(演繹定理の応用)
 
(間の39版分が非表示)
82 行: 82 行:
-
<pre>
+
<pre style="font-size:large">
environ
environ
237 行: 237 行:
=公理系と推論=
=公理系と推論=
-
=論理式=
+
==論理式==
「真」とする複数の命題から論理的操作をして,「真」である命題を導き出す演繹推論は代数的演算のような扱いができる.  
「真」とする複数の命題から論理的操作をして,「真」である命題を導き出す演繹推論は代数的演算のような扱いができる.  
243 行: 243 行:
「命題」をそれが何を主張しているかを意味を考えずに,それが「真」か「偽」であるかどうかだけを考えれば,命題は
「命題」をそれが何を主張しているかを意味を考えずに,それが「真」か「偽」であるかどうかだけを考えれば,命題は
-
代数の演算での変数とみなすことができる. これを命題変数と呼ぶ.
+
代数的な演算の変数とみなすことができる. これを命題変数と呼ぶ.
命題の「真」,「偽」はその変数の値あるいは定数のように扱うことができる.
命題の「真」,「偽」はその変数の値あるいは定数のように扱うことができる.
257 行: 257 行:
-
* および は命題論理における論理式である。
+
* および は論理式である。
-
* 個々の命題変数は命題論理における論理式である。
+
* 個々の命題変数は論理式である。
* A が論理式ならば、¬A も論理式である。
* A が論理式ならば、¬A も論理式である。
281 行: 281 行:
式を{\gt 恒真論理式}(tautology)という。
式を{\gt 恒真論理式}(tautology)という。
-
=命題論理の公理系=
+
==公理系==
公理系と呼ばれる L の部分集合 A と推論規則が適当に定めら
公理系と呼ばれる L の部分集合 A と推論規則が適当に定めら
291 行: 291 行:
以下、A,B,C は任意の L の要素とする。
以下、A,B,C は任意の L の要素とする。
-
{\gt 公理系 A} として、次の (1)(15) をとる。
+
'''公理系 A''' として、次の (1)(15) をとる。
# AA
# AA
330 行: 330 行:
* 以上によって定まるものだけが、証明可能な論理式である。
* 以上によって定まるものだけが、証明可能な論理式である。
-
=演繹定理=
+
==推論法則==
証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば
証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば
363 行: 363 行:
上で便利な手続きをまとめたもの。)
上で便利な手続きをまとめたもの。)
-
**[例]
+
'''推論法則'''
-
$
+
*$
\frac{\cal A }{\cal B \Rightarrow  A}
\frac{\cal A }{\cal B \Rightarrow  A}
\qquad (推論法則:添加)
\qquad (推論法則:添加)
372 行: 372 行:
証明可能な論理式であることを表す。 (上の「証明」の例に現れている。)
証明可能な論理式であることを表す。 (上の「証明」の例に現れている。)
-
$
+
*$
\frac{\cal A,B }{\cal A \land B}
\frac{\cal A,B }{\cal A \land B}
\qquad (推論法則:論理積)
\qquad (推論法則:論理積)
412 行: 412 行:
は証明可能な論理式である。
は証明可能な論理式である。
 +
またこれから直ちに
またこれから直ちに
-
$
+
 
 +
*$
\frac{\cal A \land B }{\cal B \land A}
\frac{\cal A \land B }{\cal B \land A}
\qquad (推論法則:交換)
\qquad (推論法則:交換)
422 行: 424 行:
同様に
同様に
-
$
+
 
 +
*$
\frac{\cal A \lor B }{\cal B \lor A}
\frac{\cal A \lor B }{\cal B \lor A}
\qquad (推論法則:交換)
\qquad (推論法則:交換)
429 行: 432 行:
も得られる。さらに
も得られる。さらに
-
$
+
 
 +
*$
\cal A \Rightarrow \lnot \lnot A,\lnot \lnot A \Rightarrow A
\cal A \Rightarrow \lnot \lnot A,\lnot \lnot A \Rightarrow A
-
「2重否定」
+
(推論法則:2重否定)
$
$
も得られる。
も得られる。
-
$
+
 
 +
*$
\frac{ \cal A \Rightarrow  B ,B \Rightarrow C  }
\frac{ \cal A \Rightarrow  B ,B \Rightarrow C  }
{\cal A \Rightarrow  C}(推論法則:推移)
{\cal A \Rightarrow  C}(推論法則:推移)
477 行: 482 行:
同様に
同様に
-
$
+
 
 +
*$
\frac{ \cal A \Rightarrow  (B \Rightarrow C) ,A \Rightarrow B  }
\frac{ \cal A \Rightarrow  (B \Rightarrow C) ,A \Rightarrow B  }
{\cal A \Rightarrow  C} (推論法則:復推移)
{\cal A \Rightarrow  C} (推論法則:復推移)
483 行: 489 行:
が得られる。これはまず、(8)から
が得られる。これはまず、(8)から
 +
$
$
516 行: 523 行:
が得られることで示される。
が得られることで示される。
-
上述の体系を H と呼ぶことにしよう。(H={\bf A}+
+
==演繹定理==
 +
 
 +
 
 +
 
 +
===演繹定理===
 +
前述の公理系と推論規則のセットを H と呼ぶことにしよう。(H={\bf A}+
Lの論理式 A が証明
Lの論理式 A が証明
541 行: 553 行:
Hは省略することにする。
Hは省略することにする。
 +
 +
'''[演繹定理]'''
上の体系Hについてその公理系Aに論理式
上の体系Hについてその公理系Aに論理式
563 行: 577 行:
また、これを繰り返せば
また、これを繰り返せば
 +
$
$
569 行: 584 行:
$
$
-
+
 
 +
 
 +
 
 +
'''[演繹定理の証明]'''
 +
 
体系Hについてその公理系Aに論理式
体系Hについてその公理系Aに論理式
577 行: 596 行:
$
$
-
を追加してできる新たな系をH1で表し、
+
を追加してできる新たな系をH1で表わす.
-
体系Hについてその公理系Aに論理式
+
-
$
 
-
{\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}
 
-
$
 
-
を追加してできる系をH2で表す。
 
$
$
590 行: 604 行:
$
$
-
+
ならば
$
$
596 行: 610 行:
$
$
-
であることを表している。示すべきことは
+
である.
 +
 
 +
 
 +
 
 +
 
 +
 
 +
体系Hについてその公理系Aに論理式
 +
 
 +
$
 +
{\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}
 +
$
 +
 
 +
を追加してできる系をH2で表す。
 +
 
 +
 
 +
 
 +
示すべきことは
$
$
667 行: 697 行:
を適用すると
を適用すると
AnBiが得られる。
AnBiが得られる。
-
 
 
-
==演繹定の応用==
 
-
$
+
===演繹定理の応用===
-
{\cal \lnot A}\vdash_H \bot
+
-
$
+
-
のとき
 
-
$
+
 
-
\vdash_H \cal A
+
*¬AHのとき $ \vdash_H \cal A $
-
$
+
 
これは、まず
これは、まず
686 行: 711 行:
$
$
-
から
+
から演繹定理により
 +
$
 +
\vdash_H \cal \lnot A \Rightarrow \bot
 +
$
 +
 
 +
これと公理(14)から
$
$
712 行: 742 行:
が成り立っている。これらより結局
が成り立っている。これらより結局
-
 
$
$
724 行: 753 行:
\frac{\cal \lnot A \Rightarrow \bot }{\cal A}
\frac{\cal \lnot A \Rightarrow \bot }{\cal A}
$
$
 +
また論理式の形で表せば
また論理式の形で表せば
733 行: 763 行:
である。(いずれもHが省略されていることに注意)
である。(いずれもHが省略されていることに注意)
-
$
+
 
 +
*$
\frac{\cal A \Rightarrow B}{\cal \lnot B \rightarrow \lnot A}
\frac{\cal A \Rightarrow B}{\cal \lnot B \rightarrow \lnot A}
(「対偶」)
(「対偶」)
751 行: 782 行:
体系 H については、次の事実が知られている:
体系 H については、次の事実が知られている:
-
%%
+
 
-
%%
+
 
-
*定理8
+
*'''命題計算の体系についての完全性定理'''
 +
 
 +
 
A が恒真論理式であることの必要十分条件は、HA  
A が恒真論理式であることの必要十分条件は、HA  
が成立することである。
が成立することである。
-
この定理は、命題計算の体系についての{\gt 完全性定理}(completeness  
+
この定理は、'''命題計算の体系についての完全性定理'''(completeness  
theorem)と呼ばれるものである。
theorem)と呼ばれるものである。
-
*[定理8の証明]\mbox{}
+
*[証明]
 +
 
まず、HAが成立すればAが恒真論理式であることを示そう。
まず、HAが成立すればAが恒真論理式であることを示そう。
774 行: 808 行:
    
    
    
    
-
* 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式
+
* 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式3
であるからAiは恒真論理式である。
であるからAiは恒真論理式である。
781 行: 815 行:
形をしている。
形をしている。
iより前の論理式は恒真論理式であると仮定すると、
iより前の論理式は恒真論理式であると仮定すると、
-
Ajと${\cal A}_k$AjAiは真理値しかとらないから真理値表
+
Ajと${\cal A}_j \Rightarrow {\cal A}_i$は真理値しかとらないから真理値表
 +
 
 +
 
 +
 
 +
{| border="3" class="wikitable"
 +
||Aj
 +
|Ai
 +
|AjAi
 +
|-
 +
|
 +
|
 +
|  
 +
|-
 +
|
 +
|  
 +
|
 +
|-
 +
|
 +
|
 +
|
 +
|-
 +
|
 +
|
 +
|
 +
|}
 +
 
-
\begin{tabular}{|c c||c|}
 
-
\hline
 
-
Aj & Ai & AjAi \\
 
-
\hline
 
-
& & \\
 
-
\hline
 
-
& & \\
 
-
\hline
 
-
& & \\
 
-
\hline
 
-
& & \\
 
-
\hline
 
-
\end{tabular}
 
から明らかなようにAiの真理値はしか取り得ない。
から明らかなようにAiの真理値はしか取り得ない。
803 行: 849 行:
逆にAが恒真論理式であるときに、
逆にAが恒真論理式であるときに、
HAが成立することをいうには次の補題1が必要になる。
HAが成立することをいうには次の補題1が必要になる。
-
*[補題1]
+
*[補題]
Aが命題変数X1,X2,,Xnから構成される論理式とする。
Aが命題変数X1,X2,,Xnから構成される論理式とする。
820 行: 866 行:
である。ただし、δXiXiに対する真理値のふり当てがの場合Xiの場合は¬Xiとする。
である。ただし、δXiXiに対する真理値のふり当てがの場合Xiの場合は¬Xiとする。
-
*[定理8の証明の続き]
+
*[定理の証明の続き]
恒真論理式Aが命題変数X1,X2,,Xnから構成されるものとする。
恒真論理式Aが命題変数X1,X2,,Xnから構成されるものとする。
865 行: 911 行:
を得る。
を得る。
-
*[補題1の証明]
+
*[補題の証明]
-
*論理式Aがただ1つの命題変数Xからなるとき
+
**論理式Aがただ1つの命題変数Xからなるとき
    
    
-
Xに対するふり当てがのとき
+
Xに対するふり当てがのときXHX また のとき ¬XH¬X
-
XHX
+
-
 
+
-
のとき  
+
-
¬XH¬X
+
これは公理の(1)から容易に示される。
これは公理の(1)から容易に示される。
-
これ以外の場合は、A¬B,BC,BCの形をして
+
**これ以外の場合は、A¬B,BC,BCの形をしている。
-
いる。この場合、部分式B,Cについては
+
 
-
この補題1が成り立つものとする。
+
そこで論理式の長さについての帰納法を使う.
-
*A¬Bである場合  
+
 
 +
Aより長さの短い部分式B,Cについてはこの補題が成り立つものとする。
 +
 
 +
 
 +
***A¬Bである場合  
 +
 
 +
 
Aの値がのときBの値はであるから
Aの値がのときBの値はであるから
890 行: 938 行:
B,¬BはそれぞれA及び¬Aである。
B,¬BはそれぞれA及び¬Aである。
      
      
-
*ABCである場合  
+
***ABCである場合  
Aの値がのときB,Cの少なくともどちらか一方の値は
Aの値がのときB,Cの少なくともどちらか一方の値は
927 行: 975 行:
-
*ABCである場合  
+
***ABCである場合  
 +
 
Aの値がのときB,Cの値はともにでなければならない。
Aの値がのときB,Cの値はともにでなければならない。

2020年12月1日 (火) 01:33 時点における最新版

目次

[非表示]

演繹推論

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


簡単な例を挙げる。

  • (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万人+1人である.

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

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

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

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


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


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

この過程(証明)は,その論証の過程に出てくる命題やそれに施す論理的な推論を計算機によって処理できる形式化された記述で書けば,計算機によってその正しさを検証できる.それを形式化を行うかどうかは別として計算機による検証で正しさが認められるものでなければ完全な演繹推論とは言えない.


実際,以下は定理証明支援系のMizarによって上記の推論を記述したものである. Mizarのような定理証明支援系あるいは形式化証明検証システムでは,命題は全て記号列であり,三段論法その他の推論規則はそれらの複数の記号列を操作して 別の新たな記号列を構成する規則に過ぎない.証明は,前提となる命題(記号列)から出発して,目的の命題(記号列)に至る,推論規則により 生成された記号列の列にに過ぎない.


特に,A.I. や ICTの進歩など数学を含む科学技術の進歩の激流の中にある,科学工学の技術者はMizarのようなシステムの操作にも慣れ親しむことが必要になってくる.


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;
   

公理系と推論

論理式

「真」とする複数の命題から論理的操作をして,「真」である命題を導き出す演繹推論は代数的演算のような扱いができる.

ここでは,そのような扱いを「命題論理」によって説明する.

「命題」をそれが何を主張しているかを意味を考えずに,それが「真」か「偽」であるかどうかだけを考えれば,命題は 代数的な演算の変数とみなすことができる. これを命題変数と呼ぶ.

命題の「真」,「偽」はその変数の値あるいは定数のように扱うことができる.


その上で,一つの命題に,あるいは命題と命題をつなぐ「~でない」 「かつ」 「または」 「ならば」 などを命題を表す命題変数に作用する演算子とみなすことにする. それらをそれぞれ および  ¬,,,で表す.

命題変数にこれらの演算子を作用させたものを論理式と呼ぶ.

論理式はこれを以下のように再帰的に定義する.


  • および は論理式である。
  • 個々の命題変数は論理式である。
  • A が論理式ならば、¬A も論理式である。
  • A,B が論理式ならば、

AB,AB,AB は、いずれも論理式である。

  • 以上によって定まるものみが論理式である。


論理式の全体を L と書くことにしよう。

L の要素である論理式は、いずれもその論理式を表現としてもつ真理 関数と考えられる。任意の真理関数は、その独立変数がとり得る値のとり方 (n 変数ならば 2n 通り)の各々の場合について、有限回の操作でその 値(関数値)を決定できる。

L の論理式の値(真理関数とみなした場合の関数値)が、(命題変数の 値のとり方のすべてに対して)つねに であるとき、そのような論理 式を{\gt 恒真論理式}(tautology)という。

公理系

公理系と呼ばれる L の部分集合 A と推論規則が適当に定めら れ、恒真論理式が A から推論規則によって導けるような体系を、 命題論理の公理的体系、あるいは命題計算の体系という。

いろいろな公理的体系が知られているが、ここではヒルベルト(D. Hilbert) 流のものを挙げておこう。

以下、A,B,C は任意の L の要素とする。 公理系 A として、次の (1)(15) をとる。

  1. AA
  2. (AB)[(BC)(AC)]
  3. A(AB)
  4. B(AB)
  5. (AC){(BC)[(AB)C]}
  6. (AB)A
  7. (AB)B
  8. (CA){(CB)[C(AB)]}
  9. [A(AB)]B
  10. [(AC)B][C(AB)]
  11. (A¬A)
  12. [(AB)](B¬A)
  13. A
  14. A
  15. A¬A

推論規則は、次の三段論法(modus ponens)のみである。横線の上の論 理式から下の論理式が導かれることを表わす。

AABB

証明可能性を定義する。すなわち、L の要素である論理式のうち、 証明可能な論理式(provable formula)を次のように定める:

  • 公理系の各公理の形の論理式は証明可能である。
  • 論理式 A と論理式 AB が証明可能ならば、(推論規則によって、)論理式 B は証明可能である。
  • 以上によって定まるものだけが、証明可能な論理式である。

推論法則

証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば

A1,A2,,An が「証明」のとき各Ai

  • 公理系の各公理の形の論理式である。
  • 論理式Aiの前に論理式AjAk(j,k<i)がありAkAjAiの形をしている。


例えば、

BAA,(BAA)(A(BA)),A(BA)

もっと具体的には

1=22>62>6(1=22>62>6)(2>6(1=22>6))2>6(1=22>6)

は証明である。(証明可能な論理式を「定理」とか「命題」と呼ぶこともある。)

「証明」の中で推論規則と公理を何回か適用する共通した手順を「推論法則」 と呼ぶ。(これ自身は公理系を定義するのに必須ではないが、それを操作する 上で便利な手続きをまとめたもの。)

推論法則

  • ABA()

Aが証明可能な論理式ならばBAも 証明可能な論理式であることを表す。 (上の「証明」の例に現れている。)

  • A,BAB()

任意の論理式Cを用いて「添加」により

(C¬C)A,(C¬C)B

が得られる。また(8)であるから

{(C¬C)A}[{(C¬C)B}{(C¬C)(AB)}]

推論規則により、

(C¬C)(AB)

が得られる。ところで(15)により

C¬C

は公理(当然証明可能な論理式であるから) 結局

AB

は証明可能な論理式である。

またこれから直ちに


  • ABBA()

が得られる。 同様に


  • ABBA()

も得られる。さらに


  • A¬¬A,¬¬AA()

も得られる。


  • AB,BCAC()

これは(2)より

(AB)[(BC)(AC)]

が得られ、これと

AB

から推論規則により、

(BC)(AC)

を得る。さらにこれと

BC

とから

AC

が得られることで示される。 %% %% 同様に


  • A(BC),ABAC ()

が得られる。これはまず、(8)から


(AB)[{A(BC)}{AB(BC)}]

これと

A(BC),AB

から

A{B(BC)}

が得られ さらに(9)

{B(BC)}C

と前述の「推移」により

AC

が得られることで示される。

演繹定理

演繹定理

前述の公理系と推論規則のセットを H と呼ぶことにしよう。(H={\bf A}+

Lの論理式 A が証明 可能であるとは、H において、公理系 A から A が推論規 則によって導けることであるから、これを

HA

と書く。推論規則

AABB

はこの表記法を用いると、

HAHABHB

と書くべきである。しかし、どの系で証明可能なのか明らかな場合は Hは省略することにする。


[演繹定理] 上の体系Hについてその公理系Aに論理式

A1,A2,,An

を追加してできる新たな系で 論理式Bが証明可能であるとき、このことを

A1,A2,,AnHB

で表す。さらにこのとき:

A1,A2,,An1HAnB

が成り立つ。

また、これを繰り返せば


A1,A2,,An2HAn1(AnB)



[演繹定理の証明]


体系Hについてその公理系Aに論理式

A1,A2,,An

を追加してできる新たな系をH1で表わす.


A1,A2,,AnHB

ならば

H1B

である.



体系Hについてその公理系Aに論理式

A1,A2,,An1

を追加してできる系をH2で表す。


示すべきことは

H2AnB

である。

B1,B2,,Bn1,Bn(=B)

H1での「証明」とするとき、定義より 各Biは次のいずれかである。


  • BiA1,A2,,Anのうち1つで

ある。

  • Biは公理系Hの各公理の形の論理式である。
  • 論理式 Bi の前に論理式 BjBk

(j,k<i)があり、BkBjBi の 形をしている。


そして、

AnB1,AnB2,,AnBn1,AnBn

H2でのAnBを含む「証明」になる。



  • BiA1,A2,,An1のうち1つであれば、「添加」

ABA()

により、 AnBiH2で証明可能な論理式になる。

BiAn自身ならば、公理(1) により、 AnAnH2で証明可能な論理式である。

  • Biが公理系Hの各公理の形の論理式であるとき、

同様に「添加」により、 AnBiH2で証明可能な論理式である。

  • 論理式 Bi の前に論理式 BjBk

(j,k<i)があり、BkBjBi の 形をしているときは、 AnBiの前に、

AnBjAn(BjBi)とがあることになる。

これに「複推移」

A(BC),ABAC ()

を適用すると AnBiが得られる。

演繹定理の応用

  • ¬AHのとき HA


これは、まず

¬AH

から演繹定理により H¬A

これと公理(14)から

H¬AA

となる。さらに(1)により、

AA

(8)から

(¬AA)[(AA){(A¬A)A}]

が得られる。また、(15)により

A¬A

が成り立っている。これらより結局

HA

上の結果を推論規則の形で表現すれば

¬AA


また論理式の形で表せば

(¬A)A

である。(いずれもHが省略されていることに注意)


  • AB¬B¬A()

まず、

HAB

を仮定する。系H¬Bを追加して得られる系をH1とする。 さらにこれに¬Aの否定¬¬Aを追加した系をH2と すると、2重否定により、H2Aが、従って H2Bが得られる。このことから H2となり、結局H1¬B¬Aが得られる。

体系 H については、次の事実が知られている:


  • 命題計算の体系についての完全性定理


A が恒真論理式であることの必要十分条件は、HA が成立することである。

この定理は、命題計算の体系についての完全性定理(completeness theorem)と呼ばれるものである。

  • [証明]

まず、HAが成立すればAが恒真論理式であることを示そう。

HAが成り立つとすると;

Hの「証明」である論理式の列

A1,A2,,An

があって、Aは最後のAnと一致しているものとしてよい。 各Ai


  • 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式3

であるからAiは恒真論理式である。

  • 論理式 Ai の前に論理式 AjAk

(j,k<i)があり、AkAjAi の 形をしている。 iより前の論理式は恒真論理式であると仮定すると、 AjAjAiは真理値しかとらないから真理値表


Aj Ai AjAi


から明らかなようにAiの真理値はしか取り得ない。 すなわちAiは恒真論理式である。


逆にAが恒真論理式であるときに、 HAが成立することをいうには次の補題1が必要になる。

  • [補題]

Aが命題変数X1,X2,,Xnから構成される論理式とする。 命題変数X1,X2,,Xnに真理値,をふり当て、そのふり当てに対しAの真理値がである場合

δX1,δX2,δXnHA

Aの真理値がである場合

δX1,δX2,δXnH¬A

である。ただし、δXiXiに対する真理値のふり当てがの場合Xiの場合は¬Xiとする。

  • [定理の証明の続き]

恒真論理式Aが命題変数X1,X2,,Xnから構成されるものとする。 する。 命題変数X1,X2,,Xnに真理値,どのようにふり当ても、 Aの真理値は常にである。

命題変数X1,X2,,Xnに真理値,どのようにふり当てるしかたは 2n通りある。これを辞書式順序で全て列挙し[補題1]を適用すると


X1,X2,,XnHAX1,X2,,¬XnHAX1,X2,,¬Xn1,XnHAX1,X2,,¬Xn1,¬XnHA¬X1,¬X2,,¬XnHA


が得られる。最初の2式から演繹定理により

X1,X2,,Xn1XnAX1,X2,,Xn1¬XnA

これから

X1,X2,,Xn1HA

が得られる。すなわちXnが消去された。同様にして順次に2式ずつ 同じ手順を繰り返せば、Xnが消去された2n1個の式を得る。この 2n1個の式からXn1を2式ずつをとり同じ手順を繰り返すとXn1が 消去された2n2個の式を得る。 この手順を繰り返せば変数X1,X2,,Xnが全て消去され、結局

HA

を得る。

  • [補題の証明]
    • 論理式Aがただ1つの命題変数Xからなるとき

     Xに対するふり当てがのときXHX また のとき ¬XH¬X これは公理の(1)から容易に示される。

    • これ以外の場合は、A¬B,BC,BCの形をしている。

そこで論理式の長さについての帰納法を使う.

Aより長さの短い部分式B,Cについてはこの補題が成り立つものとする。


      • A¬Bである場合


Aの値がのときBの値はであるから

δX1,δX2,,δXnH¬B

Aの値がのときBの値はであるから

δX1,δX2,,δXnHB

B,¬BはそれぞれA及び¬Aである。

      • ABCである場合

Aの値がのときB,Cの少なくともどちらか一方の値は であるから、Bの値がとしても一般性を失わない。このとき

δX1,δX2,,δXnHB

が成り立っている。これと公理の(3)

BBC

により δX1,δX2,,δXnHBC

BCAに他ならない。

Aの値がのときB,Cの値はともにでなければならない。 このとき δX1,δX2,,δXnH¬B

δX1,δX2,,δXnH¬C

これに推論法則の「論理積」

P,QPQ

を用いて

δX1,δX2,,δXnH¬B ¬C を得る。

¬B¬C¬A(=¬(BC))に他ならない。


      • ABCである場合


Aの値がのときB,Cの値はともにでなければならない。 このとき

δX1,δX2,,δXnHB

δX1,δX2,,δXnHC

これに推論法則の「論理積」

P,QPQ

を用いて δX1,δX2,,δXnHB C を得る。 BCAに他ならない。

Aの値がのときB,Cの少なくともどちらか一方の値は であるから、Bの値がとしても一般性を失わない。このとき

δX1,δX2,,δXnH¬B

が成り立っている。これと公理の(3)

PPQ

により

δX1,δX2,,δXnH¬B¬C

¬B¬C¬A=¬(BC)に他ならない。