「証明できる」ことと「本当は正しい」ことは、いつも一致するんだろうか。
たとえば、こんな推論を考えてほしい。
すべての人間は死ぬ。ソクラテスは人間だ。よってソクラテスは死ぬ。
この推論が「正しい」ことは、直観的には明らかだ。でも、その「正しさ」をどうやって保証するのか。論理学には二つのアプローチがある。
一つは証明論（⊢）。推論規則に従って証明木を組み立てられたら、その推論は「証明できた」と見なす。規則の一覧さえ決めてしまえば、あとは機械的に正しさを判定できる。計算機で扱うにはうってつけだ。
もう一つは意味論（⊨）。「前提が全部真なら結論も真」という関係──すなわち論理的帰結──で正しさを定義する。具体的な世界（モデル）を考えて、そこで本当にそうなっているかを確かめる。こちらの方が、直観には近い。
この二つは、同じ対象を別の角度から捉えている。では──
「証明できる」ことと「論理的に正しい」ことは、本当に一致するのか？
これに「Yes」と答えるのが、ゲーデルの完全性定理だ。驚くべきことに、二つの正しさは一致する──Γ ⊨ A ⇔ Γ ⊢ A。右向き（証明できれば真）が健全性、左向き（真なら証明できる）が完全性と呼ばれる。順に見ていこう。
健全性 —— 証明できれば、確かに正しい
健全性 Γ ⊢ A ⇒ Γ ⊨ A は、直観に照らせば当然に思える。規則が正しく設計されていれば、その規則で組み立てた証明は間違いようがないはずだ。
証明の方針は「証明木の構造に関する帰納法」の一言に尽きる。
- 証明木が仮定1つだけのとき：A が Γ に含まれているのだから、Γ ⊨ A は明らか。
- ∧I, ∧E, →I, →E, ⊥E, RAA……どの規則で終わっている場合も、その直前の部分証明について帰納法の仮定を使えば、「規則を使っても真が保たれる」ことを確認できる。
ただそれだけだ。一つ一つの規則について「この推論は正しい形をしている」ことを確かめていけば、証明は自然とできあがる。だから健全性は「比較的容易」と言われる。
これで「証明できるなら正しい」は保証された。
問題は逆だ。
正しいなら、必ず証明できるのか？
つまり、Γ ⊨ A が成り立つのに、Γ ⊢ A が成り立たない──そんなケースはあり得ないのか、と。直観的には「そりゃそうでしょ」と思いたいところだが、証明するとなると話は別だ。「証明できない」という状態を扱うのは、そもそも難しい。
完全性 —— 正しいなら、必ず証明できる
証明の基本的なアイデアは「直接示せないなら対偶を取る」だ。
示したいのは Γ ⊨ A ⇒ Γ ⊢ A。この対偶、
Γ ⊬ A ⇒ Γ ⊭ A
を証明する。つまり「Aが証明できないなら、Γを全部真にしてAだけ偽にする反例がある」ことを示せばいい。
ここから先は、ひたすら「反例を作る」ための工作が続く。
反例を作るための4ステップ
Step 1. Aが証明できない = Γ ∪ {¬A} は無矛盾
Γ ⊬ A なら、Γ に ¬A を追加しても矛盾しない（Lemma 4）。これは「Aじゃない世界を考えても問題ない」という意味だ。反例への第一歩になる。
Step 2. 矛盾しないギリギリまで膨らませる（リンデンバウム）
Γ ∪ {¬A} を出発点に、「この式を追加してもまだ矛盾しないか？」と一つずつ確かめながら、無限に追加していく。できあがるのが極大無矛盾集合 Γ*（Lemma 5）。これ以上何か追加すると、たちまち矛盾してしまうギリギリの状態だ。
ここが証明で最も技巧的な部分だが、直観は単純だ。「この世界では何が真で何が偽か」を完全に決め切ってしまいたい。そのために、可能な限り多くの式を詰め込んでいる。
Step 3. 極大無矛盾の性質を引き出す
極大無矛盾集合 Γ* には、便利な性質がいくつも成り立つ。
- Γ* は証明について閉じている：Γ* ⊢ A なら A ∈ Γ*（Lemma 6）。せっかくギリギリまで詰め込んだのだから、証明できる式は全部入っていてほしい。実際そうなっている。
- 任意の A について、A ∈ Γ* か ¬A ∈ Γ* のどちらか一方だけが成り立つ（Lemma 7）。矛盾しない範囲で最大まで詰め込んだので、「Aか¬Aか」が必ず決まる。
これで Γ* は、「真偽の割り当て」として振る舞う準備が整った。
Step 4. Γ からモデルを構成する（真理補題）*
ここがゴールだ。Γ* から直接、評価 v を作る。
- 原子論理式 P が Γ* に入っていたら、v(P) = T
- 入っていなければ v(P) = F
この v を論理式全体に拡張すると、驚くべきことが成り立つ（Lemma 8）。
A_v = T ⇔ A ∈ Γ*
つまり「Γ* に入っている式＝vで真になる式」だ。これが真理補題。Γ* の要素をそのまま「真の世界」に変換できたことになる。
もともと Γ ∪ {¬A} ⊆ Γ* だったから、この評価 v は Γ の全式を真にし、A だけを偽にする。めでたく反例ができた。
結論
以上で Γ ⊬ A ⇒ Γ ⊭ A が示せた。対偶を取れば Γ ⊨ A ⇒ Γ ⊢ A。健全性と合わせて、完全性定理 Γ ⊨ A ⇔ Γ ⊢ A が完成する。
この証明が教えてくれるのは、次のことだ。
論理の規則は、「本当に正しい推論」を過不足なく捉えている。
もし「正しいのに証明できない」推論があったら、この証明で作った反例（モデル）が見つかるはずだ。でも、その反例の存在自体が「前提は真で結論は偽」の世界があることを意味するから、その推論は「正しい」とは言えない。完全性定理は、この循環を断ち切って、「証明可能性」と「論理的帰結」が完全に一致することを示している。
その後 —— コンパクト性定理への応用
完全性定理からは、もう一つ重要な帰結が得られる。コンパクト性定理だ。
式集合 Γ が充足可能 ⇔ Γ の任意の有限部分集合が充足可能
「無限にたくさんの条件があっても、そのどんな有限部分を取っても矛盾しないなら、全体として矛盾しないモデルが存在する」という主張だ。完全性定理を使って証明できる。
この定理の面白いところは、無限の問題を有限の問題に落とし込めることにある。たとえば無限グラフの彩色問題。「任意の有限部分グラフがk色で塗れるなら、無限グラフ全体もk色で塗れる」という事実は、コンパクト性定理の応用例だ。完全性定理が単なる理論的な「一致」に留まらず、実際に使える道具でもあることを示している。
Lemmas 一覧
| Lemma | 内容 | 役割 |
|---|---|---|
| Lemma 1 | 健全性 Γ ⊢ A ⇒ Γ ⊨ A | 証明できれば真 |
| Lemma 2 | 無矛盾の3つの同値条件 | 無矛盾の定義を整理 |
| Lemma 3 | モデルがあれば無矛盾 | モデル存在→無矛盾（健全性から） |
| Lemma 4 | 矛盾から証明へ：Γ∪{¬A}矛盾⇒Γ⊢A | 対偶への足場 |
| Lemma 5 | リンデンバウム：無矛盾→極大無矛盾 | ギリギリまで膨らませる |
| Lemma 6 | 極大無矛盾は証明について閉じる | 証明できたら全部入ってる |
| Lemma 7 | 極大無矛盾での¬と→の振る舞い | 真偽の割り当てとして使える形に |
| Lemma 8 | 真理補題：A_v=T ⇔ A∈Γ* | 極大集合からモデルを構成 |
| Cor 1 | Γ⊬A⇒反例あり | 完全性の対偶を示した |