形式陈述

命题紧致性定理断言：任意命题公式集 $\Gamma$$\mathrm{\Gamma }$ 可满足，当且仅当它的每个有限子集都可满足。等价的后承形式是

$$ \Gamma\models\varphi \quad\Longrightarrow\quad \exists\text{有限 }\Gamma_0\subseteq\Gamma, \ \Gamma_0\models\varphi. $$$$\mathrm{\Gamma }\models \phi ⟹\mathrm{\exists }\text{有限 }{\mathrm{\Gamma }}_0\subseteq \mathrm{\Gamma },{\mathrm{\Gamma }}_0\models \phi .$$

一个证明从有限可满足性出发，把有限一致部分组织成树并取无限分支；也可由命题逻辑完备性与每份形式证明只使用有限多个前提推出。对任意大变量集的完整版本可借超滤子引理或乘积紧致性证明。

直觉

无限约束若真的矛盾，矛盾必已由有限多条约束见证；不存在“只有把无穷多条全部同时看完才首次出现”的纯命题冲突。

例子与边界

设无限图 $G=(V,E)$$G=(V,E)$ 的每个有限子图都可用固定的 $k$$k$ 种颜色正常着色。为每个顶点 $v$$v$ 和颜色 $c$$c$ 引入变量 $p_{v,c}$$p_{v,c}$，再加入“每个顶点恰取一种颜色”以及“相邻顶点不得同色”的有限命题公式。任意有限公式子集只涉及有限多个顶点，因而可由相应有限子图的着色满足；紧致性遂给出整个图的 $k$$k$-着色。这里每条公式本身仍是有限式，不能用无限析取偷换结论。定理只保证存在全局赋值，不给出有限时间内找到它的算法，尤其当公式集不可计算时。

推论与应用

紧致性用于从所有有限近似构造无限对象，并说明语义后承具有有限证据。它也是一阶紧致性和超积方法的有限真值原型。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，§1.7, compactness and effectiveness for sentential logic。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Ch. VI, compactness theorem; propositional special case。