ゲーデルの完全性定理
完全性定理とコンパクト性定理は、一階論理の2つの基礎である。これら定理はどちらも実効的な方法で証明できないのに対して、一方からもう一方を実効的に得ることが可能である。
コンパクト性定理は、論理式 φ が一連の論理式の(無限もありうる)集合 Γ の論理的帰結であるとき、φ は Γ の有限な部分集合の論理的帰結でもある、というものである。φ の形式的推論で言及される Γ の公理は有限個であるため、これは完全性定理から直接得られる帰結である。演繹系の健全性から、φ がこの有限集合の論理的帰結となる。このコンパクト性定理の証明は本来ゲーデルに帰されるものである。
逆に多くの演繹系では、コンパクト性定理の実効的な帰結として完全性定理を証明可能である。
完全性定理の非実効性は、集合論と逆数学で測られる。集合論では、ツェルメロ=フレンケルの集合論 (ZF) では証明できない選択公理の弱い形のウルトラフィルターの補題がある。ZF では完全性定理とコンパクト性定理は等価であり、ウルトラフィルターの補題とも等しい。従って、ZFを拡張した理論は、ウルトラフィルターの補題を証明せずに完全性定理またはコンパクト性定理のどちらかを証明することができない。逆数学では、可算性の構造と可算性の理論だけが考慮される。この場合、RCA0 上で完全性定理とコンパクト性定理は等価であり、それは公理系 WKL0 とも等価である。特に、全ての無矛盾な一階理論は完全性定理とレーヴェンハイム=スコーレムの定理から有限モデルか可算モデルを持つが、計算可能モデルを持たない無矛盾な一階理論も知られている。