コンパクト性定理とその応用

一階論理のコンパクト性定理は、文の集合の任意の有限部分が充足可能なら、集合全体も充足可能だと述べる。無限の要件の整合性を、有限部分の検査へ落とす重要な性質である。

要件を論理式にし、有限部分で成立するモデルがあることを確認する。データベースの依存関係やモデル理論の存在証明などでは、有限近似から全体の存在を導く形で使われる。

定理は一階論理の意味論と公理系に依存し、モデルを具体的に構成する手順や計算量を与えない。存在保証と実装可能なアルゴリズムを分けて扱う。