提供: Internet Web School

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万人+１人である.

しかしこれは「(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;
   

公理系と推論

論理式

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

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

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

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

その上で,一つの命題に,あるいは命題と命題をつなぐ「～でない」　「かつ」　「または」　「ならば」 などを命題を表す命題変数に作用する演算子とみなすことにする. それらをそれぞれ$\top$ および $\bot$　$\neg, \land, \lor, \Rightarrow$で表す.

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

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

• $\top$ および $\bot$ は論理式である。

• 個々の命題変数は論理式である。

• $\cal A$ が論理式ならば、$\neg\cal A$ も論理式である。

• $\cal A,B$ が論理式ならば、

$\cal A \land B, A \lor B, A \Rightarrow B$ は、いずれも論理式である。

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

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

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

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

公理系

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

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

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

1. $\cal A \Rightarrow A$
2. $\cal (A \Rightarrow B) \Rightarrow [(B \Rightarrow C) \Rightarrow (A \Rightarrow C)]$
3. $\cal A \Rightarrow (A \lor B)$
4. $\cal B \Rightarrow (A \lor B)$
5. $\cal (A \Rightarrow C) \Rightarrow \{ (B \Rightarrow C) \Rightarrow [(A \lor B) \Rightarrow C]\}$
6. $\cal (A \land B) \Rightarrow A$
7. $\cal (A \land B) \Rightarrow B$
8. $\cal (C \Rightarrow A) \Rightarrow \{ (C \Rightarrow B) \Rightarrow [C \Rightarrow (A \land B)]\}$
9. $\cal [A \land (A \Rightarrow B)] \Rightarrow B$
10. $\cal [(A \land C) \Rightarrow B] \Rightarrow [C \Rightarrow (A \Rightarrow B)]$
11. $\cal (A \land \neg A) \Rightarrow \bot$
12. $\cal [(A \land B) \Rightarrow \bot ] \Rightarrow (B \Rightarrow \neg A)$
13. $\cal A \Rightarrow \top$
14. $\cal \bot \Rightarrow A$
15. $\cal A \lor \neg A$

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

$ \frac{\cal A \quad A \Rightarrow B}{\cal B} $

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

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

推論法則

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

$ {\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n $ が「証明」のとき各${\cal A}_i$は

• 公理系の各公理の形の論理式である。
• 論理式${\cal A}_i$の前に論理式${\cal A}_j$と$ {\cal A}_k (j,k < i ) $があり${\cal A}_k$は${\cal A}_j \Rightarrow {\cal A}_i $の形をしている。

例えば、

$ \cal B \land \cal A \Rightarrow A , \quad (\cal B \land \cal A \Rightarrow \cal A) \Rightarrow (\cal A \Rightarrow (\cal B \Rightarrow \cal A)), \quad \cal A \Rightarrow (\cal B \Rightarrow \cal A) $

もっと具体的には

$1=2 \land 2> 6 \Rightarrow 2>6 \\ ( 1=2 \land 2>6 \Rightarrow 2>6) \Rightarrow (2>6 \Rightarrow (1=2 \Rightarrow 2>6)) \\ 2>6 \Rightarrow ( 1=2 \Rightarrow 2>6) $

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

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

推論法則

• $ \frac{\cal A }{\cal B \Rightarrow A} \qquad (推論法則：添加) $

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

• $ \frac{\cal A,B }{\cal A \land B} \qquad (推論法則：論理積) $

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

$ \cal (C \lor \lnot C ) \Rightarrow A,(C \lor \lnot C ) \Rightarrow B $

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

$ \cal \{ (C \lor \lnot C) \Rightarrow A \} \Rightarrow [ \{ (C \lor \lnot C) \Rightarrow B \} \Rightarrow \{ (C \lor \lnot C) \Rightarrow (A \land B ) \} ] $

推論規則により、

$ \cal (C \lor \lnot C) \Rightarrow (A \land B ) $

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

$ \cal C \lor \lnot C $

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

$ \cal A \land B $

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

またこれから直ちに

• $ \frac{\cal A \land B }{\cal B \land A} \qquad (推論法則：交換) $

が得られる。 同様に

• $ \frac{\cal A \lor B }{\cal B \lor A} \qquad (推論法則：交換) $

も得られる。さらに

• $ \cal A \Rightarrow \lnot \lnot A,\lnot \lnot A \Rightarrow A (推論法則：２重否定) $

も得られる。

• $ \frac{ \cal A \Rightarrow B ,B \Rightarrow C } {\cal A \Rightarrow C}(推論法則：推移) $

これは$(2)$より

$ \cal (A \Rightarrow B) \Rightarrow [(B \Rightarrow C ) \Rightarrow (A \Rightarrow C) ] $

が得られ、これと

$ \cal A \Rightarrow B $

から推論規則により、

$ \cal (B \Rightarrow C ) \Rightarrow (A \Rightarrow C) $

を得る。さらにこれと

$ \cal B \Rightarrow C $

とから

$ \cal A \Rightarrow C $

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

• $ \frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } {\cal A \Rightarrow C}　(推論法則：復推移) $

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

$ \cal (A \Rightarrow B) \Rightarrow [ \{ A \Rightarrow (B \Rightarrow C) \} \Rightarrow \{A \Rightarrow B \land (B \Rightarrow C) \} ] $

これと

$ {\cal A \Rightarrow (B \Rightarrow C) , A \Rightarrow B} $

から

$ {\cal A \Rightarrow \{ B \land (B \Rightarrow C) \} } $

が得られ さらに$(9)$の

$ {\cal \{B \land (B \Rightarrow C)\} \Rightarrow C } $

と前述の「推移」により

$ \cal A \Rightarrow C $

が得られることで示される。$\Box$

演繹定理

演繹定理

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

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

$ \vdash_H \cal A $

と書く。推論規則

$ \frac{\cal A \quad A \Rightarrow B}{\cal B} $

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

$ \frac{\vdash_H \cal A \quad \vdash_H A \Rightarrow B}{\vdash_H \cal B} $

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

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

$ {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n $

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

$ {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B $

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

$ {\cal A}_1,{\cal A}_2,\cdots,{\cal A} _{n-1} \vdash_H {\cal A}_n \Rightarrow {\cal B} $

が成り立つ。

また、これを繰り返せば

$ {\cal A}_1,{\cal A}_2,\cdots,{\cal A} _{n-2} \vdash_H {\cal A} _{n-1} \Rightarrow ({\cal A}_n \Rightarrow {\cal B}) $

[演繹定理の証明]

体系$H$についてその公理系${\bf A}$に論理式

$ {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n $

を追加してできる新たな系を$H^1$で表わす.

$ {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B $

ならば

$ \vdash_{H^1} \cal B $

である.

体系$H$についてその公理系${\bf A}$に論理式

$ {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1} $

を追加してできる系を$H^2$で表す。

示すべきことは

$ \vdash_{H^2} {\cal A}_n \Rightarrow \cal B $

である。

$ {\cal B}_1,{\cal B}_2, \cdots,{\cal B}_{n-1},{\cal B}_n(={\cal B}) $

が$H^1$での「証明」とするとき、定義より 各${\cal B}_i$は次のいずれかである。

• ${\cal B}_i$は${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n$のうち１つで

ある。

• ${\cal B}_i$は公理系$H$の各公理の形の論理式である。
• 論理式 ${\cal B}_i$ の前に論理式 ${\cal B}_j$と${\cal B}_k$

$(j,k<i)$があり、${\cal B}_k$は${\cal B}_j \Rightarrow {\cal B}_i$ の 形をしている。

そして、

$ {\cal A}_n \Rightarrow {\cal B}_1,{\cal A}_n \Rightarrow {\cal B}_2, \cdots,{\cal A}_n \Rightarrow {\cal B}_{n-1},{\cal A}_n \Rightarrow {\cal B}_n $

は$H^2$での${\cal A}_n \Rightarrow {\cal B}$を含む「証明」になる。

• ${\cal B}_i$が${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}$のうち１つであれば、「添加」

$ \frac{\cal A }{\cal B \Rightarrow A} \qquad (添加) $

により、 ${\cal A}_n \Rightarrow {\cal B}_i$は$H^2$で証明可能な論理式になる。

${\cal B}_i$が${\cal A}_n$自身ならば、公理$(1)$ により、 ${\cal A}_n \Rightarrow {\cal A}_n$ は$H^2$で証明可能な論理式である。

• ${\cal B}_i$が公理系$H$の各公理の形の論理式であるとき、

同様に「添加」により、 ${\cal A}_n \Rightarrow {\cal B}_i$は$H^2$で証明可能な論理式である。

• 論理式 ${\cal B}_i$ の前に論理式 ${\cal B}_j$と${\cal B}_k$

$(j,k<i)$があり、${\cal B}_k$は${\cal B}_j \Rightarrow {\cal B}_i$ の 形をしているときは、 ${\cal A}_n \Rightarrow {\cal B}_i$の前に、

${\cal A}_n \Rightarrow {\cal B}_j$と${\cal A}_n \Rightarrow ({\cal B}_j \Rightarrow {\cal B}_i)$とがあることになる。

これに「複推移」

$ \frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } {\cal A \Rightarrow C}　(復推移) $

を適用すると ${\cal A}_n \Rightarrow {\cal B}_i$が得られる。$\Box$

演繹定理の応用

• ${\cal \lnot A}\vdash_H \bot$のとき　$　\vdash_H \cal A　$

これは、まず

$ {\cal \lnot A}\vdash_H \bot $

から演繹定理により $ \vdash_H \cal \lnot A \Rightarrow \bot $

これと公理(14)から

$ \vdash_H \cal \lnot A \Rightarrow A $

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

$ \cal A \Rightarrow A $

と$(8)$から

$ \cal (\lnot A \Rightarrow A) \Rightarrow [(A \Rightarrow A) \Rightarrow \{(A \lor \lnot A ) \Rightarrow A\} ] $

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

$ \cal A \lor \lnot A $

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

$ \vdash_H \cal A $ $\Box$

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

$ \frac{\cal \lnot A \Rightarrow \bot }{\cal A} $

また論理式の形で表せば

$ \cal (\lnot A \Rightarrow \bot) \Rightarrow A $

である。（いずれも$\vdash_H$が省略されていることに注意）

• $ \frac{\cal A \Rightarrow B}{\cal \lnot B \rightarrow \lnot A} (「対偶」) $

まず、

$ \cal \vdash_H A \Rightarrow B $

を仮定する。系$H$に$\lnot B$を追加して得られる系を$H^1$とする。 さらにこれに$\lnot A$の否定$\lnot \lnot A$を追加した系を$H^2$と すると、２重否定により、$\vdash_{H^ 2} \cal A$が、従って $\vdash_{H^2} \cal B$が得られる。このことから $\vdash_{H^2} \bot $となり、結局$\vdash_{H^1} {\cal \lnot B \Rightarrow \lnot A}$が得られる。$\Box$

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

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

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

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

• [証明]

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

$\vdash_H \cal A$が成り立つとすると；

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

$ {\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n $

があって、$\cal A$は最後の${\cal A}_n$と一致しているものとしてよい。 各${\cal A}_i$は

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

であるから${\cal A}_i$は恒真論理式である。

• 論理式 ${\cal A}_i$ の前に論理式 ${\cal A}_j$と${\cal A}_k$

$(j,k<i)$があり、${\cal A}_k$は${\cal A}_j \Rightarrow {\cal A}_i$ の 形をしている。 $i$より前の論理式は恒真論理式であると仮定すると、 ${\cal A}_j$と${\cal A}_j \Rightarrow {\cal A}_i$は真理値$\top$しかとらないから真理値表

から明らかなように${\cal A}_i$の真理値は$\top$しか取り得ない。 すなわち${\cal A}_i$は恒真論理式である。

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

• [補題]

$\cal A$が命題変数$X_1,X_2,\cdots,X_n$から構成される論理式とする。 命題変数$X_1,X_2,\cdots,X_n$に真理値$\top,\bot$をふり当て、そのふり当てに対し$\cal A$の真理値が$\top$である場合

$ \delta X_1,\delta X_2,\cdots \delta X_n \vdash_H \cal A $

$\cal A$の真理値が$\bot $である場合

$ \delta X_1,\delta X_2,\cdots \delta X_n \vdash_H \cal \lnot A $

である。ただし、$\delta X_i$は$X_i$に対する真理値のふり当てが$\top$の場合$X_i$、$\bot$の場合は$\lnot X_i$とする。$\Box$

• [定理の証明の続き]

恒真論理式$\cal A$が命題変数$X_1,X_2,\cdots,X_n$から構成されるものとする。 する。 命題変数$X_1,X_2,\cdots,X_n$に真理値$\top,\bot$どのようにふり当ても、 $\cal A$の真理値は常に$\top$である。

命題変数$X_1,X_2,\cdots,X_n$に真理値$\top,\bot$どのようにふり当てるしかたは $2^n$通りある。これを辞書式順序で全て列挙し[補題１]を適用すると

$X_1,X_2,\cdots , X_n \vdash_H \cal A \\ X_1,X_2,\cdots , \lnot X_n \vdash_H \cal A \\ X_1,X_2,\cdots , \lnot X_{n-1},X_n \vdash_H \cal A \\ X_1,X_2,\cdots , \lnot X_{n-1},\lnot X_n \vdash_H \cal A \\ \cdots \\ \cdots \\ \lnot X_1,\lnot X_2,\cdots , \lnot X_n \vdash_H \cal A \\ $

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

$X_1,X_2,\cdots , X_{n-1} \vdash X_n \Rightarrow \cal A \\ X_1,X_2,\cdots , X_{n-1} \vdash \lnot X_n \Rightarrow \cal A \\ $

これから

$ X_1,X_2,\cdots , X_{n-1} \vdash_H \cal A $

が得られる。すなわち$X_n$が消去された。同様にして順次に２式ずつ 同じ手順を繰り返せば、$X_n$が消去された$2^{n-1}$個の式を得る。この $2^{n-1}$個の式から$X_{n-1}$を２式ずつをとり同じ手順を繰り返すと$X_{n-1}$が 消去された$2^{n-2}$個の式を得る。 この手順を繰り返せば変数$X_1,X_2,\cdots,X_n$が全て消去され、結局

$ \vdash_H \cal A $

を得る。$\Box$

• [補題の証明]

• • 論理式$\cal A$がただ１つの命題変数$X$からなるとき

　　　　 $X$に対するふり当てが$\top$のとき$ X \vdash_H X$　また　$\bot$のとき $ \lnot X \vdash_H \lnot X$ これは公理の$(1)$から容易に示される。

• • これ以外の場合は、$\cal A$は$\cal \lnot B,B \land C,B \lor C$の形をしている。

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

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

• • • $\cal A$ が$\cal \lnot B$である場合

$\cal A$の値が$\top$のとき$\cal B$の値は$\bot$であるから

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \lnot \cal B$

$\cal A$の値が$\bot$のとき$\cal B$の値は$\top$であるから

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal B$

$\cal B,\lnot B$はそれぞれ$\cal A$及び$\cal \lnot A$である。

• • • $\cal A$ が$\cal B \lor C$である場合

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

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal B$

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

$\cal B \Rightarrow B \lor C$

により $ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal B \lor C$

$\cal B \lor C$は$\cal A$に他ならない。

$\cal A$の値が$\bot$のとき$\cal B,C$の値はともに$\bot$でなければならない。 このとき $ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal \lnot B$

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal \lnot C$

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

$ \frac{\cal P,Q}{\cal P \land Q} $

を用いて

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal \lnot B　\land \lnot C$ を得る。

$\cal \lnot B \land \lnot C$は$\cal \lnot A(=\lnot (B \lor C))$に他ならない。

• • • $\cal A$ が$\cal B \land C$である場合

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

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal B$

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal C$

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

$ \frac{\cal P,Q}{\cal P \land Q} $

を用いて $ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal B　\land C$ を得る。 $\cal B \land C$は$\cal A$に他ならない。

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

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal \lnot B$

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

$\cal P \Rightarrow P \lor Q$

により

$ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \cal \lnot B \lor \lnot C$

$\cal \lnot B \lor \lnot C$は$\cal \lnot A=\lnot(B \land C)$に他ならない。 　$\Box$