Gödelの完全性定理

同義語：ゲーデルの完全性定理完全性定理Gödel's completeness theorem

概要

意味論と証明論を結ぶ定理

一階述語論理には、推論が正しいということを表す二つの関係がある。文の集合 $\Gamma$ のすべてのモデルで文 $\varphi$ が真になることを
$$ \Gamma\models\varphi $$
と書く。これは意味論的帰結である。一方、固定した形式的証明体系で、$\Gamma$ を前提として有限の証明により $\varphi$ を導けることを
$$ \Gamma\vdash\varphi $$
と書く。これは構文論的な証明可能性である。
証明できる文がすべてのモデルで真であるという向き
$$ \Gamma\vdash\varphi\quad\Longrightarrow\quad\Gamma\models\varphi $$
は健全性定理と呼ばれる。Gödelの完全性定理はその逆向きも成り立つことを述べる。したがって、意味論的に強制される結論を、有限の記号操作からなる証明が一つ残らず捉える。
本稿では通常のZFC集合論を背景として、等号を含む集合サイズの一階言語 $L$ を固定し、構造の台集合は空でないとする。また、健全な標準的一階述語論理の証明体系を固定する。この体系では演繹定理、背理法、等号の公理、存在量化子の導入、汎化が使えるものとする。$\Gamma$ は $L$ の文の集合、$\varphi$ と $\psi$ は $L$ の文を表す。自由変数をもつ論理式について述べる場合は、その普遍閉包を取る流儀を採る。

基本概念

意味論的帰結と証明可能性

$L$ 構造 $\mathcal M$ が $\Gamma$ のすべての文を充足するとき、$\mathcal M$ を $\Gamma$ のモデルという。$\Gamma$ の任意のモデルが $\varphi$ を充足するとき、$\Gamma\models\varphi$ と書く。
$\Gamma$ の文と論理的公理から始め、推論規則を有限回適用して $\varphi$ に至る証明があるとき、$\Gamma\vdash\varphi$ と書く。

無矛盾性

文の集合 $\Gamma$ が矛盾するとは、ある文 $\psi$ について
$$ \Gamma\vdash\psi, \qquad \Gamma\vdash\lnot\psi $$
がともに成り立つことをいう。矛盾しないとき、$\Gamma$ は無矛盾であるという。

矛盾の定義には、一つの固定した矛盾式 $\bot$ が証明できるという同値な形もある。標準的な古典論理では爆発律が成り立つため、$\Gamma$ が矛盾すれば任意の文が $\Gamma$ から証明できる。
完全性の直感は、モデルを一つももたない前提集合は、すでに有限の形式的矛盾を含むということである。意味論側ではすべてのモデルを調べる必要があるように見えるが、構文論側の証明は常に有限である。この有限性が、後にコンパクト性定理を生む。

Gödelの完全性定理

任意の文の集合 $\Gamma$ と文 $\varphi$ に対して、
$$ \Gamma\models\varphi \quad\Longleftrightarrow\quad \Gamma\vdash\varphi $$
が成り立つ。

右から左は健全性定理である。完全性定理という名で特に指すのは、左から右の
$$ \Gamma\models\varphi \quad\Longrightarrow\quad \Gamma\vdash\varphi $$
である。$\Gamma=\emptyset$ とすれば、すべての構造で真な文は証明可能であるという弱い形を得る。一般の $\Gamma$ を許す形は強完全性とも呼ばれる。標準的な証明は、無矛盾な文集合からモデルを構成するHenkinの方法に基づく End01 CK90。

証明が使う二つの補題

証明の有限性

$\Gamma\vdash\varphi$ ならば、$\Gamma$ の有限部分集合 $\Gamma_0$ で $\Gamma_0\vdash\varphi$ を満たすものが存在する。

証明

$\Gamma$ からの $\varphi$ の証明を一つ固定する。証明は有限列であり、その各行は論理的公理、$\Gamma$ の元、または先行する有限個の行への推論規則の適用である。この有限列に実際に現れる $\Gamma$ の元を集めて $\Gamma_0$ とする。$\Gamma_0$ は有限であり、同じ証明列が $\Gamma_0\vdash\varphi$ を示す。

モデル存在定理は、一般の集合サイズの言語について「無矛盾な文の集合はモデルをもつ」と述べる。これが完全性定理の核心となる。一般版は CK90 を外部入力とし、ここでは構成の全体が見える可算言語版を証明する。通常のZFC集合論では、一般版も列挙を整列順序に沿う超限帰納へ置き換えることで得られる。

モデル存在定理（可算言語）

$L$ が可算で、$\Gamma$ が無矛盾な $L$ の文集合ならば、$\Gamma$ は高々可算なモデルをもつ。

証明（可算言語）

$\Gamma$ を無矛盾とする。可算個の新しい定数を加えた言語を $L^H$ とする。$L^H$ の存在文を
$$ \exists x\,\theta_0(x),\ \exists x\,\theta_1(x),\ \exists x\,\theta_2(x),\ldots $$
と列挙する。各 $n$ について、論理式 $\theta_n$ にも、それまでに構成した理論にも現れない新定数 $c_n$ を選び、証人公理
$$ \exists x\,\theta_n(x)\to\theta_n(c_n) $$
を加える。
各段階で $\theta_n$ に現れる定数も、それまでに証人として選んだ定数も有限個なので、可算無限個用意した新定数の中からこの条件を満たす $c_n$ を選べる。
この操作は無矛盾性を保つ。実際、新定数 $c$ を含まない無矛盾な理論 $T$ に証人公理 $\exists x\,\theta(x)\to\theta(c)$ を加えた結果が矛盾したと仮定する。演繹定理と古典命題論理により、$T$ から
$$ \exists x\,\theta(x) \quad\text{かつ}\quad \lnot\theta(c) $$
が導かれる。$c$ は $T$ に現れない新定数なので、定数の一般化により $T\vdash\forall x\,\lnot\theta(x)$ も得る。これは $T\vdash\exists x\,\theta(x)$ と矛盾する。したがって各段階は無矛盾であり、その合併 $T_H$ も無矛盾である。もし合併が矛盾すれば、証明の有限性により有限段階ですでに矛盾するからである。
次に $L^H$ のすべての文を $\sigma_0,\sigma_1,\ldots$ と列挙し、$T_H$ を極大無矛盾理論 $T^*$ へ拡大する。$n$ 番目の段階で、それまでの理論に $\sigma_n$ を加えて無矛盾なら $\sigma_n$ を加え、そうでなければ $\lnot\sigma_n$ を加える。後者も無矛盾である。両方を加えると矛盾するなら、演繹定理と背理法によって元の理論自身が矛盾するからである。有限性により合併 $T^*$ は無矛盾であり、任意の文 $\sigma$ について $\sigma\in T^*$ または $\lnot\sigma\in T^*$ が成り立つ。また、$T^*$ は証人公理をすべて含む。

&&&lem 極大無矛盾理論の演繹閉性 [lem-godel-completeness-deductive-closure]
任意の $L^H$ の文 $\sigma$ について、
$$ T^*\vdash\sigma \quad\Longrightarrow\quad \sigma\in T^* $$
が成り立つ。

証明

$T^*\vdash\sigma$ かつ $\sigma\notin T^*$ と仮定する。$T^*$ はすべての文を決定するので、後者から $\lnot\sigma\in T^*$ を得る。理論に属する文はその理論から証明できるから $T^*\vdash\lnot\sigma$ でもあり、$T^*$ の無矛盾性に反する。したがって $\sigma\in T^*$ である。

$L^H$ の閉項全体を取り、
$$ s\sim t \quad:\Longleftrightarrow\quad T^*\vdash s=t $$
と定める。等号の公理により、これは同値関係であり、関数記号と関係記号に関する合同関係でもある。閉項 $t$ の同値類を $[t]$ と書く。閉項の同値類を台集合とする構造 $\mathcal M_{T^*}$ を
$$ f^{\mathcal M_{T^*}}([t_1],\ldots,[t_n]) :=[f(t_1,\ldots,t_n)] $$
および
$$ \mathcal M_{T^*}\models R([t_1],\ldots,[t_n]) \quad:\Longleftrightarrow\quad T^*\vdash R(t_1,\ldots,t_n) $$
で定める。合同性により、これらは代表元によらず定まる。
論理式の複雑さに関する帰納法で、自由変数が $x_1,\ldots,x_m$ に含まれる任意の論理式 $\alpha$ と閉項 $t_1,\ldots,t_m$ について真理補題
$$ \mathcal M_{T^*}\models\alpha([t_1],\ldots,[t_m]) \quad\Longleftrightarrow\quad T^*\vdash\alpha(t_1,\ldots,t_m) $$
を示す。右辺では自由変数へ閉項を代入する。原子式の場合は構造の定義そのものである。否定と論理結合子の場合は、$T^*$ の極大無矛盾性と古典命題論理から従う。
存在量化子の場合を詳しく確認する。$T^*\vdash\exists x\,\theta(x)$ ならば、上の演繹閉性により $\exists x\,\theta(x)\in T^*$ である。対応する証人公理も $T^*$ に属するので、modus ponensにより、ある $c_n$ について $T^*\vdash\theta(c_n)$ を得る。帰納法の仮定から $[c_n]$ が存在文の証人になる。逆に、$\mathcal M_{T^*}\models\exists x\,\theta(x)$ ならば、台集合の定義により、ある閉項 $t$ の同値類 $[t]$ が $\theta$ を満たす。帰納法の仮定により $T^*\vdash\theta(t)$ であり、存在量化子の導入によって $T^*\vdash\exists x\,\theta(x)$ となる。これで存在量化子の場合が閉じ、真理補題が従う。
$\Gamma\subseteq T^*$ なので、真理補題により $\mathcal M_{T^*}\models\Gamma$ である。最後に $L^H$ の新定数を忘れれば、$\Gamma$ の $L$ 構造のモデルが得られる。

完全性の証明

&&&prf 証明 [prf-godel-completeness-main]
健全性により、$\Gamma\vdash\varphi$ ならば $\Gamma\models\varphi$ である。
逆に $\Gamma\models\varphi$ と仮定する。$\Gamma\cup\{\lnot\varphi\}$ が無矛盾なら、一般のモデル存在定理 CK90 により、そのモデル $\mathcal M$ が存在する。このとき $\mathcal M\models\Gamma$ なので、仮定から $\mathcal M\models\varphi$ である。一方、$\mathcal M\models\lnot\varphi$ でもあり、充足の定義に反する。したがって $\Gamma\cup\{\lnot\varphi\}$ は矛盾する。
演繹定理により、矛盾から使った文を $\psi$ とすれば
$$ \Gamma\vdash\lnot\varphi\to\psi, \qquad \Gamma\vdash\lnot\varphi\to\lnot\psi $$
である。古典命題論理のトートロジー
$$ (\lnot\varphi\to\psi) \to \bigl((\lnot\varphi\to\lnot\psi)\to\varphi\bigr) $$
とmodus ponensから $\Gamma\vdash\varphi$ を得る。

同値な形と帰結

完全性とモデル存在

健全性を満たす標準的証明体系について、次の二つは同値である。

$\Gamma\models\varphi$ ならば $\Gamma\vdash\varphi$ である。
無矛盾な文集合はモデルをもつ。

証明

2から1は主定理の証明で示した。1を仮定し、無矛盾な $\Gamma$ がモデルをもたないと仮定する。モデルが一つもないので、意味論的帰結の定義から任意の文 $\psi$ について $\Gamma\models\psi$ が空虚に成り立つ。したがって $\Gamma\models\psi$ と $\Gamma\models\lnot\psi$ がともに成り立つ。1により $\Gamma\vdash\psi$ かつ $\Gamma\vdash\lnot\psi$ となり、無矛盾性に反する。よって $\Gamma$ はモデルをもつ。

コンパクト性定理

文集合 $\Gamma$ のすべての有限部分集合がモデルをもつならば、$\Gamma$ 自身もモデルをもつ。

証明

対偶を示す。$\Gamma$ がモデルをもたなければ、一般のモデル存在定理の対偶により $\Gamma$ は矛盾する。ある文 $\psi$ について $\Gamma\vdash\psi$ かつ $\Gamma\vdash\lnot\psi$ である。証明の有限性により、この二つの証明で使われる前提をすべて含む有限集合 $\Gamma_0\subseteq\Gamma$ が存在する。もし $\Gamma_0$ がモデル $\mathcal M$ をもてば、健全性から $\mathcal M\models\psi$ かつ $\mathcal M\models\lnot\psi$ となり不可能である。したがって $\Gamma_0$ はモデルをもたない。

完全性定理は、意味論的なモデルの存在問題を構文論的な無矛盾性へ移す。コンパクト性定理はさらに、無限個の公理からなる理論の有限部分がすべて実現可能なら、全体も同時に実現可能であると保証する。モデル理論では、この原理を用いて無限モデルや非標準モデルを構成する。

例と反例

妥当な文と証明可能な文

空でない構造だけを考える通常の一階意味論では、
$$ \forall x\,P(x)\to\exists x\,P(x) $$
は任意の構造で真である。完全性定理により、この文は固定した標準的証明体系で証明可能である。
一方、
$$ \exists x\,P(x)\to\forall x\,P(x) $$
は妥当でない。台集合を $\{0,1\}$ とし、$P$ を $\{0\}$ と解釈すれば、前件は真で後件は偽になる。健全性により、この文は証明可能でもない。

健全だが完全でない証明体系

公理も推論規則も一つも持たない形式体系を考える。この体系では何も証明できないので、「証明できる文は妥当である」という健全性は空虚に成り立つ。しかし、例えば等号を含む言語の文 $\forall x\,x=x$ は任意の構造で真であるのに証明できない。したがって、この体系は完全ではない。
これは、完全性定理が任意の形式体系について成り立つのではなく、古典一階述語論理を正しく表現する十分な公理と推論規則を備えた標準的証明体系についての定理であることを示す。

近接概念との区別

命題論理の完全性

命題論理にも、付値に関する意味論的帰結と形式的証明可能性が一致する完全性定理がある。命題論理では極大無矛盾集合から付値を直接作れるのに対し、一階述語論理では量化子の証人を確保するHenkin構成と項モデルが必要になる。本稿は一階述語論理のGödelの完全性定理を所有し、命題論理版は完全性定理(命題論理)が所有する。

理論の完全性と不完全性定理

一階理論 $T$ が完全であるとは、任意の文 $\varphi$ について $T\vdash\varphi$ または $T\vdash\lnot\varphi$ が成り立つことをいう。これは証明体系の意味論的完全性とは別の概念である。
Gödelの不完全性定理も完全性定理と矛盾しない。不完全性定理は、十分な算術を含む適切な帰納的理論 $T$ には、$T\vdash\varphi$ も $T\vdash\lnot\varphi$ も成り立たない文があると述べる。完全性定理によれば、そのとき $T\cup\{\varphi\}$ と $T\cup\{\lnot\varphi\}$ はそれぞれモデルをもち得る。すなわち、$T$ のすべてのモデルで同じ真理値を取ることが強制されていないのであり、論理体系の完全性は保たれている。