命题紧致性定理

命题紧致性断言：无限公式集若真的不可满足，矛盾必已由某个有限子集见证，不会“只有把无穷多条全部看完才首次出现”。每条公式只涉及有限多个命题变量，有限证明也只使用有限前提；紧致性把这种局部有限性提升到整个集合。它不同于拓扑紧致性的定义，却可通过 Cantor 空间的拓扑紧致性解释。

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

紧致性依赖每条命题公式都是有限长的。若允许可数无限合取，可取

任意有限子集都可满足：把其中要求为真的有限多个 $p_n$ 设真，再把某个未被要求的 $p_m$ 设假；但整个 $\mathrm{\Gamma }$ 不可满足。这个反例不属于普通命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。，因为其中出现了无限长公式。标准紧致性只保证全局赋值存在，不提供寻找该赋值的有效算法。若改在 ZF 中追踪任意变量集版本的强度，还必须显式注明所用的 Boolean Prime Ideal Theorem／超滤子引理；它弱于完整 AC，却不是一般可省略的纯逻辑背景。

可满足性公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。给出语义表述，命题逻辑可靠性与完备性公理库命题逻辑可靠性与完备性定理Soundness and completeness of propositional logic命题演算中的可证性与对所有赋值成立的语义蕴涵恰好一致。则可由证明的有限性推出紧致性。它用于从有限近似构造无限对象、图着色的有限到无限转移和布尔代数，并说明语义后承具有有限证据；它还是一阶紧致性与超积方法的有限真值原型。