# 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由

> 一階述語論理の構文と意味論を定義し、ヒルベルト流の証明体系の健全性とゲーデルの完全性定理をヘンキンの構成で証明する。コンパクト性定理、レーヴェンハイム–スコーレムの定理、非標準モデルを導く。
> https://rikai.mugen-giken.com/mathematics/logic-and-type-theory/first-order-logic

## 0. この記事の要点

数学の本にある「公理から従う」という言い回しを、誰が確かめても同じ判定になる形で定めたい、という話です。例えば群の公理から「単位元は一意」を導くとき、決まった規則で記号を並べて示す方法と、群のあらゆる例で成り立つことを確かめる方法の二通りが考えられます。この記事では、一階述語論理の範囲でこの二つが完全に一致することを示します。読み終えると、「証明できる」と「真である」が同じ意味になる理由と、そこから出るコンパクト性や非標準モデルといった帰結が分かります。

- **一階述語論理**は、数学の命題を書くための形式言語（項と論理式）と、その意味（構造における充足）と、機械的に検査できる証明の三つ組です。この記事ではそれぞれを定義し、「$\Gamma$ から $\varphi$ が証明できる」($\Gamma\vdash\varphi$) と「$\Gamma$ のすべてのモデルで $\varphi$ が真」($\Gamma\models\varphi$) を比べます。
- **健全性**（<Ref to="thm-soundness" />）：$\Gamma\vdash\varphi$ ならば $\Gamma\models\varphi$。証明の長さに関する帰納法で示します。
- **ゲーデルの完全性定理**（<Ref to="thm-completeness" />、可算言語）：無矛盾な理論はモデルをもつ。ヘンキンの構成で、理論に「証人」（「〜を満たさない元がある」ときの具体例の名前）となる定数を足し、極大無矛盾（これ以上どの文を足しても矛盾する）にして、閉項（変数を含まない項）そのものからモデルを組み立てます。
- 完全性から**コンパクト性定理**（<Ref to="thm-compactness" />）と**レーヴェンハイム–スコーレムの定理**（<Ref to="thm-ls" />）が従います。有限個ずつ満たせる条件の族は一度に満たせること、一階の理論は無限の構造の大きさを区別できないことが、ここから分かります。
- 完全性定理は「公理から導く」の意味を確定させます。数学の命題が「ある公理系から導ける」とは、「その公理系のあらゆるモデルで成り立つ」と同じことです。一階の枠内では、証明という有限の対象で真理（の一部）を捉え切れます。
- この記事はテーマ「数理論理学と型理論」の最初の章です。次に計算可能性、公理的集合論、ラムダ計算を経て、カリー＝ハワード対応、依存型理論、Lean へ進みます（§1）。

<Aside type="tip" title="この記事で使う事前知識">

- **述語**: 「$x$ は偶数である」のように、対象を入れると真か偽かが決まる文。→ [述語](/mathematics/foundations/sets-and-logic#def-predicate)
- **可算**: 自然数と一対一に対応させて並べられる、という性質。→ [可算](/mathematics/foundations/cardinality-and-infinity#def-countable)
- **対偶**: 「$P$ ならば $Q$」と「$Q$ でないならば $P$ でない」は同じ内容である、という関係。→ [対偶](/mathematics/foundations/proof-techniques#def-converse-contrapositive)
- **同値関係**: 反射律・対称律・推移律を満たす関係。同じ類にまとめるのに使う。→ [同値関係](/mathematics/foundations/equivalence-relations#def-equivalence)
- **極大元**: それより真に大きい元が（順序の中に）存在しない元。→ [極大元](/mathematics/foundations/axiom-of-choice-zorn#def-bounds)

</Aside>

## 1. 動機：「公理から導く」を定理にする

数学の本には「補題 3 より明らか」「公理から従う」といった言い回しが並びます。この「従う」とは何でしょうか。人間の読者が納得するという意味なら、納得の基準は人によって違います。私たちが欲しいのは、誰が検査しても同じ判定になる基準です。

そのために数学者たちは二つの道を用意しました。一つは**証明**の道で、公理から出発し、決められた推論規則だけを有限回使って結論に至る記号列を考えます。証明であるかどうかは、記号の形だけを見て機械的に検査できます。もう一つは**真理**の道で、公理を満たすあらゆる数学的対象（**モデル**）を考え、そのすべてで結論が成り立つかを問います。群の公理から「単位元は一意」が従う、というとき、私たちは通常この意味で「従う」を理解しています。

二つの道が同じ命題を拾うのか、というのが自然な問いです。証明が見つかれば結論は常に真でしょう（健全性）。逆に、すべてのモデルで真な命題には、必ず証明があるのでしょうか。一階述語論理については、**ある**、というのがゲーデル (1930) の答えです。この記事の中心の定理です。

### 1.1. このテーマの見通し

この記事は新しいテーマ「数理論理学と型理論」の最初の章です。テーマ全体は次のように進みます。

1. **一階述語論理と完全性定理**（本章）。証明と真理の二つの「従う」が一致することを示し、「公理から導く」を定める終点とする。
2. **計算可能性**。「機械的に検査できる」「アルゴリズムで判定できる」とは何かをチューリング機械で定義する。停止問題は解けないこと、そして証明の検査が機械的であっても証明の発見は機械的にできないことを示す。
3. **公理的集合論**。ZFC の公理から、数学の対象（数、関数、空間）がすべて集合として作られること、選択公理の同値形、連続体仮説が公理から独立であることを見る。
4. **不完全性定理**（[ゲーデルの不完全性定理](/mathematics/logic-and-type-theory/incompleteness-theorems)）。完全性定理と対になって、「証明の力」の限界を決める。
5. **型なしラムダ計算**。計算をもう一つの形（関数の適用と置換）で捉え直す。
6. **単純型付きラムダ計算とカリー＝ハワード対応**。「命題 = 型」「証明 = プログラム」という対応を定理として示す。
7. **依存型理論**。型が値に依存できるようにして、述語論理まで含む論理と数学の体系を一つの型理論で与える。
8. **証明支援系 Lean**。依存型理論を土台とする証明検査器が、どのように「この証明は正しい」と判定するかを分解する。そのうえで Rikai の定理の形式化へ進む。

この道筋では、証明が記号列から始まり、プログラムになり、型検査の対象になっていきます。出発点として必要なのは、証明を数学の対象として扱う足場、すなわち一階述語論理です。以下、記号を厳密に導入し、定理の証明を最後まで書きます。

## 2. 準備：一階の言語

### 2.1. 言語、項、論理式

<Definition id="def-language" title="一階の言語">

**言語** $L$ とは、次の三種類の記号の（可算または非可算の）集合の組である。

- **定数記号**の集合。
- 各 $n\ge1$ について、**$n$ 変数関数記号**の集合。
- 各 $n\ge1$ について、**$n$ 変数関係記号**の集合。

これらとは別に、可算無限個の**変数** $x,y,z,x_1,x_2,\ldots$、等号 $=$、論理記号 $\neg,\to,\forall$、括弧を用意する。等号と論理記号は言語に依らず常に使える。

</Definition>

例えば群の言語は、定数記号 $e$、2 変数関数記号 $\cdot$、1 変数関数記号 ${}^{-1}$ からなります。算術の言語は、定数 $0$、1 変数関数 $S$、2 変数関数 $+,\times$、2 変数関係 $<$ です。

<Definition id="def-formula" title="項と論理式">

$L$ の**項**を次の規則で帰納的に定める。

1. 変数と定数記号は項である。
2. $f$ が $n$ 変数関数記号で $t_1,\ldots,t_n$ が項ならば、$f(t_1,\ldots,t_n)$ は項である。

$L$ の**論理式**を次で帰納的に定める。

1. $t_1,t_2$ が項ならば、$t_1=t_2$ は論理式（**原子論理式**）である。$R$ が $n$ 変数関係記号で $t_1,\ldots,t_n$ が項ならば、$R(t_1,\ldots,t_n)$ も原子論理式である。
2. $\varphi,\psi$ が論理式ならば、$\neg\varphi$ と $(\varphi\to\psi)$ は論理式である。
3. $\varphi$ が論理式で $x$ が変数ならば、$\forall x\,\varphi$ は論理式である。

$\varphi\vee\psi$、$\varphi\wedge\psi$、$\varphi\leftrightarrow\psi$、$\exists x\,\varphi$ は、それぞれ $\neg\varphi\to\psi$、$\neg(\varphi\to\neg\psi)$、$(\varphi\to\psi)\wedge(\psi\to\varphi)$、$\neg\forall x\,\neg\varphi$ の略記とする。

</Definition>

論理式 $\varphi$ に含まれる記号 $\neg,\to,\forall$ の個数を $\varphi$ の**複雑さ** $\mathrm{c}(\varphi)$ と呼びます。

変数 $x$ の出現が $\forall x$ の作用範囲の外にあるとき、その出現は**自由**であるといい、$\varphi$ に自由に現れる変数の集合を $\mathrm{FV}(\varphi)$ と書きます。$\mathrm{FV}(\varphi)=\varnothing$ の論理式を**閉論理式**（**文**）、文の集合を**理論**と呼びます。

**代入**を定めます。$\varphi[t/x]$ は、$\varphi$ の中の $x$ の自由な出現をすべて項 $t$ に置き換えた論理式です。ただし $t$ に現れる変数が代入先で $\forall$ に捕まってしまうと意味が変わります。例えば $\varphi=\exists y\,(y\ne x)$ に $t=y$ を代入すると $\exists y\,(y\ne y)$ になって、意図と変わります。$x$ の自由な出現のどれもが、$t$ に現れる変数についての量化子の作用範囲に入っていないとき、$t$ は $\varphi$ の中で $x$ に**代入可能**であるといいます。要するに、代入した項の変数が量化子に巻き込まれて、別の変数を指すようになる事故を避けるための条件です。以後、代入 $\varphi[t/x]$ を書くときは代入可能性を仮定します。$t$ が閉項（変数を含まない項）ならば、常に代入可能です。

## 3. 意味論：構造と充足

<Definition id="def-structure" title="構造と充足">

$L$ の**構造** $\mathcal{M}$ とは、空でない集合 $M$（**領域**）と、次の解釈の組である。

- 各定数記号 $c$ に元 $c^{\mathcal{M}}\in M$。
- 各 $n$ 変数関数記号 $f$ に関数 $f^{\mathcal{M}}:M^n\to M$。
- 各 $n$ 変数関係記号 $R$ に部分集合 $R^{\mathcal{M}}\subseteq M^n$。

変数への**割り当て**とは、写像 $s:\{\text{変数}\}\to M$ である。項 $t$ の値 $t^{\mathcal{M}}[s]\in M$ を、変数 $x$ には $s(x)$、定数 $c$ には $c^{\mathcal{M}}$、$f(t_1,\ldots,t_n)$ には $f^{\mathcal{M}}(t_1^{\mathcal{M}}[s],\ldots,t_n^{\mathcal{M}}[s])$ と定める。

論理式 $\varphi$ について、**$\mathcal{M}$ は $s$ のもとで $\varphi$ を満たす**($\mathcal{M}\models\varphi[s]$) を次で定める。

1. $\mathcal{M}\models(t_1=t_2)[s]$ $\iff$ $t_1^{\mathcal{M}}[s]=t_2^{\mathcal{M}}[s]$（領域の元として等しい）。
2. $\mathcal{M}\models R(t_1,\ldots,t_n)[s]$ $\iff$ $(t_1^{\mathcal{M}}[s],\ldots,t_n^{\mathcal{M}}[s])\in R^{\mathcal{M}}$。
3. $\mathcal{M}\models\neg\varphi[s]$ $\iff$ $\mathcal{M}\not\models\varphi[s]$。
4. $\mathcal{M}\models(\varphi\to\psi)[s]$ $\iff$ $\mathcal{M}\not\models\varphi[s]$ または $\mathcal{M}\models\psi[s]$。
5. $\mathcal{M}\models\forall x\,\varphi\,[s]$ $\iff$ $M$ の**すべての**元 $a$ について $\mathcal{M}\models\varphi[s(x\mapsto a)]$。ここで $s(x\mapsto a)$ は $x$ だけ値を $a$ に替えた割り当てである。

</Definition>

論理式の充足は $\mathrm{FV}(\varphi)$ の変数への割り当てだけで決まります（$s,s'$ が $\mathrm{FV}(\varphi)$ 上で一致すれば $\mathcal{M}\models\varphi[s]\iff\mathcal{M}\models\varphi[s']$。論理式の複雑さに関する帰納法でただちに分かります）。特に文 $\sigma$ の充足は割り当てに依らないので、$\mathcal{M}\models\sigma$ と書き、$\mathcal{M}$ は $\sigma$ の**モデル**であるといいます。理論 $\Sigma$ のすべての文が成り立つとき $\mathcal{M}\models\Sigma$ と書きます。

<Definition id="def-consequence" title="意味論的帰結">

$\Gamma$ を文の集合、$\varphi$ を論理式とする。$\mathcal{M}\models\Gamma$ を満たす**すべて**の構造 $\mathcal{M}$ と**すべて**の割り当て $s$ について $\mathcal{M}\models\varphi[s]$ が成り立つとき、$\Gamma\models\varphi$ と書く。

</Definition>

<Example id="ex-group-consequence" title="群の公理からの帰結">

$\Gamma$ を群の公理（結合律、$e\cdot x=x$、$x^{-1}\cdot x=e$）とすると、$\Gamma\models\forall x\,(x\cdot e=x)$ です。群のあらゆる実例で成り立つ、という意味です。一方 $\Gamma\not\models\forall x\forall y\,(x\cdot y=y\cdot x)$ です。非可換群（例えば $S_3$）が反例になります。

</Example>

次の補題は、代入という記号の操作と、割り当ての更新という意味の操作が対応することを述べます。証明の中で何度も使います。

<Lemma id="lem-substitution" title="代入補題">

$\mathcal{M}$ を構造、$s$ を割り当て、$w$ を項とし、$a=w^{\mathcal{M}}[s]$ とおく。

1. 任意の項 $u$ について、$(u[w/x])^{\mathcal{M}}[s]=u^{\mathcal{M}}[s(x\mapsto a)]$。
2. $w$ が論理式 $\varphi$ の中で $x$ に代入可能ならば、$\mathcal{M}\models\varphi[w/x]\,[s]\iff\mathcal{M}\models\varphi[s(x\mapsto a)]$。

</Lemma>

<Proof of="lem-substitution">
(1) $u$ の構成に関する帰納法。$u$ が変数 $x$ なら左辺は $w^{\mathcal{M}}[s]=a$、右辺は $s(x\mapsto a)(x)=a$。$u$ が $x$ と異なる変数 $y$ なら両辺とも $s(y)$。定数も同様。$u=f(u_1,\ldots,u_n)$ なら、両辺とも $f^{\mathcal{M}}$ を各 $u_i$ の値に適用したもので、帰納法の仮定から一致する。

(2) $\varphi$ の複雑さに関する帰納法。原子論理式の場合は (1) から従う。$\neg,\to$ の場合は帰納法の仮定から明らか。$\varphi=\forall y\,\psi$ とする。$y=x$ のときは $x$ が自由に現れないので $\varphi[w/x]=\varphi$ で、$s$ と $s(x\mapsto a)$ は $\forall x$ の中で上書きされるため両辺は一致する。$y\ne x$ のとき、$x$ が $\psi$ に自由に現れないなら同様に自明である。現れるなら代入可能性より $y$ は $w$ に現れず、$\varphi[w/x]=\forall y\,(\psi[w/x])$ である。各元 $b$ について、$s(y\mapsto b)$ のもとでの $w$ の値は $y\notin w$ だから $a$ のままで、帰納法の仮定を $s(y\mapsto b)$ に適用すれば
$$
\mathcal{M}\models\psi[w/x]\,[s(y\mapsto b)]\iff\mathcal{M}\models\psi\,[s(y\mapsto b)(x\mapsto a)]
$$
を得る（更新の順序は $x\ne y$ なので交換できる）。$b$ について「すべて」をとれば主張が従う。
</Proof>

## 4. 証明体系と健全性

### 4.1. ヒルベルト流の証明体系

証明の検査を機械的にするため、公理と推論規則を明示します。ここでは公理の数が多く、推論規則が少ないヒルベルト流の体系を採ります。論理式 $\varphi$ の自由変数についての扱いを単純にするため、仮定の集合 $\Gamma$ には**文だけ**を入れます。推論規則は二つで、モーダスポネンスは「$A$ と $A\to B$ が得られていれば $B$ を得てよい」という規則、一般化は「$\varphi$ が得られていれば $\forall x\,\varphi$ を得てよい」という規則です（下の定義にある形）。

<Definition id="def-deduction" title="論理公理と導出">

次の形の論理式を**論理公理**という。$\varphi,\psi$ は任意の論理式、$s,t$ は任意の項である。

- (L1) 命題論理のトートロジー（真理値表で常に真になる式）の変数を論理式で置き換えて得られるもの。
- (L2) $\forall x\,\varphi\to\varphi[t/x]$（$t$ は $\varphi$ の中で $x$ に代入可能）。
- (L3) $\forall x\,(\varphi\to\psi)\to(\forall x\,\varphi\to\forall x\,\psi)$。
- (L4) $\varphi\to\forall x\,\varphi$（$x\notin\mathrm{FV}(\varphi)$）。
- (L5) $t=t$。
- (L6) $s=t\to(\varphi[s/x]\to\varphi[t/x])$（$\varphi$ は原子論理式）。

文の集合 $\Gamma$ からの**導出**とは、論理式の有限列 $\varphi_1,\ldots,\varphi_n$ で、各 $\varphi_i$ が次のいずれかであるものをいう。

- 論理公理である。
- $\Gamma$ の元である。
- **モーダスポネンス**：ある $j,k<i$ について $\varphi_k=(\varphi_j\to\varphi_i)$。
- **一般化**：ある $j<i$ と変数 $x$ について $\varphi_i=\forall x\,\varphi_j$。

$\varphi_n=\varphi$ となる導出があるとき $\Gamma\vdash\varphi$ と書く。$\Gamma$ が**無矛盾**であるとは、$\Gamma\vdash\varphi$ かつ $\Gamma\vdash\neg\varphi$ となる $\varphi$ が存在しないことをいう。

</Definition>

(L6) と (L5) から等号の対称律・推移律と、関数記号・関係記号との整合性が出ます。例えば $x$ を $s,t$ に現れない変数として、$\varphi$ を $x=s$ とすると (L6) は $s=t\to(s=s\to t=s)$ で、(L5) と合わせて $s=t\to t=s$ が導かれます。関数記号 $f$ については、$\varphi$ を $f(\ldots,s,\ldots)=f(\ldots,x,\ldots)$ ととれば $s=t\to f(\ldots,s,\ldots)=f(\ldots,t,\ldots)$ が同様に出ます。

<Example id="ex-derivation" title="導出の一例">

$\vdash\forall x\,(x=x)$ の導出です。(1) $x=x$（L5）。(2) $\forall x\,(x=x)$（(1) への一般化）。2 行で終わります。ここで一般化を仮定のない論理式にだけ使っている点が大切です。仮定 $\Gamma$ に含まれる論理式に自由変数があれば、一般化は健全性を壊します（<Ref to="exr-gen" />）。

</Example>

<Theorem id="thm-soundness" title="健全性">
文の集合 $\Gamma$ と論理式 $\varphi$ について、$\Gamma\vdash\varphi$ ならば $\Gamma\models\varphi$。
</Theorem>

<Proof of="thm-soundness">
導出 $\varphi_1,\ldots,\varphi_n$ の長さに関する帰納法で、各 $\varphi_i$ について「$\mathcal{M}\models\Gamma$ なるすべての $\mathcal{M}$ とすべての $s$ で $\mathcal{M}\models\varphi_i[s]$」を示す。

(L1) 構造と割り当てを固定すると、各部分論理式は真か偽かのどちらかで、$\neg,\to$ の充足条件は真理値表そのものである。よってトートロジーの代入例は常に満たされる。
(L2) $\mathcal{M}\models\forall x\,\varphi\,[s]$ とすると、特に $a=t^{\mathcal{M}}[s]$ について $\mathcal{M}\models\varphi[s(x\mapsto a)]$ である。<Ref to="lem-substitution" />(2) より $\mathcal{M}\models\varphi[t/x]\,[s]$。
(L3) $\forall x(\varphi\to\psi)$ と $\forall x\varphi$ が $s$ で成り立つとする。各元 $a$ で $\varphi\to\psi$ と $\varphi$ が成り立つので $\psi$ が成り立ち、$\forall x\,\psi$ を得る。
(L4) $x\notin\mathrm{FV}(\varphi)$ なので、$\varphi$ の充足は $x$ への割り当てに依らない。$\varphi$ が $s$ で成り立てば、すべての $s(x\mapsto a)$ でも成り立つ。
(L5)(L6) 等号は領域の元の恒等的な等しさとして解釈されている。(L5) は明らか。(L6) は、$s^{\mathcal{M}}[s']=t^{\mathcal{M}}[s']$ のとき、<Ref to="lem-substitution" /> により $\varphi[s/x]$ の充足は $x$ に共通の値を割り当てたときの $\varphi$ の充足と一致し、$\varphi[t/x]$ の充足とも一致する（記号の衝突を避けるため割り当てを $s'$ と書いた）。
$\Gamma$ の元は仮定 $\mathcal{M}\models\Gamma$ より成り立つ。
モーダスポネンスは $\to$ の充足条件から従う。
一般化では、$\varphi_j$ が**すべての割り当て**で成り立つ（帰納法の仮定）ので、とくに任意の $s$ と任意の $a$ について $\varphi_j$ が $s(x\mapsto a)$ で成り立ち、$\forall x\,\varphi_j$ が $s$ で成り立つ。
</Proof>

### 4.2. 無矛盾性の基本事実

完全性定理の証明のために、導出に関する基本事実を整理します。

<Proposition id="prop-deduction" title="演繹定理">
$\Gamma$ を文の集合、$\sigma$ を文、$\varphi$ を論理式とする。$\Gamma\cup\{\sigma\}\vdash\varphi$ ならば $\Gamma\vdash\sigma\to\varphi$。
</Proposition>

<Proof of="prop-deduction">
$\Gamma\cup\{\sigma\}$ からの導出 $\varphi_1,\ldots,\varphi_n=\varphi$ の長さに関する帰納法で、各 $i$ について $\Gamma\vdash\sigma\to\varphi_i$ を示す。
- $\varphi_i$ が論理公理か $\Gamma$ の元のとき：$\varphi_i$ と $\varphi_i\to(\sigma\to\varphi_i)$（L1）からモーダスポネンスで。
- $\varphi_i=\sigma$ のとき：$\sigma\to\sigma$ はトートロジー（L1）。
- モーダスポネンスで $\varphi_k=(\varphi_j\to\varphi_i)$ のとき：帰納法の仮定より $\Gamma\vdash\sigma\to\varphi_j$ と $\Gamma\vdash\sigma\to(\varphi_j\to\varphi_i)$ があり、$(\sigma\to\varphi_j)\to((\sigma\to(\varphi_j\to\varphi_i))\to(\sigma\to\varphi_i))$ はトートロジーなので $\Gamma\vdash\sigma\to\varphi_i$。
- 一般化で $\varphi_i=\forall x\,\varphi_j$ のとき：$\Gamma\vdash\sigma\to\varphi_j$ に一般化を適用して $\Gamma\vdash\forall x\,(\sigma\to\varphi_j)$。(L3) で $\forall x\,\sigma\to\forall x\,\varphi_j$ が得られる形にし、$\sigma$ は文なので (L4) により $\sigma\to\forall x\,\sigma$ である。よってトートロジー推論で $\Gamma\vdash\sigma\to\forall x\,\varphi_j$。
</Proof>

最後の場合が、仮定を文に限った理由です。仮定に自由変数があると (L4) が使えません。

<Proposition id="prop-consistency" title="無矛盾性の基本性質">
$\Gamma$ を文の集合、$\sigma$ を文とする。

1. $\Gamma$ が矛盾するならば、任意の論理式 $\varphi$ について $\Gamma\vdash\varphi$。
2. $\Gamma\cup\{\neg\sigma\}$ が矛盾するならば $\Gamma\vdash\sigma$。$\Gamma\cup\{\sigma\}$ が矛盾するならば $\Gamma\vdash\neg\sigma$。
3. $\Gamma$ が無矛盾ならば、$\Gamma\cup\{\sigma\}$ と $\Gamma\cup\{\neg\sigma\}$ の少なくとも一方は無矛盾。
4. $\Gamma$ が矛盾するならば、$\Gamma$ のある有限部分集合が矛盾する。
</Proposition>

<Proof of="prop-consistency">
(1) $\Gamma\vdash\psi$ かつ $\Gamma\vdash\neg\psi$ とする。$\neg\psi\to(\psi\to\varphi)$ はトートロジーなので、モーダスポネンスを 2 回使って $\Gamma\vdash\varphi$。
(2) 前半：(1) より $\Gamma\cup\{\neg\sigma\}\vdash\sigma$ なので、<Ref to="prop-deduction" /> から $\Gamma\vdash\neg\sigma\to\sigma$。$(\neg\sigma\to\sigma)\to\sigma$ はトートロジーなので $\Gamma\vdash\sigma$。後半：(1) より $\Gamma\cup\{\sigma\}\vdash\neg\sigma$ なので $\Gamma\vdash\sigma\to\neg\sigma$。$(\sigma\to\neg\sigma)\to\neg\sigma$ はトートロジーなので $\Gamma\vdash\neg\sigma$。
(3) 両方が矛盾すれば、(2) から $\Gamma\vdash\sigma$ と $\Gamma\vdash\neg\sigma$。
(4) 導出は有限列で、使われる $\Gamma$ の元は有限個である。
</Proof>

もう一つ、**新しい定数**に関する補題が必要です。ヘンキンの構成で、言語に定数を足しても無矛盾性が保たれることを確かめるために使います。(1) は、定数を足しても元の言語の式について証明できる範囲は変わらないこと、(2) は、新しい定数について示せたことは任意の元について示せたことになる、ということを述べています。

<Lemma id="lem-constants" title="新しい定数の変数化">
$L'$ を言語 $L$ に定数記号の集合 $C$ を加えた言語とする。

1. $\Gamma$ を $L$ の文の集合、$\varphi$ を $L$ の論理式とする。$\Gamma$ から $L'$ で $\varphi$ が導出できるならば、$L$ で導出できる。特に、$\Gamma$ が $L$ で無矛盾ならば $L'$ でも無矛盾。
2. $\Gamma$ を $L'$ の文の集合、$\varphi$ を $L'$ の論理式、$c$ を $L'$ の定数記号とし、$c$ は $\Gamma$ にも $\varphi$ にも現れないとする。$\Gamma\vdash\varphi[c/x]$ ならば $\Gamma\vdash\forall x\,\varphi$。
</Lemma>

<Proof of="lem-constants">
(1) $L'$ での導出に現れる $C$ の定数は有限個。それらを導出のどこにも現れない互いに異なる変数で置き換える。論理公理の形（トートロジーの代入例、代入可能性、$x\notin\mathrm{FV}$ の条件）は、新しい変数が他の変数や量化子と衝突しないので保たれる。$\Gamma$ の文と $\varphi$ には $C$ の定数が現れないので、置き換えで変わらない。結果は $L$ での導出である。無矛盾性についての主張は、矛盾の定義（ある $\psi$ で $\Gamma\vdash\psi,\neg\psi$）に、$\psi$ が $L'$ の論理式であっても (1) の置き換えを両方の導出に適用すればよい。
(2) $\varphi[c/x]$ の導出に現れる $c$ を、導出に現れない変数 $y$ で置き換える。$\Gamma$ の文には $c$ が現れないので置き換えで変わらず、(1) と同じ理由で導出のままであり、結論は $\varphi[y/x]$ になる。一般化で $\forall y\,\varphi[y/x]$。(L2) で $\forall y\,\varphi[y/x]\to\varphi$（$\varphi[y/x][x/y]=\varphi$、$y$ は新しいので代入可能）。モーダスポネンスで $\Gamma\vdash\varphi$、さらに一般化して $\Gamma\vdash\forall x\,\varphi$。
</Proof>

## 5. 完全性定理

健全性は「証明できれば真」でした。逆向き、つまり「すべてのモデルで真ならば証明できる」を示すには、[対偶](/mathematics/foundations/proof-techniques#def-converse-contrapositive)をとって**「証明できない $\sigma$ があれば、$\sigma$ が偽になるモデルを作る」**ことを目指します。モデルを作る材料は、言語の記号しかありません。ヘンキンの方法は、記号そのものからモデルを組み立てます。

<Figure caption="完全性定理の証明の流れ。無矛盾な理論から、記号だけでモデルを組み立てる。">
<svg viewBox="0 0 640 150" width="100%" role="img" aria-label="無矛盾な理論から、ヘンキン定数の追加、極大無矛盾化、項モデルの構成を経てモデルを得る流れの図">
  <defs>
    <marker id="fol-arrow" markerWidth="8" markerHeight="8" refX="6" refY="3" orient="auto">
      <path d="M 0 0 L 6 3 L 0 6 z" fill="var(--sl-color-accent)" />
    </marker>
  </defs>
  <rect x="8" y="40" width="130" height="70" rx="8" fill="none" stroke="currentColor" stroke-width="1.5" />
  <text x="73" y="70" text-anchor="middle" fill="currentColor" font-size="13">無矛盾な理論 Σ</text>
  <text x="73" y="92" text-anchor="middle" fill="currentColor" font-size="11">（言語 L）</text>
  <rect x="172" y="40" width="130" height="70" rx="8" fill="none" stroke="currentColor" stroke-width="1.5" />
  <text x="237" y="66" text-anchor="middle" fill="currentColor" font-size="13">証人の定数を</text>
  <text x="237" y="86" text-anchor="middle" fill="currentColor" font-size="13">足した理論</text>
  <text x="237" y="104" text-anchor="middle" fill="currentColor" font-size="11">（ヘンキン公理）</text>
  <rect x="336" y="40" width="130" height="70" rx="8" fill="none" stroke="currentColor" stroke-width="1.5" />
  <text x="401" y="66" text-anchor="middle" fill="currentColor" font-size="13">極大無矛盾な</text>
  <text x="401" y="86" text-anchor="middle" fill="currentColor" font-size="13">理論 Γ</text>
  <text x="401" y="104" text-anchor="middle" fill="currentColor" font-size="11">（リンデンバウム）</text>
  <rect x="500" y="40" width="130" height="70" rx="8" fill="none" stroke="var(--sl-color-accent)" stroke-width="2" />
  <text x="565" y="66" text-anchor="middle" fill="currentColor" font-size="13">閉項のなす</text>
  <text x="565" y="86" text-anchor="middle" fill="currentColor" font-size="13">構造 M ⊨ Γ</text>
  <text x="565" y="104" text-anchor="middle" fill="currentColor" font-size="11">（真理補題）</text>
  <line x1="140" y1="75" x2="168" y2="75" stroke="var(--sl-color-accent)" stroke-width="2" marker-end="url(#fol-arrow)" />
  <line x1="304" y1="75" x2="332" y2="75" stroke="var(--sl-color-accent)" stroke-width="2" marker-end="url(#fol-arrow)" />
  <line x1="468" y1="75" x2="496" y2="75" stroke="var(--sl-color-accent)" stroke-width="2" marker-end="url(#fol-arrow)" />
</svg>
</Figure>

以下、言語 $L$ は[**可算**](/mathematics/foundations/cardinality-and-infinity#def-countable)とします（非可算の場合は <Ref to="rem-uncountable" /> で述べます）。このとき $L$ の論理式は有限記号列なので可算個です。

### 5.1. 証人となる定数の追加

「$\forall x\,\varphi$ が偽ならば、$\varphi$ を満たさない具体的な元がある」。モデルの元を記号で名指しするため、そのような元の名前（**証人**）を言語に予約します。

<Definition id="def-henkin" title="ヘンキン公理">
言語 $L$ の論理式 $\varphi$ と変数 $x$ の組で $\mathrm{FV}(\varphi)\subseteq\{x\}$ を満たすものそれぞれに、新しい定数記号 $c_{\varphi,x}$ を用意し、$L$ にこれらを加えた言語を $L^{+}$ と書く。**ヘンキン公理**とは $L^{+}$ の文
$$
\neg\forall x\,\varphi\ \to\ \neg\varphi[c_{\varphi,x}/x]
$$
である。$L$ の論理式すべてについてのヘンキン公理の集合を $H(L)$ と書く。
</Definition>

次の補題は背理法で示します。矛盾を起こす有限個のヘンキン公理のうち、個数が最小のものをとると、最後の一つだけが矛盾の原因になります。その公理の定数が新しいことを使い、<Ref to="lem-constants" />(2) で元の理論自身の矛盾を導きます。

<Lemma id="lem-henkin-step" title="ヘンキン公理を足しても無矛盾">
$\Sigma$ が $L$ の無矛盾な理論ならば、$\Sigma\cup H(L)$ は $L^{+}$ で無矛盾である。
</Lemma>

<Proof of="lem-henkin-step">
$\Sigma\cup H(L)$ が矛盾すると仮定する。導出は有限なので（<Ref to="prop-consistency" />(4)）、有限個のヘンキン公理 $h_1,\ldots,h_k$（$h_i$ は定数 $c_i=c_{\varphi_i,x_i}$ に対応し、$c_i$ は互いに異なる）で $\Sigma\cup\{h_1,\ldots,h_k\}$ が矛盾するものがある。$k$ を最小にとる。$k=0$ とすると $\Sigma$ が $L^{+}$ で矛盾することになるが、<Ref to="lem-constants" />(1) により $\Sigma$ は $L^{+}$ で無矛盾なので、$k\ge1$ である。

$\Sigma'=\Sigma\cup\{h_1,\ldots,h_{k-1}\}$ は $k$ の最小性により無矛盾で、$h_k$ だけが矛盾の原因である。$c=c_k$、$\varphi=\varphi_k$、$x=x_k$ とおく。$\Sigma'$ にも $\varphi$ にも $c$ は現れない（$\varphi$ は $L$ の論理式、$h_1,\ldots,h_{k-1}$ には別の定数しか現れない）。<Ref to="prop-consistency" />(2) より $\Sigma'\vdash\neg h_k$。$\neg(A\to B)$ からは $A$ と $\neg B$ がトートロジー推論で出るので、
$$
\Sigma'\vdash\neg\forall x\,\varphi,\qquad\Sigma'\vdash\varphi[c/x].
$$
後者に <Ref to="lem-constants" />(2) を使うと $\Sigma'\vdash\forall x\,\varphi$ となり、前者と合わせて $\Sigma'$ が矛盾する。これは $\Sigma'$ の無矛盾性に反する。
</Proof>

この操作を繰り返します。$L_0=L$、$L_{n+1}=L_n^{+}$、$L_\omega=\bigcup_nL_n$ とし、$\Sigma_0=\Sigma$、$\Sigma_{n+1}=\Sigma_n\cup H(L_n)$、$\Sigma_\omega=\bigcup_n\Sigma_n$ とします。

<Lemma id="lem-henkin-theory" title="ヘンキン理論">
$\Sigma$ が（任意の濃度の言語）$L$ で無矛盾ならば、次が成り立つ。

1. $\Sigma_\omega$ は $L_\omega$ で無矛盾。$L$ が可算ならば $L_\omega$ も可算言語である。
2. $L_\omega$ の論理式 $\varphi$ と変数 $x$ が $\mathrm{FV}(\varphi)\subseteq\{x\}$ を満たすなら、$L_\omega$ の定数 $c$ で $\neg\forall x\,\varphi\to\neg\varphi[c/x]\in\Sigma_\omega$ となるものがある。
3. $L_\omega$ は閉項をもつ。
</Lemma>

<Proof of="lem-henkin-theory">
(1) $L$ が可算なら、各 $L_n$ が可算であることが帰納的に分かる（$L_n$ の論理式は可算個だから $L_{n+1}$ に加わる定数も可算個）ので、$L_\omega$ は可算。無矛盾性について、$\Sigma_n$ は $L_n$ で無矛盾であることを帰納法で示す：$\Sigma_0=\Sigma$ は仮定。$\Sigma_n$ が $L_n$ で無矛盾なら、<Ref to="lem-henkin-step" /> より $\Sigma_{n+1}$ は $L_{n+1}$ で無矛盾。$\Sigma_\omega$ が $L_\omega$ で矛盾するなら、有限部分集合が矛盾し、それは $\Sigma_n$ に含まれるある $n$ があって、<Ref to="lem-constants" />(1) から $\Sigma_n$ が $L_n$ で矛盾する、という矛盾に至る。
(2) $\varphi$ は有限記号列なので、ある $L_n$ の論理式である。ヘンキン公理 $\in H(L_n)\subseteq\Sigma_{n+1}$。
(3) 論理式 $x=x$ に (2) を使う。
</Proof>

### 5.2. 極大無矛盾化

<Lemma id="lem-lindenbaum" title="リンデンバウムの補題">
$L'$ を可算言語、$\Sigma'$ を $L'$ の無矛盾な理論とする。このとき、$\Sigma'\subseteq\Gamma$ を満たす $L'$ の理論 $\Gamma$ で、次をみたすものがある。

- (a) $\Gamma$ は無矛盾。
- (b) 完全：任意の文 $\sigma$ について $\sigma\in\Gamma$ または $\neg\sigma\in\Gamma$。
- (c) 演繹的に閉じている：$\Gamma\vdash\sigma$ ならば $\sigma\in\Gamma$。
</Lemma>

<Proof of="lem-lindenbaum">
$L'$ の文を $\sigma_0,\sigma_1,\ldots$ と並べる（可算個）。$\Gamma_0=\Sigma'$ とし、$\Gamma_n$ が無矛盾なとき、$\Gamma_n\cup\{\sigma_n\}$ が無矛盾ならそれを $\Gamma_{n+1}$、そうでなければ $\Gamma_{n+1}=\Gamma_n\cup\{\neg\sigma_n\}$ とする。<Ref to="prop-consistency" />(3) より $\Gamma_{n+1}$ も無矛盾。$\Gamma=\bigcup_n\Gamma_n$ とおく。矛盾すれば有限部分集合が矛盾し、それはある $\Gamma_n$ に含まれるので不可能（(a)）。構成から各 $\sigma_n$ について $\sigma_n$ か $\neg\sigma_n$ が $\Gamma$ に入る（(b)）。(c)：$\Gamma\vdash\sigma$ で $\sigma\notin\Gamma$ とすると (b) から $\neg\sigma\in\Gamma$ で、$\Gamma$ は $\sigma$ と $\neg\sigma$ の両方を証明して矛盾する。
</Proof>

### 5.3. 項モデルと真理補題

$\Sigma$ を $L$ の無矛盾な理論とし、<Ref to="lem-henkin-theory" /> の $L_\omega$ と $\Sigma_\omega$ を用意します。<Ref to="lem-lindenbaum" /> を $(L_\omega,\Sigma_\omega)$ に適用して得られる理論を $\Gamma$ とします。$\Gamma$ はヘンキン公理をすべて含みます。

モデルの元は、閉項そのものを使います。ただし $\Gamma$ が $t=s$ を含むなら $t$ と $s$ は同じ元を指すべきなので、そうした閉項どうしは同一視してまとめます。

<Definition id="def-term-model" title="項モデル">
$T$ を $L_\omega$ の閉項全体とし、$t\sim s\iff(t=s)\in\Gamma$ とおく。(L5), (L6) と $\Gamma$ の演繹的閉性から $\sim$ は[同値関係](/mathematics/foundations/equivalence-relations#def-equivalence)で、関数記号・関係記号と整合的である（例：$t_i\sim s_i$ ($i=1..n$) ならば $f(t_1,..,t_n)\sim f(s_1,..,s_n)$、$R(t_1,..,t_n)\in\Gamma\iff R(s_1,..,s_n)\in\Gamma$）。**項モデル** $\mathcal{M}$ を次で定める。

- 領域は $T/{\sim}$（<Ref to="lem-henkin-theory" />(3) より空でない）。閉項 $t$ の類を $[t]$ と書く。
- $c^{\mathcal{M}}=[c]$、$f^{\mathcal{M}}([t_1],\ldots,[t_n])=[f(t_1,\ldots,t_n)]$。
- $([t_1],\ldots,[t_n])\in R^{\mathcal{M}}\iff R(t_1,\ldots,t_n)\in\Gamma$。
</Definition>

帰納法ですぐに分かるように、閉項 $t$ の値は $t^{\mathcal{M}}=[t]$ です。したがって**領域のどの元も閉項 $t$ によって $[t]$ と書けます**。ここが「記号が尽くしてモデルを作る」ことの核心です。

次の真理補題は、「$\Gamma$ に入っている」ことと「$\mathcal{M}$ で真である」ことが一致する、と述べます。証明は文の作り方に沿った帰納法です。難所は $\forall$ の場合で、$\forall x\,\varphi$ が $\Gamma$ に入らないときは、証人の定数 $c$ が反例の元を与える、という流れで進みます。

<Lemma id="lem-truth" title="真理補題">
$L_\omega$ のすべての文 $\sigma$ について、$\mathcal{M}\models\sigma\iff\sigma\in\Gamma$。
</Lemma>

<Proof of="lem-truth">
$\sigma$ の複雑さ $\mathrm{c}(\sigma)$ に関する帰納法。閉項 $t$ による代入 $\varphi[t/x]$ は複雑さを変えないことに注意する。

*原子文*。$\mathcal{M}\models(t=s)\iff[t]=[s]\iff(t=s)\in\Gamma$。$R(t_1,..,t_n)$ は $R^{\mathcal{M}}$ の定義そのもの。

*$\neg\tau$*。$\mathcal{M}\models\neg\tau\iff\mathcal{M}\not\models\tau\iff\tau\notin\Gamma$（帰納法の仮定）$\iff\neg\tau\in\Gamma$（$\Gamma$ が無矛盾かつ完全）。

*$\tau\to\rho$*。$\mathcal{M}\models(\tau\to\rho)$ は「$\tau\notin\Gamma$ または $\rho\in\Gamma$」と同値。これが $(\tau\to\rho)\in\Gamma$ と同値であることを示す。$(\tau\to\rho)\in\Gamma$ かつ $\tau\in\Gamma$ なら $\Gamma\vdash\rho$ で、$\rho\in\Gamma$。逆に $\tau\notin\Gamma$ なら $\neg\tau\in\Gamma$ で、$\neg\tau\to(\tau\to\rho)$ がトートロジーなので $(\tau\to\rho)\in\Gamma$。$\rho\in\Gamma$ なら $\rho\to(\tau\to\rho)$ から同様。

*$\forall x\,\varphi$*（$\mathrm{FV}(\varphi)\subseteq\{x\}$）。

($\Leftarrow$) $\forall x\,\varphi\in\Gamma$ とする。領域の任意の元は閉項 $t$ による $[t]$ の形。(L2) とモーダスポネンスで $\varphi[t/x]\in\Gamma$。帰納法の仮定から $\mathcal{M}\models\varphi[t/x]$。<Ref to="lem-substitution" />(2) により、$x$ に $[t]$ を割り当てて $\varphi$ は成り立つ。$[t]$ は任意なので $\mathcal{M}\models\forall x\,\varphi$。

($\Rightarrow$) 対偶を示す。$\forall x\,\varphi\notin\Gamma$ とすると、$\neg\forall x\,\varphi\in\Gamma$。<Ref to="lem-henkin-theory" />(2) の定数 $c$ のヘンキン公理が $\Gamma$ にあるので、モーダスポネンスで $\neg\varphi[c/x]\in\Gamma$、すなわち $\varphi[c/x]\notin\Gamma$。帰納法の仮定から $\mathcal{M}\not\models\varphi[c/x]$。<Ref to="lem-substitution" />(2) により、$x$ に $c^{\mathcal{M}}$ を割り当てると $\varphi$ は成り立たないので $\mathcal{M}\not\models\forall x\,\varphi$。
</Proof>

### 5.4. 完全性定理

<Theorem id="thm-completeness" title="ゲーデルの完全性定理（可算言語）">
$L$ を可算言語とする。

1. $L$ の理論 $\Sigma$ が無矛盾ならば、$\Sigma$ はモデルをもつ。
2. $\Gamma$ を文の集合、$\varphi$ を論理式とするとき、$\Gamma\models\varphi$ ならば $\Gamma\vdash\varphi$。

したがって健全性（<Ref to="thm-soundness" />）と合わせて、$\Gamma\vdash\varphi\iff\Gamma\models\varphi$。
</Theorem>

<Proof of="thm-completeness">
(1) 上の構成で $\Sigma\subseteq\Sigma_\omega\subseteq\Gamma$ と $\mathcal{M}$ を得る。<Ref to="lem-truth" /> より $\mathcal{M}\models\Gamma$、特に $\mathcal{M}\models\Sigma$。$\mathcal{M}$ の $L$ への制限（$L$ に属さない記号を忘れたもの）は、$L$ の文について同じ真偽を与えるので $\Sigma$ のモデルである。

(2) $\varphi$ の自由変数を $x_1,\ldots,x_n$ とし、$\sigma=\forall x_1\cdots\forall x_n\,\varphi$ とおく。$\Gamma\models\varphi$ ならば $\Gamma\models\sigma$ である（$\Gamma$ のモデルでは $\varphi$ がすべての割り当てで成り立つ）。$\Gamma\nvdash\sigma$ とすると、<Ref to="prop-consistency" />(2) の対偶から $\Gamma\cup\{\neg\sigma\}$ は無矛盾（$\Gamma\cup\{\neg\sigma\}$ が矛盾すれば $\Gamma\vdash\sigma$）。(1) によりそのモデルがあるが、それは $\Gamma\models\sigma$ に反する。よって $\Gamma\vdash\sigma$。(L2)（$t$ として変数 $x_i$ 自身をとる）とモーダスポネンスを $n$ 回使って $\Gamma\vdash\varphi$。
</Proof>

これが「証明できる」と「真である」の一致です。数学の側から見れば、公理系 $\Gamma$ から $\varphi$ が従う（すべてのモデルで成り立つ）ことと、$\Gamma$ から $\varphi$ への形式的な導出が存在することは同じことなのです。前者を確かめる道は無数のモデルを調べるしかなさそうに見えますが、後者は有限の記号列を示せば済みます。

<Lemma id="lem-lindenbaum-zorn" title="リンデンバウムの補題（任意の言語）">
$L'$ を任意の言語、$\Sigma'$ を $L'$ の無矛盾な理論とする。このとき <Ref to="lem-lindenbaum" /> の (a)(b)(c) をみたす $L'$ の理論 $\Gamma\supseteq\Sigma'$ がある。
</Lemma>

<Proof of="lem-lindenbaum-zorn">
$\Sigma'$ を含む $L'$ の無矛盾な理論全体を包含関係で順序づけます。鎖の合併は（導出が有限なので、<Ref to="prop-consistency" />(4)）無矛盾で、鎖の上界になります。<Ref to="mathematics/foundations/axiom-of-choice-zorn#thm-zorn" /> から[極大元](/mathematics/foundations/axiom-of-choice-zorn#def-bounds) $\Gamma$ が得られます。$\Gamma$ は (a) をみたします。任意の文 $\sigma$ について、$\Gamma\cup\{\sigma\}$ が無矛盾なら極大性から $\sigma\in\Gamma$ で、そうでなければ <Ref to="prop-consistency" />(3) により $\Gamma\cup\{\neg\sigma\}$ が無矛盾なので $\neg\sigma\in\Gamma$ です（(b)）。(c) は <Ref to="lem-lindenbaum" /> の証明と同じく (b) から従います。
</Proof>

<Theorem id="thm-completeness-uncountable" title="ゲーデルの完全性定理（任意の言語）">
$L$ を任意の言語とする。(1) $L$ の無矛盾な理論はモデルをもつ。(2) $\Gamma\models\varphi$ ならば $\Gamma\vdash\varphi$。
</Theorem>

<Proof of="thm-completeness-uncountable">
<Ref to="thm-completeness" /> の証明で、<Ref to="lem-henkin-theory" /> は任意の $L$ について成り立ち（可算性は $L_\omega$ の可算性の主張にしか使わない）、リンデンバウムの補題を <Ref to="lem-lindenbaum-zorn" /> に替えます。項モデルの構成（<Ref to="def-term-model" />）と真理補題（<Ref to="lem-truth" />）は言語の濃度を使わないので、そのまま通ります。(2) は (1) から <Ref to="thm-completeness" /> の (2) の議論と同じです。
</Proof>

<Remark id="rem-uncountable" title="非可算言語の場合">
可算性を使ったのは、リンデンバウムの補題での文の枚挙と、$L_\omega$ が可算であることだけです。非可算の $L$ では、リンデンバウムの補題を**ツォルンの補題**で置き換えます（<Ref to="lem-lindenbaum-zorn" />、完全性定理は <Ref to="thm-completeness-uncountable" />）。ヘンキンの段階 $L_n$ は $\omega$ 回で閉じ、$L_\omega$ の記号の個数は $|L|+\aleph_0$ のまま変わりません。以下、コンパクト性定理と上向きの Löwenheim–Skolem では、この非可算言語版の完全性定理を使います。
</Remark>

## 6. コンパクト性定理と Löwenheim–Skolem の定理

導出が有限であるという事実と完全性定理を組み合わせると、次のことが分かります。

<Theorem id="thm-compactness" title="コンパクト性定理">
$\Sigma$ を文の集合とする。$\Sigma$ のどの有限部分集合もモデルをもつならば、$\Sigma$ 全体もモデルをもつ。
</Theorem>

<Proof of="thm-compactness">
$\Sigma$ がモデルをもたないと仮定する。$\Sigma$ は無矛盾でない（無矛盾なら完全性定理 (<Ref to="thm-completeness" />。言語が非可算ならその非可算版、<Ref to="thm-completeness-uncountable" />) でモデルをもつ）。よって <Ref to="prop-consistency" />(4) により有限部分集合 $\Sigma_0\subseteq\Sigma$ が矛盾する。健全性より、$\Sigma_0$ がモデルをもてば $\Sigma_0\vdash\varphi,\neg\varphi$ から $\varphi$ と $\neg\varphi$ がそのモデルで成り立ち、不可能である。よって $\Sigma_0$ はモデルをもたず、仮定に反する。
</Proof>

コンパクト性は「有限の情報だけからは見えないこと」を一階論理が表現できないことを教えてくれます。二つの典型例を見ます。

<Example id="ex-nonstandard-arithmetic" title="非標準モデル">
算術の言語に新しい定数 $d$ を加え、$\Sigma=\mathrm{Th}(\mathbb{N})\cup\{\,d>\overline{n}\mid n\in\mathbb{N}\,\}$ を考えます。$\mathrm{Th}(\mathbb{N})$ は $\mathbb{N}$ で真な文全体、$\overline{n}$ は $S(S(\cdots S(0)))$（$S$ を $n$ 回）です。有限部分集合は、現れる $n$ の最大値 $N$ より大きい自然数を $d$ の解釈とした $\mathbb{N}$ で満たされます。コンパクト性定理から $\Sigma$ のモデル $\mathcal{N}^{*}$ があり、そこには $d$ という「すべての標準的な自然数より大きい元」が含まれます。$\mathcal{N}^{*}$ は $\mathrm{Th}(\mathbb{N})$ を満たすのに $\mathbb{N}$ と同型ではない（**非標準モデル**）。つまり「$\mathbb{N}$ ちょうど」を一階の文で指定することはできません。ペアノ算術の非標準モデルも、同じ手法で作れます（[ゲーデルの不完全性定理](/mathematics/logic-and-type-theory/incompleteness-theorems)の記事には、不完全性定理から非標準モデルを作る別の方法があります）。
</Example>

<Example id="ex-finiteness" title="「有限」は一階では表せない">
文の集合 $T$ が任意に大きな有限モデルをもつとします。各 $n$ に対し「要素が $n$ 個以上ある」を表す文 $\lambda_n=\exists x_1\cdots\exists x_n\bigwedge_{i<j}x_i\neq x_j$ をとります。$T\cup\{\lambda_n\mid n\ge1\}$ の有限部分集合は $T$ の十分大きな有限モデルで満たされるので、コンパクト性定理により $T$ は**無限モデル**をもちます。したがって、モデルがちょうど有限構造全体であるような一階の理論は存在しません。
</Example>

<Theorem id="thm-ls" title="レーヴェンハイム–スコーレムの定理">
$L$ を言語とする。

1. （下向き）$L$ が可算で、理論 $\Sigma$ がモデルをもつならば、$\Sigma$ は高々可算なモデルをもつ。
2. （上向き）$\Sigma$ が無限モデルをもつならば、任意の無限基数 $\kappa$ について、濃度 $\kappa$ 以上のモデルをもつ。
</Theorem>

<Proof of="thm-ls">
(1) $\Sigma$ はモデルをもつので、健全性から無矛盾である（矛盾する $\Sigma$ のモデルがあれば、同じモデルで $\varphi$ と $\neg\varphi$ が成り立ってしまう）。<Ref to="thm-completeness" /> の証明で作った項モデル $\mathcal{M}$ は $\Sigma$ のモデルで、領域は可算集合 $T$ の商だから高々可算。
(2) $L$ に新しい定数 $\{d_\alpha\}_{\alpha<\kappa}$ を加え、$\Sigma'=\Sigma\cup\{d_\alpha\neq d_\beta\mid\alpha\neq\beta\}$ とする。$\Sigma'$ の有限部分集合は有限個の定数についての不等式しか含まないので、$\Sigma$ の無限モデルでそれらの定数を相異なる元に解釈して満たせる。コンパクト性定理（<Ref to="thm-compactness" />。言語が非可算でもよい。その証明で <Ref to="thm-completeness-uncountable" /> を使う）により $\Sigma'$ はモデル $\mathcal{M}'$ をもち、その領域は互いに異なる $\kappa$ 個の元 $d_\alpha^{\mathcal{M}'}$ を含む。$L$ に制限して $\Sigma$ のモデルを得る。
</Proof>

<Remark id="rem-skolem-paradox" title="スコーレムのパラドックス">
集合論 ZFC の公理は可算言語の一階の文の集合です。ZFC が無矛盾なら、下向きの LS 定理により ZFC は可算モデルをもちます。ところが ZFC はその内部で「非可算集合が存在する」ことを証明します。矛盾に見えますが、「非可算」という性質は「$\omega$ から $X$ への全単射が**モデルの内部に**存在しない」ことを意味するだけです。可算モデルの外から見れば全単射は存在しても、それがモデルの元でなければ、モデルは自分の中の集合を非可算と判定します。「非可算」はモデルに相対的な性質であり、構造を外から見たときの基数とは別です。
</Remark>

## 7. 演習

<Exercise id="exr-valid" difficulty="標準">
$L$ を 2 変数関係記号 $R$ をもつ言語とする。(1) 文 $\exists x\forall y\,R(x,y)\to\forall y\exists x\,R(x,y)$ はすべての構造で成り立つことを意味論から示せ。(2) 逆向きの含意 $\forall y\exists x\,R(x,y)\to\exists x\forall y\,R(x,y)$ は妥当でないことを、反例の構造を与えて示せ。
<Solution>
(1) 構造 $\mathcal{M}$ が $\exists x\forall y\,R(x,y)$ を満たすとする。そのような $a\in M$ を一つ取る。任意の $b\in M$ について $R(a,b)$ が成り立つ。よって各 $b$ に対して $x=a$ が $R(x,b)$ を満たすので、$\mathcal{M}\models\forall y\exists x\,R(x,y)$。
(2) 領域を $\mathbb{N}$、$R^{\mathcal{M}}=\{(m,n)\mid m\ge n\}$ とする。各 $n$ に対して $x=n$ をとれば $R(n,n)$ なので $\forall y\exists x\,R(x,y)$ は成り立つ。一方、どの $m$ についても $R(m,m+1)$ は偽なので、$\exists x\forall y\,R(x,y)$ は成り立たない。含意は偽。量化子の順序は交換できません。
</Solution>
</Exercise>

<Exercise id="exr-torsion" difficulty="標準">
群の言語の理論 $\Sigma$ について、「モデルがちょうど捩れ群（すべての元が有限位数の群）全体である」ものは存在しないことを、コンパクト性定理から示せ。
<Solution>
そのような $\Sigma$ があったとする。定数 $c$ を加え、$\Sigma'=\Sigma\cup\{\neg(c^n=e)\mid n\ge1\}$ を考える。有限部分集合に現れる $n$ の最大値を $N$ とし、巡回群 $\mathbb{Z}/(N+1)\mathbb{Z}$ を（これは捩れ群で $\Sigma$ のモデル）、$c$ を生成元 $1$ と解釈すると、$1\le n\le N$ で $c^n\ne e$ だから有限部分集合は満たされる。コンパクト性定理により $\Sigma'$ のモデルがあり、そこでは $c$ はどの $n\ge1$ についても $c^n\ne e$、つまり無限位数の元である。しかしこれは $\Sigma$ のモデル、つまり捩れ群のはずである。矛盾。
</Solution>
</Exercise>

<Exercise id="exr-gen" difficulty="標準">
この記事の証明体系で仮定 $\Gamma$ を文に限った理由を、次の観察から説明せよ。仮定に論理式 $P(x)$（$x$ が自由）を許し、一般化を自由に使うと $\{P(x)\}\vdash\forall x\,P(x)$ が導出できてしまう。これが演繹定理と健全性をどう壊すか。
<Solution>
$\{P(x)\}$ から $P(x)$ を取り、一般化で $\forall x\,P(x)$ が得られる。演繹定理が成り立つなら $\vdash P(x)\to\forall x\,P(x)$ となるはずだが、領域 $\{0,1\}$、$P=\{0\}$、$s(x)=0$ では $P(x)$ が真で $\forall x\,P(x)$ が偽なので、この論理式は妥当でない。演繹定理の証明で壊れるのは一般化の場合で、(L4) $\sigma\to\forall x\,\sigma$ が $x\in\mathrm{FV}(\sigma)$ のとき使えないところである。仮定を文に限れば (L4) が常に使え、しかも $\Gamma\models\varphi$ を「$\Gamma$ のモデルで $\varphi$ が**すべての**割り当てで成り立つ」と定めておくことで、一般化が健全性を保つ（<Ref to="thm-soundness" /> の証明の最後の場合）。
</Solution>
</Exercise>

<Exercise id="exr-ls-real" difficulty="易">
言語 $\{0,1,+,\cdot,<\}$ での $\mathbb{R}$ の完全な理論 $\mathrm{Th}(\mathbb{R})$ は、可算モデルをもつことを示し、その可算モデルが $\mathbb{R}$ と同型でないことを説明せよ。
<Solution>
言語は有限だから可算。$\mathbb{R}$ は $\mathrm{Th}(\mathbb{R})$ のモデルなので、<Ref to="thm-ls" />(1) により高々可算なモデル $\mathcal{K}$ がある。$\mathrm{Th}(\mathbb{R})$ は各 $n$ について $\underbrace{1+\cdots+1}_{n}\ne0$ を含むので、$\mathcal{K}$ は有限ではなく可算無限である。$\mathbb{R}$ は非可算（<Ref to="mathematics/foundations/cardinality-and-infinity#thm-r-uncountable" />）だから、$\mathcal{K}$ との間に全単射は存在せず、同型でない。実代数的数全体のなす順序体が一例であることが知られている。完備性（上限の存在）は集合の量化を含むので、一階の文では表せない。
</Solution>
</Exercise>

## 参考文献

- H. B. Enderton, *A Mathematical Introduction to Logic*, 2nd ed., Academic Press, 2001 — 第 2 章（一階論理、完全性定理とコンパクト性定理）。
- D. van Dalen, *Logic and Structure*, 5th ed., Springer, 2013 — 第 3 章（完全性定理）。
- K. Gödel, "Die Vollständigkeit der Axiome des logischen Funktionenkalküls", *Monatshefte für Mathematik und Physik* 37 (1930), 349–360.
- L. Henkin, "The completeness of the first-order functional calculus", *The Journal of Symbolic Logic* 14 (1949), 159–166.
- 田中一之編『ゲーデルと 20 世紀の論理学』東京大学出版会、2006–2007。