項モデルと完全性定理 | 数理論理

1 証明可能な等号による商

$L$ を集合サイズの有限項言語、 $T\subseteq\operatorname{Sent}(L)$ を構文的に無矛盾な理論とする。§E19.11 定理 6.1によって得られる拡大言語と理論を $L^H,T^H$ と書く。 $L^H$ の閉項全体を $\operatorname{CTerm}(L^H)$ と書く。

定義 1.1 (証明可能な等号). $t,u\in\operatorname{CTerm}(L^H)$ に対して

t\sim_{T^H}u \quad\Longleftrightarrow\quad T^H\vdash t=u

と定める。この関係を証明可能等号関係 (provable-equality relation) という。文脈から明らかな場合は添字を省いて $t\sim u$ と書き、 $t$ の同値類を $[t]$ と書く。

定理 1.2. 関係 $\sim$ は $\operatorname{CTerm}(L^H)$ 上の同値関係である。さらに、任意の非負整数 $n$ について次が成り立つ。

$f$ が $n$ 項関数記号であり、すべての $i<n$ について $t_i\sim u_i$ なら、 $f(t_1,\ldots,t_n)\sim f(u_1,\ldots,u_n).$
$R$ が $n$ 項関係記号であり、すべての $i<n$ について $t_i\sim u_i$ なら、 $T^H\vdash R(t_1,\ldots,t_n)\leftrightarrow R(u_1,\ldots,u_n).$ 特に、 $R(t_1,\ldots,t_n)$ と $R(u_1,\ldots,u_n)$ の一方が $T^H$ から導出可能であることと、他方が $T^H$ から導出可能であることは同値である。

$n=0$ の場合には、二つの引数列はともに空であり、同じ零項記号の解釈を比較する。

証明. 等号公理の反射律から $T^H\vdash t=t$ なので、 $t\sim t$ である。§E19.10 補題 4.1により、 $t\sim u$ なら $u\sim t$ であり、 $t\sim u$ かつ $u\sim v$ なら $t\sim v$ である。したがって $\sim$ は同値関係である。

$f$ を $n$ 項関数記号とし、各 $t_i\sim u_i$ を仮定する。定義により $T^H\vdash t_i=u_i$ である。有限個の等式を命題論理の派生則によって連言にまとめ、関数合同公理

(t_1=u_1\land\cdots\land t_n=u_n) \to f(t_1,\ldots,t_n)=f(u_1,\ldots,u_n)

へ modus ponens を適用すると、 $T^H\vdash f(\bar t)=f(\bar u)$ を得る。 $n=0$ では前件が空の連言であり、結論は同じ零項関数記号が表す閉項の反射的等式である。

$R$ を $n$ 項関係記号とする。同じ連言と関係合同公理から

T^H\vdash R(t_1,\ldots,t_n)\leftrightarrow R(u_1,\ldots,u_n)

を得る。双条件の二方向と modus ponens により、一方が導出可能なら他方も導出可能である。 $n=0$ では公理で同じ零項関係 $R$ と自身の双条件が述べられるので、同じ結論が成り立つ。以上はすべての有限 $n$ に対する個別の公理スキーマに基づいており、二項演算だけの商降下には依存しない。▨

2 項モデル

定義 2.1. $T^H$ の項モデル (term model) $M_{T^H}$ を次のように定める。

|M_{T^H}|=\operatorname{CTerm}(L^H)/{\sim}.

$n$ 項関数記号 $f$ と $n$ 項関係記号 $R$ の解釈を

\begin{aligned} f^{M_{T^H}}([t_1],\ldots,[t_n]) &=[f(t_1,\ldots,t_n)],\\ R^{M_{T^H}} &=\left\{([t_1],\ldots,[t_n]):T^H\vdash R(t_1,\ldots,t_n)\right\} \end{aligned}

によって定める。論理的等号は、商集合上の同一性として解釈する。

定理 1.2により、関数の値と関係の真理値は代表元の選択に依存しない。 Henkin 構成では少なくとも一つの新定数が加わるため、閉項が存在する。したがって、項モデルの台集合は空でない。より具体的には、一自由変数論理式 $x=x$ に対する証人定数により閉項が得られる。

補題 2.2. $\tau$ を、各変数 $x$ へ閉項 $\tau(x)$ を割り当てる写像とし、 $s_\tau(x)=[\tau(x)]$ とおく。任意の $L^H$ 項 $r$ について

\llbracket r\rrbracket_{s_\tau}^{M_{T^H}}=[r[\tau]]

が成り立つ。 $r[\tau]$ は、 $r$ に実際に現れる有限個の変数だけを対応する閉項へ同時代入した閉項である。

証明. $r$ の構造に関する帰納法を用いる。 $r=x$ なら、左辺は定義により $s_\tau(x)=[\tau(x)]$ であり、右辺と一致する。 $r$ が定数記号なら、両辺はその定数の同値類である。

$r=f(r_1,\ldots,r_n)$ とする。帰納法の仮定と項モデルの関数解釈により

\begin{aligned} \llbracket f(r_1,\ldots,r_n)\rrbracket_{s_\tau}^{M_{T^H}} &=f^{M_{T^H}}([r_1[\tau]],\ldots,[r_n[\tau]])\\ &=[f(r_1[\tau],\ldots,r_n[\tau])]\\ &=[r[\tau]]. \end{aligned}

$n=0$ の場合も第2行が零項関数の定義そのものである。▨

3 真理補題

論理式 $\varphi$ と閉項割当て $\tau$ に対し、 $\varphi[\tau]$ は $FV(\varphi)$ に属する有限個の変数へ、 $\tau$ が割り当てる閉項を、捕獲を避けて同時代入した文を表す。

補題 3.1. 任意の $L^H$ 論理式 $\varphi$ と閉項割当て $\tau$ について、

M_{T^H},s_\tau\models\varphi \quad\Longleftrightarrow\quad T^H\vdash\varphi[\tau]

が成り立つ。

同値な有限変数表示として、 $FV(\varphi)\subseteq\{x_1,\ldots,x_n\}$ とし、 $s(x_i)=[t_i]$ とすれば、

M_{T^H},s\models\varphi \quad\Longleftrightarrow\quad T^H\vdash\varphi[x_1:=t_1,\ldots,x_n:=t_n]

である。

証明の方針は、論理式の構造に関する帰納法である。全称量化子の逆向きでは、全閉項による例を証明することができることから全称文を導く必要がある。全称文を証明することができないと仮定すると、その否定の存在文に Henkin 証人を与えることができ、全閉項による例と矛盾する。

証明. $\varphi$ の構造に関する帰納法を用いる。

$\varphi$ が $r=u$ なら、補題 2.2と商集合の等号から

\begin{aligned} M_{T^H},s_\tau\models r=u &\Longleftrightarrow [r[\tau]]=[u[\tau]]\\ &\Longleftrightarrow r[\tau]\sim u[\tau]\\ &\Longleftrightarrow T^H\vdash r[\tau]=u[\tau] \end{aligned}

を得る。 $\varphi=R(r_1,\ldots,r_n)$ の場合も、項評価補題と関係の定義から

M_{T^H},s_\tau\models R(\bar r) \Longleftrightarrow T^H\vdash R(\bar r[\tau])

を得る。 $n=0$ も同じ定義に含まれる。

$\varphi=\neg\psi$ とする。帰納法の仮定と極大無矛盾性により

\begin{aligned} M_{T^H},s_\tau\models\neg\psi &\Longleftrightarrow M_{T^H},s_\tau\not\models\psi\\ &\Longleftrightarrow T^H\nvdash\psi[\tau]\\ &\Longleftrightarrow T^H\vdash\neg\psi[\tau]. \end{aligned}

最後の同値は§E19.11 補題 5.3 (1)と§E19.11 補題 5.3 (2)による。

$\varphi=\psi\to\chi$ とする。含意の意味と二つの帰納法の仮定により、左辺が真であることは $T^H\nvdash\psi[\tau]$ または $T^H\vdash\chi[\tau]$ と同値である。§E19.11 補題 5.3 (1)と§E19.11 補題 5.3 (3)により、同じ条件は $T^H\vdash\psi[\tau]\to\chi[\tau]$ と同値である。

$\varphi=\forall x\psi$ とする。束縛変数を必要ならアルファ変換し、 $x$ が $\tau$ で代入する閉項に現れないようにする。 $x$ 以外の自由変数を $\tau$ で置き換えた論理式を $\theta(x)$ と書く。まず $T^H\vdash\forall x\theta(x)$ とする。任意の閉項 $t$ について全称具体化の公理§E19.10 定義 1.1 (Q1)から $T^H\vdash\theta(t)$ である。帰納法の仮定により、 $M_{T^H},s_\tau[x\mapsto[t]]\models\psi$ である。項モデルの各要素に対して、その要素を同値類として表す閉項 $t$ が存在するので、 $M_{T^H},s_\tau\models\forall x\psi$ を得る。

逆に $M_{T^H},s_\tau\models\forall x\psi$ とする。任意の閉項 $t$ について帰納法の仮定から $T^H\vdash\theta(t)$ である。 $T^H\nvdash\forall x\theta(x)$ と仮定する。極大無矛盾性により $T^H\vdash\neg\forall x\theta(x)$ であり、量化子の否定に関する派生同値から $T^H\vdash\exists x\neg\theta(x)$ を得る。 Henkin 性により、Henkin 定数 $c$ が存在して

T^H\vdash\exists x\neg\theta(x)\to\neg\theta(c)

となる。modus ponens により $T^H\vdash\neg\theta(c)$ となるが、全閉項の場合から $T^H\vdash\theta(c)$ でもある。 $\theta(c)$ とその否定の二つの導出は $T^H$ の無矛盾性に反する。したがって $T^H\vdash\forall x\theta(x)$ である。

存在量化子は $\exists x\psi:=\neg\forall x\neg\psi$ と定義されるため、以上の帰納法にすでに含まれる。証人の対応を直接確認すると、 $T^H\vdash\exists x\theta(x)$ なら Henkin 性により、 $T^H\vdash\theta(c)$ を満たす閉項 $c$ が存在する。帰納法の仮定から $[c]$ が意味論的な証人になる。逆に意味論的な証人 $[t]$ が存在すれば、帰納法の仮定から $T^H\vdash\theta(t)$ であり、存在量化子導入の派生則から $T^H\vdash\exists x\theta(x)$ となる。

以上で原始結合子のすべての場合を処理した。有限変数表示では、 $s(x_i)=[t_i]$ となる閉項割当て $\tau$ を選び、残りの変数へ一つの固定閉項を割り当てる。§E19.6 定理 4.1により、 $s$ と $s_\tau$ の $FV(\varphi)$ 外での違いは真理値を変えない。▨

4 モデル存在定理

定理 4.1. $L$ を集合サイズの有限項言語、 $T\subseteq\operatorname{Sent}(L)$ を構文的に無矛盾な理論とする。このとき $T$ はモデル $M$ をもつ。さらに

|M|\le\kappa(L,T):=\max(\aleph_0,|L|,|T|)

とすることができる。

証明.§E19.11 定理 6.1により $T$ を極大無矛盾な Henkin 理論 $T^H$ へ拡大し、定義 2.1の項モデル $M_{T^H}$ を作る。 $\sigma\in T^H$ は文なので、真理補題で代入する自由変数は無い。§E19.11 補題 5.3の導出閉包と補題 3.1により

M_{T^H}\models\sigma \quad\Longleftrightarrow\quad T^H\vdash\sigma \quad\Longleftrightarrow\quad \sigma\in T^H

である。したがって $M_{T^H}\models T^H$ であり、特に $M_{T^H}\models T$ である。厳密には $M_{T^H}$ は拡大言語の構造なので、元の言語 $L$ への還元を $M$ とすれば $M\models T$ である。

§E19.11 系 2.2により $L^H$ の閉項集合は高々 $\kappa(L,T)$ 個である。項モデルの台集合はその商なので $|M|=|M_{T^H}|\le\kappa(L,T)$ である。▨

系 4.2. 任意の $L$ 理論 $T$ について、 $T$ が充足可能であることと、 $T$ が構文的に無矛盾であることは同値である。

証明. モデルをもつ理論が無矛盾であることは健全性から従う。無矛盾な理論がモデルをもつことは定理 4.1で証明した。▨

5 強完全性定理

補題 5.1. $T\subseteq\operatorname{Sent}(L)$ と $\varphi\in\operatorname{Sent}(L)$ について、 $T\nvdash\varphi$ なら $T\cup\{\neg\varphi\}$ は構文的に無矛盾である。

証明. $T\cup\{\neg\varphi\}$ が矛盾すると仮定する。演繹定理により $T\vdash\neg\varphi\to\bot$ である。古典命題論理では $(\neg\varphi\to\bot)\to\varphi$ を導出することができるので、modus ponens により $T\vdash\varphi$ となり、 $T\nvdash\varphi$ という仮定に反する。▨

定理 5.2. 集合サイズの有限項言語 $L$ 、任意の理論 $T\subseteq\operatorname{Sent}(L)$ 、任意の文 $\varphi\in\operatorname{Sent}(L)$ について

T\models\varphi \quad\Longleftrightarrow\quad T\vdash\varphi

が成り立つ。

証明の方針は、健全性で右から左を示し、左から右は対偶を用いることである。 $T\nvdash\varphi$ なら、 $T\cup\{\neg\varphi\}$ のモデルを構成し、 $T\models\varphi$ を否定する。

証明. $T\vdash\varphi$ なら、一階 Hilbert 系の健全性により $T\models\varphi$ である。

逆向きの対偶を示す。 $T\nvdash\varphi$ とする。補題 5.1により $T\cup\{\neg\varphi\}$ は構文的に無矛盾である。定理 4.1を適用すると、ある $L$ 構造 $M$ が存在して

M\models T\cup\{\neg\varphi\}

となる。したがって $M\models T$ かつ $M\not\models\varphi$ であり、 $T\not\models\varphi$ である。対偶により $T\models\varphi$ なら $T\vdash\varphi$ である。▨

注意 5.3.定理 5.2では、言語 $L$ と理論 $T$ が可算であることを仮定しない。濃度は Henkin 言語、閉項集合、および構成されるモデルの大きさを評価するときにだけ現れる。意味論的帰結と形式的導出の一致そのものは、任意の集合サイズの有限項言語と任意の理論について成り立つ。

6 項モデルの具体的な読み方

例 6.1. $a,b$ を定数記号、 $f$ を一項関数記号とし、極大無矛盾な Henkin 理論 $T^H$ が

T^H\vdash a=b, \qquad T^H\vdash\forall x\,f(x)=x

を満たすとする。項モデルでは $[a]=[b]$ である。また全称具体化の公理§E19.10 定義 1.1 (Q1)から $T^H\vdash f(a)=a$ なので

f^{M_{T^H}}([a])=[f(a)]=[a]

である。項の文字列が異なっていても、理論が等しいと証明する項は同じモデル要素を表す。

7 演習

問題 7.1. 次の 1 と 2 では、 $L'$ 理論 $S$ が極大無矛盾であるとき、定義 1.1と定義 2.1の $T^H$ を $S$ に、 $L^H$ を $L'$ に置き換えて、 $L'$ の閉項の関係 $\sim_S$ と構造 $M_S$ を同じ式で定める。 $\mathcal M$ が $L'$ 構造のとき、 $\operatorname{Th}(\mathcal M)$ は $\mathcal M$ で真な $L'$ 文の全体である。

$L'=\{c,f\}$ を定数記号 $c$ と一項関数記号 $f$ からなる言語とし、台集合 $\{0,1\}$ 上で $c^{\mathcal M}=0$ 、 $f^{\mathcal M}(a)=1-a$ と定めた構造を $\mathcal M$ とする。 $S=\operatorname{Th}(\mathcal M)$ が極大無矛盾な Henkin 理論であることを示せ。さらに、閉項 $f^n(c)$ （ $f$ を $n$ 回適用した項）について $f^n(c)\sim_Sf^m(c)$ であることと $n-m$ が偶数であることが同値であることを示し、 $M_S$ が $\mathcal M$ と同型であることを示せ。
$L'=\{c,P\}$ を定数記号 $c$ と一項関係記号 $P$ からなる言語とし、台集合 $\{0,1\}$ 上で $c^{\mathcal M}=0$ 、 $P^{\mathcal M}=\{0\}$ と定めた構造を $\mathcal M$ とする。 $S=\operatorname{Th}(\mathcal M)$ は極大無矛盾であるが Henkin 理論でないことを示し、 $M_S\models\forall x\,P(x)$ かつ $S\nvdash\forall x\,P(x)$ であることを示せ。
$R$ を二項関係記号とし、 $x\neq y$ とする。定理 5.2を用いて $\vdash\exists y\forall x\,R(x,y)\to\forall x\exists y\,R(x,y)$ を示せ。また、 $\vdash\forall x\exists y\,R(x,y)\to\exists y\forall x\,R(x,y)$ ではないことを示せ。
二項関係記号 $<$ だけからなる言語 $L$ と、 $L$ 構造 $(\R,<)$ の理論 $T=\operatorname{Th}((\R,<))$ を考える。定理 4.1を用いて、 $T$ が可算無限な台集合をもつモデル $M$ をもつことを示せ。さらに、 $M$ と $(\R,<)$ が同じ $L$ 文を満たすが同型でないことを示せ。

解答 (確認問題の解答).

1 と 2 で共通に用いる事実を先に示す。 $L'$ 構造 $\mathcal M$ について $S=\operatorname{Th}(\mathcal M)$ とおく。 $\mathcal M\models S$ であるから、§E19.10 系 7.3により $S$ は構文的に無矛盾である。 $S\vdash\sigma$ ならば健全性により $\mathcal M\models\sigma$ 、すなわち $\sigma\in S$ である。文 $\sigma\notin S$ ならば $\mathcal M\models\neg\sigma$ であるから $\neg\sigma\in S$ であり、 $S\cup\{\sigma\}$ からは $\sigma$ と $\neg\sigma$ がともに導出されるので、 $S\cup\{\sigma\}$ は構文的に無矛盾でない。よって $S$ は極大無矛盾であり、文 $\sigma$ について $S\vdash\sigma$ と $\mathcal M\models\sigma$ は同値である。

前段により $S$ は極大無矛盾である。閉項 $f^n(c)$ の値は、 $n$ が偶数ならば $0$ 、奇数ならば $1$ である。 $FV(\varphi)\subseteq\{x\}$ を満たす論理式 $\varphi(x)$ を取る。 $\mathcal M\models\exists x\varphi(x)$ ならば、 $\mathcal M,s[x\mapsto a]\models\varphi$ を満たす $a\in\{0,1\}$ が存在する。 $a=0$ ならば $t=c$ 、 $a=1$ ならば $t=f(c)$ とおくと $t$ の値は $a$ であり、§E19.7 系 5.3により $\mathcal M\models\varphi(t)$ である。 $\mathcal M\not\models\exists x\varphi(x)$ ならば $t=c$ とおく。いずれの場合も $\mathcal M\models\exists x\varphi(x)\to\varphi(t)$ であるから、この文は $S$ に属し、 $S\vdash\exists x\varphi(x)\to\varphi(t)$ である。よって $S$ は Henkin 理論である。

前段の同値により、 $f^n(c)\sim_Sf^m(c)$ であることは $\mathcal M\models f^n(c)=f^m(c)$ 、すなわち二つの閉項の値が等しいことと同値であり、これは $n$ と $m$ の偶奇が一致すること、すなわち $n-m$ が偶数であることと同値である。 $L'$ の閉項は $f^n(c)$ （ $n\geq0$ ）の形のものだけであるから、 $M_S$ の台集合は $\{[c],[f(c)]\}$ であり、この二元は異なる。写像 $h:M_S\to\{0,1\}$ を $h([f^n(c)])$ を $f^n(c)$ の値とすることで定めると、前の同値により $h$ は代表元によらず、全単射である。 $h(c^{M_S})=h([c])=0=c^{\mathcal M}$ であり、 $h(f^{M_S}([f^n(c)]))=h([f^{n+1}(c)])=1-h([f^n(c)])=f^{\mathcal M}(h([f^n(c)]))$ であるから、 $h$ は同型である。
前段により $S$ は極大無矛盾である。 $L'$ の閉項は $c$ だけである。 $\varphi(x)=\neg P(x)$ とすると、 $1\notin P^{\mathcal M}$ であるから $\mathcal M\models\exists x\neg P(x)$ であり、 $0\in P^{\mathcal M}$ であるから $\mathcal M\not\models\neg P(c)$ である。よって $\mathcal M\not\models\exists x\neg P(x)\to\neg P(c)$ であり、前段の同値により $S\nvdash\exists x\neg P(x)\to\neg P(c)$ である。閉項は $c$ だけであるから $S$ は Henkin 理論でない。

$M_S$ の台集合は $\{[c]\}$ の一元集合であり、 $\mathcal M\models P(c)$ から $S\vdash P(c)$ であるので $P^{M_S}=\{[c]\}$ である。台集合のただ一つの元が $P^{M_S}$ に属するので $M_S\models\forall x\,P(x)$ である。一方、 $\mathcal M\not\models\forall x\,P(x)$ であるから、前段の同値により $S\nvdash\forall x\,P(x)$ である。したがって、Henkin 性をもたない極大無矛盾な理論では、補題 3.1の同値は全称量化子の場合に $M_S\models\forall x\psi$ から導出可能性を導く向きで成り立たない。
構造 $\mathcal M$ と割当て $s$ を取り、 $\mathcal M,s\models\exists y\forall x\,R(x,y)$ とする。 $\mathcal M,s[y\mapsto b]\models\forall x\,R(x,y)$ を満たす $b$ が存在する。任意の $a$ について、 $x\neq y$ であるから $s[y\mapsto b][x\mapsto a]=s[x\mapsto a][y\mapsto b]$ であり、 $\mathcal M,s[x\mapsto a][y\mapsto b]\models R(x,y)$ である。よって $\mathcal M,s[x\mapsto a]\models\exists y\,R(x,y)$ であり、 $\mathcal M,s\models\forall x\exists y\,R(x,y)$ である。したがって文 $\exists y\forall x\,R(x,y)\to\forall x\exists y\,R(x,y)$ は $\varnothing$ の意味論的帰結であり、定理 5.2を $T=\varnothing$ に適用すると $\vdash\exists y\forall x\,R(x,y)\to\forall x\exists y\,R(x,y)$ である。

台集合 $\{0,1\}$ 上で $R^{\mathcal M}=\{(0,0),(1,1)\}$ とした構造 $\mathcal M$ では、各 $a$ について $(a,a)\in R^{\mathcal M}$ であるから $\mathcal M\models\forall x\exists y\,R(x,y)$ である。一方、各 $b$ について $(1-b,b)\notin R^{\mathcal M}$ であるから $\mathcal M\not\models\exists y\forall x\,R(x,y)$ である。よって $\forall x\exists y\,R(x,y)\to\exists y\forall x\,R(x,y)$ は $\mathcal M$ で偽であり、健全性によりこの文は導出可能でない。
$(\R,<)\models T$ であるから、§E19.10 系 7.3により $T$ は構文的に無矛盾である。 $L$ は一つの記号からなり、§E19.11 補題 2.1により $|T|\leq|\operatorname{Sent}(L)|\leq\aleph_0$ であるから、定理 4.1により $|M|\leq\max(\aleph_0,|L|,|T|)=\aleph_0$ を満たすモデル $M\models T$ が存在する。各正の整数 $n$ について、相異なる $n$ 個の元が存在することを述べる文
$\exists x_1\cdots\exists x_n\bigwedge_{1\leq i<j\leq n}\neg(x_i=x_j)$
は $(\R,<)$ で真であるから $T$ に属し、 $M$ でも真である。よって $M$ は無限集合であり、可算無限である。

$L$ 文 $\sigma$ について、 $(\R,<)\models\sigma$ ならば $\sigma\in T$ であるから $M\models\sigma$ である。 $(\R,<)\not\models\sigma$ ならば $\neg\sigma\in T$ であるから $M\not\models\sigma$ である。よって $M$ と $(\R,<)$ は同じ文を満たす。同型 $h:(\R,<)\to M$ が存在すると仮定すると、 $h$ は全単射であり、 $M$ は高々可算であるから、 $h$ と単射 $M\to\N$ の合成は単射 $\R\to\N$ となり、§E1.19 定理 3.3に反する。したがって $M$ と $(\R,<)$ は同型でない。

▨

§E19.12項モデルと完全性定理