Logo

Nola's Backyard

ゲーテルの完全性定理

一階述語論理では、理論 TT を満たすすべての
モデルで論理式 φ\varphi が真ならば、TT から φ\varphi を形式的に証明できる。

T⊨φ⟹T⊢φ T \models \varphi \quad\Longrightarrow\quad T \vdash \varphi
  • T⊨φT \models \varphi：TT のすべてのモデルで φ\varphi が真（意味論）
  • T⊢φT \vdash \varphi：公理と推論規則から φ\varphi の有限な証明を作れる（構文論）
Hint

つまり、一階述語論理では「意味的に必ず正しいが、形式的には証明できない」という取りこぼしがない。

Exapmle

すべての群では、各要素について

(x−1)−1=x (x^{-1})^{-1}=x

が成り立つ。φ\varphi を ∀x ((x−1)−1=x)\forall x\,((x^{-1})^{-1}=x) とすれば、これは

Tgroup⊨φ T_{\mathrm{group}} \models \varphi

と表せる。完全性定理は、この意味論的な事実から、群の公理だけを使った形式的証明も存在すること、すなわち

Tgroup⊢φ T_{\mathrm{group}} \vdash \varphi

を保証する。

Note

同値な表現として、次のモデル存在定理がある。

一階の理論 TT が無矛盾ならば、TT を満たすモデルが存在する。

なお、逆向きの T⊢φ⇒T⊨φT \vdash \varphi \Rightarrow T \models \varphi は健全性定理である。