述語論理の完全性定理

命題論理と同様に 体系 $H$ については，次の事実が知られている:

定理10(述語論理の妥当性)

論理式$\cal A$が$H$で証明可能( $\vdash_H \cal A$) ならば任意の解釈に対して$\cal A$ が恒真論理式である。 即ち，任意の解釈 ${\cal M}({\bf D},\rho,\pi)$ に対して

$$\tau({\cal M}))[{\cal A}] = T$$ (4.69)

$\Box$ この定理は，述語論理の体系についての妥当性と呼ばれるものである。

妥当性の証明

$\vdash_H \cal A$が成り立つとすると； 系$H$の「証明」である論理式の列

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

があって，$\cal A$は最後の${\cal A}_n$と一致しているものとしてよい。 命題論理の妥当性の証明と同様，${\cal A}_k$の添え字$k$についての数学的帰納法による。

各${\cal A}_i$は

(1).

公理系の各公理の形の論理式である場合、 公理$(1)$から$(15)$までは命題論理の公理系のそれと同じ形式で 容易に恒真論理式であることを示すことができる。 ここでは，$(16)$,$(17)$が恒真論理式であることを示そう。 任意の解釈 ${\cal M}=({\bf D},\rho,\pi)$と対象変数記号と${\bf D}$の要素との対応 ${\bf\alpha}$ に対して，

$(16)$式については：

$$\tau({\cal M},{\bf\alpha})(t)=d \in {\bf D}$$ (4.70)

$$\tau({\cal M},{\bf\alpha})[(\forall x)({\cal C}(x)) \Rightarrow C(t)] =\tau({\cal M},{\bf\alpha})[\lnot (\forall x)({\cal C}(x)) \lor C(t)]$$

$$=\lnot \tau({\cal M},{\bf\alpha})[(\forall x)({\cal C}(x))] \lor \tau({\cal M},{\bf\alpha})[C(t)]$$

$$=\lnot \bigwedge_{b \in {\bf D}} \tau({\cal M},{\bf\alpha})[{\cal C}](b) \lor (\tau({\cal M},{\bf\alpha})[C](d)$$

$$\,$$ (4.71)

さらに右辺は

$$= \bigvee_{b \in {\bf D}} \{ \lnot \tau({\cal M},{\bf\alpha})[{\cal C}](b) \} \lor \tau({\cal M},{\bf\alpha})[C](d)$$

$$= \bigvee_{b \in {\bf D},b \neq d } \{ \lnot \tau({\cal M},{\bf\alpha})[{\cal C}](b) \}$$

$$\lor \lnot \tau({\cal M},{\bf\alpha})[{\cal C}(d)] \lor \tau({\cal M},{\bf\alpha})[C](d)$$ (4.72)

さらに続ければ

$$= \bigvee_{b \in {\bf D},b \neq d } \{ \lnot \tau({\cal M},{\bf\alpha})[{\cal C}](b) \} \lor T$$

$$=T$$ (4.73)

$(17)$式については：

$$\tau({\cal M},{\bf\alpha})[{\cal C}(t)] \Rightarrow (\exists x)({\cal C}(x))] =\lnot \tau({\cal M},{\bf\alpha})[{\cal C}](d) \lor \tau({\cal M},{\bf\alpha})[(\exists x)({\cal C}(x) ) ]$$

$$\,$$ (4.74)

さらに右辺は

$$=\lnot \tau({\cal M},{\bf\alpha})[{\cal C}](d) \lor \bigvee_{b \in {\bf D}}\tau({\cal M},{\bf\alpha})[{\cal C}](b)$$

$$=\lnot \tau({\cal M},{\bf\alpha})[{\cal C}](d) \lor \tau({\cal M},{\bf\alpha})[{\cal C}](d)$$

$$\lor \bigvee_{b \in {\bf D},b \neq d}\tau({\cal M},{\bf\alpha})[{\cal C}](b)$$

$$=T \lor \bigvee_{b \in {\bf D},b \neq d}\tau({\cal M},{\bf\alpha})[{\cal C}](b)$$

$$=T$$ (4.75)

(2).

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

${\cal A}_i$	${\cal A}_k$	${\cal A}_i \Rightarrow {\cal A}_k$
$F$	$F$	$T$
$F$	$T$	$T$
$T$	$F$	$F$
$T$	$T$	$T$

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

(3).

論理式 ${\cal A}_k$ の前に論理式 ${\cal A}_j$ $(j<k)$があり，${\cal A}_j$は 　　

$${\cal C} \Rightarrow {\cal D}(t)$$ (4.76)

であり，${\cal A}_k$は

$${\cal C} \Rightarrow (\forall t)({\cal D}(t))$$ (4.77)

の形をしている場合。 ただし$t$は自由変数記号で$\cal C$には現れないものとする。 この場合，まず,${\cal A}_k$の ${\cal M},{\bf\alpha}$での真理値は

$$\tau({\cal M},{\bf\alpha})[{\cal C} \Rightarrow (\forall t)({\cal D}(t))]$$

$$=\lnot \tau({\cal M},{\bf\alpha})[{\cal C}] \lor \bigwedge_{b \in {\bf D}} \tau({\cal M},{\bf\alpha})[{\cal C}](b)$$

$$=\bigwedge_{b \in {\bf D}} \{ \lnot \tau({\cal M},{\bf\alpha})[{\cal C}] \lor \tau({\cal M},{\bf\alpha})[{\cal C}](b) \}$$ (4.78)

である。 しかし,帰納法の仮定から ${\cal A}_j$すなわち

$${\cal C} \Rightarrow {\cal D}(t)$$ (4.79)

は 任意の ${\cal M},{\bf\alpha}$について

$$\tau({\cal M},{\bf\alpha})[({\cal C} \Rightarrow {\cal D}(t)]=T$$ (4.80)

ゆえ任意の$b \in {\bf D}$について

$$\tau({\cal M},{\bf\alpha})[(\lnot {\cal C} \lor {\cal D}(b)]=T$$ (4.81)

従って

$$\bigwedge_{b \in {\bf D}} \{ \lnot \tau({\cal M},{\bf\alp... ...cal C}] \lor \tau({\cal M},{\bf\alpha})[{\cal C}](b) \} =T$$ (4.82)

すなわち,

$$\tau({\cal M},{\bf\alpha})[{\cal C} \Rightarrow (\forall t)({\cal D}(t))] =T$$ (4.83)

最後に，

(4).

論理式 ${\cal A}_k$ の前に論理式 ${\cal A}_j$ $(j<k)$があり，${\cal A}_j$は

$${\cal C}(t) \Rightarrow {\cal D}$$ (4.84)

であり，${\cal A}_k$は

$$(\exists t)({\cal C}(t)) \Rightarrow {\cal D}$$ (4.85)

の形をしている場合を考えよう。 ただし$t$は自由変数記号で$\cal D$には現れないものとする。 まず,

$$\tau({\cal M},{\bf\alpha})[ (\exists t)({\cal C}(t)) \Rightarrow {\cal D}]$$

$$=\lnot \bigvee_{b \in {\bf D}} \tau({\cal M},{\bf\alpha})[{\cal C}](b) \lor {\cal D}$$

$$=\bigwedge_{b \in {\bf D}} \lnot \tau({\cal M},{\bf\alpha})[{\cal C}](b) \lor {\cal D}$$ (4.86)

さらに右辺は

$$=\bigwedge_{b \in {\bf D}} \{ \lnot \tau({\cal M},{\bf\alpha})[{\cal C}](b) \lor {\cal D} \}$$

$$=\bigwedge_{b \in {\bf D}} \{ \tau({\cal M},{\bf\alpha})[{\cal C}](b) \Rightarrow {\cal D} \}$$ (4.87)

しかし帰納法の仮定から ${\cal A}_j$すなわち

$${\cal C}(t) \Rightarrow {\cal D}$$ (4.88)

任意の ${\cal M},{\bf\alpha}$について

$$\tau({\cal M},{\bf\alpha})[{\cal C}(t) \Rightarrow {\cal D}]=T$$ (4.89)

従って任意の$b \in {\bf D}$について

$$\tau({\cal M},{\bf\alpha})[{\cal C}(b) \Rightarrow {\cal D}]=T$$ (4.90)

よって

$$\bigwedge_{b \in {\bf D}} \{ \tau({\cal M},{\bf\alpha})[{\cal C}](b) \Rightarrow {\cal D} \}=T$$ (4.91)

すなわち

$$\tau({\cal M},{\bf\alpha})[ (\exists t)({\cal C}(t)) \Rightarrow {\cal D}] =T$$ (4.92)

$\Box$

定理11(述語論理の無矛盾性)

述語論理の公理系$H$は無矛盾である。 すなわち

$$\vdash_H {\cal A} \qquad \vdash_H \lnot {\cal A}$$ (4.93)

となるような論理式は存在しない。 $\Box$　
この定理は，述語論理の体系についての無矛盾性と呼ばれるものである。

無矛盾性の証明

命題論理の証明と全く同じである。系$H$が矛盾すれば 定理6により任意の論理式${\cal C}$が証明可能である。 従って，${\cal C}$は述語論理の妥当性の定理により任意の解釈${\cal M}$ について恒真論理式である。 しかるに，$H$の$0$変数の述語記号${\bf P }^0$，すなわち命題変数は論理式ではあるが恒真論理式 ではない。$\Box$

定理12(述語論理の完全性定理)

$\cal A$ が恒真論理式であることの必要十分条件は， $\vdash_H \cal A$ が成立することである。$\Box$
この定理は，述語論理の体系についての完全性定理(completeness theorem)と呼ばれるものである。

完全性定理の証明

$\vdash_H \cal A$が成立すれば任意の解釈${\cal M}$について

$$\tau({\cal M})[{\cal A}]=T$$ (4.94)

すなわち$\cal A$が恒真論理式であることは妥当性の定理で既に証明済みである。

逆に$\cal A$が恒真論理式であるときに， $\vdash_H \cal A$が成立することをいうには次のHenkinの定理を 利用する。

Henkinの定理

論理式の集合${\cal G}$が無矛盾ならば${\cal G}$は充足可能である。 すなわち解釈 ${\cal M}=({\bf D},\rho,\pi)$と, 対象変数記号と${\bf D}$との 対応$\alpha$が存在して, ${\cal G}$の任意の論理式$\cal A$ について

$$\tau({\cal M},{\alpha})[{\cal A}]=T$$ (4.95)

$\Box$

定理12の証明の続き

任意の解釈${\cal M}$について

$$\tau({\cal M})[{\cal A}]=T$$ (4.96)

であるすれば

$$\tau({\cal M})[\lnot {\cal A}]=T$$ (4.97)

となる解釈${\cal M}$は存在しない。 すなわち ${\cal G}=\{ \lnot {\cal A} \}$ は充足し得ない。

Henkinの定理の対偶によれば, 体系 ${\cal G}=\{ \lnot {\cal A} \}$は矛盾する。
定理5によれば,任意の論理式${\cal B}$について

$$\lnot {\cal A} \vdash_H {\cal B}$$ (4.98)

かつ

$$\lnot {\cal A} \vdash_H \lnot {\cal B}$$ (4.99)

である。
これらから 演繹定理8によれば

$$\vdash_H \lnot {\cal A} \Rightarrow {\cal B}$$ (4.100)

$$\vdash_H \lnot {\cal A} \Rightarrow \lnot {\cal B}$$ (4.101)

を得る。これらから公理$(5)$を用いれば

$$\vdash_H (\lnot {\cal A} ) \Rightarrow ({\cal B} \land \lnot {\cal B})$$ (4.102)

対偶をとれば

$$\vdash_H (\lnot {\cal B} \lor {\cal B}) \Rightarrow {\cal A}$$ (4.103)

ここで,公理$(15)$によれば

$$\vdash_H \lnot {\cal B} \lor {\cal B}$$ (4.104)

従って

$$\vdash_H {\cal A}$$ (4.105)

を得る。$\Box$

Henkinの定理の証明

論理式の集合${\cal G}$が無矛盾とする。段階的に${\cal G}$が充足可能で あることを示そう。

1. 定義
   論理式の集合${\cal L}$に論理式${\cal C}$を加えた ${\cal L} \cup \{ {\cal C} \}$ が矛盾するとき，${\cal C}$は${\cal L}$と矛盾するという。
   
2. ${\cal C}$が${\cal L}$と矛盾するときは必ず，${\cal L}$の有限部分集合 $\{ {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \} \subset {\cal L}$と矛盾している。
   実際，
   

   $${\cal L}　\vdash_H {\cal B},\lnot {\cal B}$$ (4.106)

   
   
   となる論理式${\cal B}$あれば， ${\cal B}$， $\lnot {\cal B}$の証明である論理式の有限列
   

   $${\cal P}_1,{\cal P}_2,\cdots ,{\cal B}$$ (4.107)

   
   
   と
   

   $${\cal Q}_1,{\cal Q}_2,\cdots ,\lnot {\cal B}$$ (4.108)

   
   
   が存在するが，これらに現われる${\cal L}$の論理式と公理は 有限個しかない。他の論理式は推論規則によって，上の有限列中に現われる ${\cal L}$の論理式と公理から導出されている。 従って，${\cal B}$， $\lnot {\cal B}$は有限個のLの論理式と公理 から導出される。$\Box$
   
3. 定義
   論理式の集合${\cal L}$が無矛盾で，${\cal L}$に属さない総ての論理式が${\cal L}$と矛盾するとき${\cal L}$を最大無矛盾集合という。

4. 定義
   自由変数記号(限定記号で束縛されていない対象変数記号) を持たない論理式を個体閉論理式という。
   

5. 補題
   ${\cal K}$を述語論理の系$H$の個体閉論理式全体の集合とする。
   ${\cal K}_0$を${\cal K}$の無矛盾な部分集合とする。
   ${\cal K}_0$をその部分集合として含む最大無矛盾集合 ${\cal L}$が存在する。$\Box$
   　
6. [補題の証明] 述語論理の論理式は対象定数記号，対象変数記号，論理記号，関数記号，述語記号を有限個並べた記号列であり，その論理式全体の集合は高々加算無限集合である。
   (要素は無限個でもその要素一つ一つに自然数による番号を付与することができる。)
   従って，論理式全体の集合の部分集合${\cal K}$も高々加算である。
   ${\cal K}$の要素である論理式に番号を付けておく。
   ${\cal K}_0$から初めて，以下の手順で，論理式の集合${\cal K}_n$を構成する。
   1. ${\cal K}$の$n+1$番目の論理式が $(\forall a){\cal A}(a)$の形であるとき。
      ${\cal K}_n$の論理式すべてと，${\cal A}$の中に現われない対象定数記号 $v$を選び，論理式 ${\cal A}(v) \Rightarrow (\forall a){\cal A}(a)$を ${\cal K}_n$に追加して， ${\cal K}_{n+1}$とする。即ち，
      
      

      $${\cal K}_{n+1}={\cal K}_{n} \cup \{ {\cal A}(v) \Rightarrow (\forall a){\cal A}(a) \}$$ (4.109)

      
      
      とする。
   2. ${\cal K}$の$n+1$番目の論理式が $(\forall a){\cal A}(a)$の形でないときは 何も追加せず
      
      

      $${\cal K}_{n+1}={\cal K}_{n}$$ (4.110)

      
      
      とする。
   上の構成手続きによって個体閉論理式の集合の増大列
   

   $${\cal K}_0 \subset {\cal K}_1 \subset \cdots {\cal K}_n \subset {\cal K}_{n+1} \cdots$$ (4.111)

   
   
   が得られるが，${\cal K}_n$はすべて無矛盾集合である。
   これを示すには$n$についての帰納法による。
   $n=0$については${\cal K}_0$の仮定により，無矛盾。${\cal K}_n$が無矛盾として ${\cal K}_{n+1}$が矛盾するとすれば，ある論理式${\cal B}$が存在して，

   
   

   $${\cal K}_{n},{\cal A}(v) \Rightarrow (\forall a){\cal A}(a) \vdash_H {\cal B}, \lnot {\cal B}$$ (4.112)

   
   
   ${\cal K}_n$の論理式すべてと，${\cal A}$の中に現われない対象変数記号 $w$を選べば， ${\cal A}(a)$の$a$を$w$に書き換えた論理式を${\cal A}(w)$とすると
   

   $${\cal A}(v) \Rightarrow {\cal A}(w)$$ (4.113)

   
   
   から
   

   $$[{\cal A}(w) \Rightarrow (\forall a) {\cal A}(a)] \Rightarrow [{\cal A}(v) \Rightarrow (\forall a) {\cal A}(a)]$$ (4.114)

   
   
   よって，
   

   $${\cal K}_{n},{\cal A}(w) \Rightarrow (\forall a){\cal A}(a) \vdash_H {\cal B}, \lnot {\cal B}$$ (4.115)

   
   
   こから演繹定理により，
   

   $${\cal K}_{n} \vdash_H (\forall w)({\cal A}(w) \Rightarrow (\forall a){\cal A}(a)) \Rightarrow {\cal B}$$ (4.116)

   
   
   
   

   $${\cal K}_{n} \vdash_H (\forall w)({\cal A}(w) \Rightarrow (\forall a){\cal A}(a)) \Rightarrow \lnot {\cal B}$$ (4.117)

   
   
   これらから，
   

   $${\cal K}_{n} \vdash_H \lnot (\forall w)({\cal A}(w) \Rightarrow (\forall a){\cal A}(a))$$ (4.118)

   
   
   を得て，${\cal A}(w)$では$a$は自由変数でないから冠頭標準形の議論により，
   

   $$(\forall w)({\cal A}(w) \Rightarrow (\forall a){\cal A}(a... ...(\forall w)(\forall a) ({\cal A}(w) \Rightarrow {\cal A}(a))$$ (4.119)

   
   
   従って，
   

   $${\cal K}_{n} \vdash_H \lnot (\forall w)(\forall a)({\cal A}(w) \Rightarrow {\cal A}(a))$$ (4.120)

   
   
   これから
   

   $${\cal K}_{n} \vdash_H \lnot (\forall a)({\cal A}(a) \Rightarrow {\cal A}(a))$$ (4.121)

   
   
   しかし，公理$(1)$と推論規則「全称化」によれば，
   

   $${\cal K}_{n} \vdash_H (\forall a)({\cal A}(a) \Rightarrow {\cal A}(a))$$ (4.122)

   
   
   従って，${\cal K}_{n}$は矛盾する。これは帰納法の仮定に反する。 よって ${\cal K}_{n+1}$は無矛盾。$\Box$
   

   結局，無矛盾な個体閉論理式の集合の増大列
   

   $${\cal K}_0 \subset {\cal K}_1 \subset \cdots {\cal K}_n \subset {\cal K}_{n+1} \cdots$$ (4.123)

   
   
   が得られていた。
   

   ここで，
   

   $${\cal L}=\cup_{n=0}^{n= \infty }{\cal K}_n$$ (4.124)

   
   
   とおけば，${\cal L}$も無矛盾である。 実際，
   

   $${\cal L}　\vdash_H {\cal B},\lnot {\cal B}$$ (4.125)

   
   
   となる論理式${\cal B}$あれば， ${\cal B}$， $\lnot {\cal B}$の証明である論理式の有限列
   

   $${\cal P}_1,{\cal P}_2,\cdots ,{\cal B}$$ (4.126)

   
   
   と
   

   $${\cal Q}_1,{\cal Q}_2,\cdots ,\lnot {\cal B}$$ (4.127)

   
   
   が存在するが，これらに現われる${\cal L}$の論理式と公理は 有限個しかない。他の論理式は推論規則によって，上の有限列中に現われる ${\cal L}$の論理式と公理から導出されている。 従って，${\cal B}$， $\lnot {\cal B}$は有限個の${\cal L}$の論理式と公理 から導出される。 $n$を十分大きく取れば，${\cal K}_n$がそれらの論理式を全てその要素と してもち，これは${\cal K}_n$自身が既に矛盾することを示す。 $\Box$
   

7. 最大無矛盾集合${\cal L}$は以下の性質をもつ。
   1. ${\cal K}$に属する論理式${\cal A}$が${\cal L}$の元なら $\lnot {\cal A}$は${\cal L}$の元でない
      実際， $\lnot {\cal A}$も${\cal L}$の元なら${\cal L}$は矛盾する。$\Box$
   2. ${\cal K}$の論理式${\cal A}$が${\cal L}$の元でないならば $\lnot {\cal A}$は${\cal L}$の元である。
      実際， ${\cal A}$が${\cal L}$の元でないなら${\cal L}$の最大性により， ${\cal L} \cup \{ {\cal A}\}$は矛盾。従って論理式${\cal B}$が存在して

      
      

      $${\cal L},\lnot {\cal A} \vdash_H {\cal B}, \lnot {\cal B}$$ (4.128)

      
      
      これらから 演繹定理8によれば
      

      $${\cal L} \vdash_H {\cal A} \Rightarrow {\cal B} \land \lnot {\cal B}$$ (4.129)

      
      
      対偶をとれば
      

      $${\cal L} \vdash_H (\lnot {\cal B} \lor {\cal B}) \Rightarrow \lnot {\cal A}$$ (4.130)

      
      

      ここで,公理$(15)$によれば
      

      $${\cal L} \vdash_H \lnot {\cal B} \lor {\cal B}$$ (4.131)

      
      
      従って
      

      $${\cal L} \vdash_H \lnot {\cal A}$$ (4.132)

      
      
      を得る。従って $\lnot {\cal A}$は${\cal L}$と無矛盾。従って これの元となる。$\Box$
      
   3. ${\cal K}$に属する論理式 ${\cal A},{\cal B}$が両方とも${\cal L}$の元であるとき， ${\cal A} \land {\cal B}$は${\cal L}$の元である。
      ${\cal A},{\cal B}$が両方とも${\cal L}$の元なら推論規則「論理積」により
      

      $${\cal L} \vdash_H {\cal A} \land {\cal B}$$ (4.133)

      
      
      で ${\cal A} \land {\cal B}$は${\cal L}$と無矛盾。$\Box$

   4. ${\cal K}$に属する論理式 ${\cal A},{\cal B}$のどちらか一方が${\cal L}$の 元でないとき， ${\cal A} \land {\cal B}$は${\cal L}$の元でない。
      ${\cal A} \land {\cal B}$が${\cal L}$の元なら， 公理$(6),(7)$から ${\cal A},{\cal B}$の何れも${\cal L}$と矛盾しない。 これから ${\cal A},{\cal B}$の何れも${\cal L}$の元なる。$\Box$

   5. ${\cal K}$に属する論理式 ${\cal A},{\cal B}$がのどちらか一方が${\cal L}$の元であるとき， ${\cal A} \lor {\cal B}$は${\cal L}$の元である。
      証明は$\land$の場合と双対であるから省略する。

   6. ${\cal K}$に属する論理式 ${\cal A},{\cal B}$が両方とも${\cal L}$の元でないとき， ${\cal A} \lor {\cal B}$は${\cal L}$の元でない。
      証明は$\land$の場合と双対であるから省略する。

   7. $a$を対象変数記号，$c$を対象定数記号とする。 すべての$c$について${\cal K}$に属する論理式${\cal A}(c)$が${\cal L}$の元であるとき， $(\forall a)({\cal A}(a))$は${\cal L}$の元である。
      

      $(\forall a){\cal A}(a)$が${\cal K}$の$n+1$番目の個体閉論理式とすると， ${\cal K}_{n+1}$の構成法から ${\cal K}_{n+1}$は, 論理式
      

      $${\cal A}(w) \Rightarrow (\forall a){\cal A}(a)$$ (4.134)

      
      
      を元にもつ。$w$は${\cal K}_{n}$の全ての論理式と${\cal A}$に現われない対象変数記号である。仮定から，${\cal A}(w)$は${\cal L}$の元ゆえ，
      

      $$(\forall a){\cal A}(a)$$ (4.135)

      
      
      も${\cal L}$と矛盾せず，${\cal L}$の最大性から $(\forall a){\cal A}(a)$ は，${\cal L}$の元となる。$\Box$
      

   8. $a$を対象変数記号，$c$を対象定数記号とする。 少なくとも一つの$c$について${\cal K}$に属する論理式$({\cal A}(c))$ が${\cal L}$の元でないとき， $(\forall a)({\cal A}(a))$は${\cal L}$の元でない。
      

      $(\forall a)({\cal A}(a))$は${\cal L}$の元ならば，公理 $(16)$により， ${\cal A}(w)$について ${\cal L} \vdash_H {\cal A}(w)$であり，従って，${\cal L}$と矛盾しない から，その元になる。

   9. $a$を対象変数記号，$c$を対象定数記号とする。 少なくとも一つの$c$について${\cal K}$に属する論理式${\cal A}(c)$が${\cal L}$の元であるとき， $(\exists a)({\cal A}(a))$は${\cal L}$の元である。
      証明は$\forall$の場合と双対であるから省略する。

   10. $a$を対象変数記号，$c$を対象定数記号とする。 すべての$c$について${\cal K}$に属する論理式${\cal A}(c)$が${\cal L}$の元で ないならば， $(\exists a)({\cal A}(a))$は${\cal L}$の元でない。
       証明は$\forall$の場合と双対であるから省略する。

8. 最大無矛盾集合${\cal L}$を用いた$H$の解釈
   以下のように解釈 ${\cal M}=({\bf D},\rho,\pi)$を構成する。
   1. ${\bf D}$を対象定数記号全体の集合とする。
   2. $H$の対象変数記号に${\bf D}$の要素 を対応させる対応$\alpha$は任意にとる。
   3. 関数記号と${\bf D}$上の関数との対応$\rho$：
      $n$変数の関数記号の全体${\cal F}^n$と${\bf D}$上の関数全体の集合
      

      $${\cal F}({\bf D}^n,{\bf D}) =\{ f \vert f :(x_1,x_2,\cdots... ...\in {\bf D}^n \mapsto f (x_1,x_2,\cdots,x_n) \in {\bf D} \}$$ (4.136)

      
      
      の間の対応$\rho$は ${\bf\phi }^n \in {\cal F}^n$に対して
      

      $$\rho({\bf\phi }^n)(x_1,x_2,\cdots,x_n)={\phi }^n(x_1,x_2,\cdots,x_n) ,\in {\bf D}^n$$ (4.137)

      
      
      で定義する。(結局，恒等対応で， $\rho({\bf\phi }^n)$は${\bf\phi}^n$の定義域を${\bf D}$に制限するだけである。)
   4. $H$の述語記号と${\bf D}$上の述語との対応 ：
      真理値の集合を ${\bf V}=\{T,F\}$， $H$の$n$変数の述語記号の 全体の集合${\cal P}^n$と, ${\bf D}$上の$n$変数の述語全体の集合
      

      $${\cal P}({\bf D}^n;{\bf V}) =\{ P \vert P :(y_1,y_2,\cdot... ... \in {\bf D}^n \mapsto P(y_1,y_2,\cdots,y_n) \in {\bf V} \}$$ (4.138)

      
      
      の間の対応
      

      $${\bf P }^n \in {\cal P}^n \mapsto \pi({\bf P }^n) \in {\cal P}({\bf D}^n,{\bf V}) \\$$ (4.139)

      
      
      については，$n$変数の述語記号${\bf P } ^n$に
      

      $$(y_1,y_2,\cdots,y_n) \in {\bf D}^n \mapsto {\bf Q}(y_1,y_2,\cdots,y_n)$$

      $$=\left\{ \begin{array}{lc} T & {\bf P} (y_1,y_2,\cdots,y_n) が {\... ...る \\ F & {\bf P} (y_1,y_2,\cdots,y_n) が{\cal L}に属さない \end{array}\right.$$

      
      
      となる述語${\bf Q}$を対応させる。
   以上の構成法により，$H$の任意の論理式${\cal A}$について ${\cal A}$が${\cal L}$の元でないとき
   

   $$\tau({\cal M},{\alpha})[{\cal A}]=F$$ (4.140)

   
   

   また${\cal A}$が${\cal L}$の元のとき

   
   

   $$\tau({\cal M},{\alpha})[{\cal A}]=T$$ (4.141)

   
   

   　これは論理式${\cal A}$の記号列のとしての長さについての帰納法による。

   1. 論理式${\cal A}$が$n$ 変数述語記号${\bf P}$と項 $c_1,c_2,\cdots,c_n$を用いて
      　
      

      $${\bf P}(c_1,c_2,\cdots,c_n)$$ (4.142)

      
      
      で表されるとき：
      

      $${\bf P}(c_1,c_2,\cdots,c_n)$$ (4.143)

      
      
      が${\cal L}$に属すれば

      $\pi$の定義から，
      

      $$\tau({\cal M},{\alpha})[{\cal A}]=\pi ({\bf P})(c_1,c_2,\cdots,c_n)=T$$ (4.144)

      
      

      ${\cal L}$に属さなければ

      $\pi$の定義から，

      
      

      $$\tau({\cal M},{\alpha})[{\cal A}]=\pi ({\bf P})(c_1,c_2,\cdots,c_n)=F$$ (4.145)

      
      

   2. 論理式${\cal A}$が $\lnot {\cal B}$の形をしている場合。
      1. $\lnot {\cal B}$が${\cal L}$に属すれば ${\cal B}$は${\cal L}$に属さない。この論理式の長さは${\cal A}$ より短いので，帰納法の仮定により，
         

         $$\tau( {\cal M},{\bf\alpha})[{\cal B}]=F$$ (4.146)

         
         
         よって
         

         $$\tau({\cal M},{\bf\alpha})[{\cal A}] =\lnot \tau({\cal M},{\bf\alpha })[{\cal B}]=T$$ (4.147)

         
         

      2. $\lnot {\cal B}$が${\cal L}$に属さなければ ${\cal B}$は${\cal L}$に属す。この論理式の長さは${\cal A}$ より短いので，帰納法の仮定により，
         

         $$\tau({\cal M},{\bf\alpha})[{\cal B}]=T$$ (4.148)

         
         
         よって
         

         $$\tau({\cal M},{\bf\alpha})[{\cal A}] =\lnot \tau({\cal M},{\bf\alpha})[{\cal B}]=F$$ (4.149)

         
         

   3. 論理式${\cal A}$が ${\cal B} \lor {\cal C}$の形をしている場合。
      
      1. ${\cal B} \lor {\cal C}$が${\cal L}$に属せば ${\cal B},{\cal C}$のうち少なくとも一方は${\cal L}$に属する。 これらの論理式の長さは${\cal A}$ より短いので，帰納法の仮定により，
         

         $$\tau({\cal M},{\bf\alpha})[{\cal B}]=T$$ (4.150)

         
         
         または
         

         $$\tau({\cal M},{\bf\alpha})[{\cal C}]=T$$ (4.151)

         
         
         よって
         

         $$\tau({\cal M},{\bf\alpha})[{\cal A}] =\tau({\cal M},{\bf... ...})[{\cal B}] \lor \tau({\cal M},{\bf\alpha } )[{\cal C}]=T$$ (4.152)

         
         

      2. ${\cal B} \lor {\cal C}$が${\cal L}$に属さなければ
         ${\cal B},{\cal C}$の何れも${\cal L}$に属さない。 ${\cal B}$は${\cal L}$に属す。この論理式の長さは${\cal A}$ より短いので，帰納法の仮定により，
         

         $$\tau( {\cal M},{\bf\alpha})[{\cal B}]=F$$ (4.153)

         
         
         かつ
         

         $$\tau({\cal M},{\bf\alpha})[{\cal C}]=F$$ (4.154)

         
         
         よって
         

         $$\tau({\cal M},{\bf\alpha})[{\cal A}]= \tau({\cal M},{\bf... ...ha})[{\cal B}] \lor \tau({\cal M},{\bf\alpha})[{\cal C}]=F$$ (4.155)

         
         

   4. 論理式${\cal A}$が ${\cal B} \Rightarrow {\cal C}$の形をしている場合。
      

      $${\cal B} \Rightarrow {\cal C}= \lnot {\cal B} \lor {\cal C}$$ (4.156)

      
      
      で$\lor,\lnot$の結果を用いて示すことができるので省略する。

   5. ${\cal C}(a)$ が対象変数記号$a$を含む論理式で，$a$が自由変数記号， $x$を${\cal C}(a)$の中に現れない対象変数記号， ${\cal A}$が $(\forall x)({\cal C}(x) )$の形をしているとき。
      1. $(\forall x)({\cal C}(x) )$が${\cal L}$に属すれば ${\cal L}$の性質について述べたことから， すべての対象定数記号$v$について ${\cal C}(v)$は${\cal L}$の元。従って，
         

         $$\tau({\cal M},{\bf\alpha})[{\cal C}(v)]= \tau({\cal M},{\bf\alpha})[{\cal C}](v)=T$$ (4.157)

         
         
         ここで，$\rho(v)=v$に注意する。 従って，
         

         $$\tau({\cal M},{\bf\alpha})[(\forall x)({\bf\cal C}(x))] =... ...edge_{b \in {\bf D}}\tau({\cal M},{\bf\alpha})[{\cal C}](b)=T$$ (4.158)

         
         

      2. $(\forall x)({\cal C}(x) )$が${\cal L}$に属さなければ ${\cal L}$の性質について述べたことから， ある対象定数記号$v$について ${\cal C}(v)$は${\cal L}$の元でない。従って，
         

         $$\tau({\cal M},{\bf\alpha})[{\cal C}(v)]= \tau({\cal M},{\bf\alpha})[{\cal C}](v)=F$$ (4.159)

         
         
         従って，
         

         $$\tau({\cal M},{\bf\alpha})[(\forall x)({\cal C}(x))] =\bigwedge_{b \in {\bf D}}\tau({\cal M},{\bf\alpha})[{\cal C}](b)=F$$ (4.160)

         
         

   6. ${\cal C}(a)$ が対象変数記号$a$を含む論理式で，$a$が自由変数記号， $x$を${\cal C}(a)$の中に現れない対象変数記号， ${\cal A}$が $(\exists x)({\cal C}(x) )$の形をしているとき。 これも $(\forall x)({\cal C}(x) )$の場合と双対的にできるので省略する。

9. ${\cal K}_0$は${\cal L}$の部分集合である。

   
   

   $${\cal K}_0 \subset {\cal K} ,{\cal K}_0 \subset {\cal L}$$ (4.161)

   
   

   従って，${\cal K}_0$の任意の論理式${\cal C}$について
   

   $$\tau({\cal M},{\bf\alpha})[{\cal C}]=T$$ (4.162)

   
   
   即ち，${\cal K}_0$は充足可能である。
10. ${\cal G}$から無矛盾な個体閉論理式の集合${\cal K}_0$を作る。
    
    1. ${\cal G}$の論理式の自由変数記号に対象定数記号を 代入する。こうしてできる論理式は個体閉論理式である。
       
    2. ${\cal G}$の総ての論理式のこの操作を施して作った 論理式の集合を${\cal K}_0$で表す。${\cal G}$が無矛盾 ゆえ${\cal K}_0$は無矛盾である。
       例
       

       $$(\forall x)(\exists y){\bf P}(x,y,z)$$ (4.163)

       
       
       から自由変数$z$に対象定数記号$c$を代入すると
       

       $$(\forall x)(\exists y){\bf P}(x,y,c)$$ (4.164)

       
       
       を得る。
    3. 個体閉論理式の集合${\cal K}_0$が無矛盾であれば，充足可能な ことは示した。さらに${\cal K}_0$の${\cal G}$からの構成法から ${\cal G}$は充足可能である。