一阶逻辑紧致性定理

一阶逻辑公理库一阶逻辑First-order logic · Predicate logic在命题逻辑上加入对象、关系、函数与量词的形式语言和模型语义。中的矛盾总能由有限信息见证；无限约束只要每个有限片段兼容，就存在统一模型。

紧致性说，一组可能无限的句子若每个有限子集都能同时满足，那么整组也有模型。有限观察无法发现矛盾，就不存在只在“无限尾部”突然出现的矛盾。它把局部有限一致性提升为全局可满足性公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。，是一阶逻辑能够处理无限结构却仍受有限证明控制的核心特征。

用“至少有 $n$ 个元素”的句子族可构造无限模型。紧致性不适用于完整二阶语义，也不保证模型有限或可计算。

向自然数的一阶理论加入常元 $c$ 与句子 $c>\overline{n}$（每个标准自然数 $n$ 一条）。任何有限子集都能在标准结构 $\mathbb{N}$ 中通过把 $c$ 解释成足够大的数而满足；整组句子在 $\mathbb{N}$ 中不可满足，但紧致性保证它与该理论共同拥有一个模型，其中 $c$ 大于每个标准数码所表示的元素。这给出含非标准元素的模型；改用完整二阶语义时，紧致性一般失效。

它产生非标准模型、不可公理化结果和 Löwenheim–Skolem 型构造。

由 一阶逻辑完备性定理公理库一阶逻辑完备性定理Gödel completeness theorem · Completeness theorem for first-order logic每个语义有效的一阶公式都可在合适证明系统中形式证明。可推出紧致性：若全体不可满足，矛盾有有限证明，只使用有限多前提。它进一步导出 Löwenheim–Skolem 定理公理库Löwenheim–Skolem 定理Löwenheim–Skolem theorem有无限模型的一阶理论在适当基数上存在较小或较大的模型。、非标准模型和图论中的有限到无限转移。