コンパクト性定理

対偶を証明する:$\Sigma$ がモデルを持たないならば、ある有限な $\Sigma_0 \subseteq \Sigma$ がモデルを持たない。

$\Sigma$ が充足不可能であると仮定する。一階論理に対するゲーデルの完全性定理(意味論的帰結と構文的導出可能性は一致する:$\Sigma \models \bot$ iff $\Sigma \vdash \bot$)により、$\Sigma$ が充足不可能であることは $\Sigma$ が構文的に矛盾していること、すなわち $\Sigma \vdash \bot$——$\Sigma$ から矛盾が形式的に導出可能であること——と同値である。

形式的導出は定義により、各行が公理、$\Sigma$ からの前提、あるいは先行する行への推論規則の適用のいずれかによって正当化される、論理式の有限列である。$\bot$ の導出は有限なので、$\Sigma$ からの前提は有限個しか引用されない。それらを有限集合 $\Sigma_0 = \{\sigma_1, \dots, \sigma_n\} \subseteq \Sigma$ にまとめる。

$\Sigma_0$ からの前提のみを使ったまさにその同じ有限の導出が、$\Sigma_0 \vdash \bot$ を証拠立てる。一階論理の健全性(導出可能性は帰結を含意する)により、$\Sigma_0 \models \bot$、すなわち $\Sigma_0$ は充足不可能である——モデルを持たない。

こうしてモデルを持たない有限な $\Sigma_0 \subseteq \Sigma$ を作り出したので、対偶が証明された。同値に言えば:$\Sigma$ のすべての有限部分集合がモデルを持つならば、そのような矛盾した有限導出は存在しえないので、$\Sigma$ は充足不可能ではありえず、したがって $\Sigma$ はモデルを持つ。