一阶逻辑紧致性定理

每个有限检查都通过，并不在任意数学问题里保证全部约束能同时实现。紧致性是经典一阶语义的一项特殊性质：若无限约束真的相互冲突，冲突一定已经藏在有限片段内。它不提供“取所有有限模型的并”这样的通用算法。

可以从证明的长度理解它。若 $T$ 无模型，完备性定理公理库一阶逻辑完备性定理Gödel completeness theorem · Completeness theorem for first-order logic每个语义有效的一阶公式都可在合适证明系统中形式证明。保证从 $T$ 可推导矛盾。一次正式证明是有限对象，只引用有限多条前提，记为 $T_0$；由证明系统的可靠性公理库一阶逻辑可靠性定理Soundness theorem for first-order logic一阶证明系统中可证的公式在每个模型中都语义有效。，$T_0$ 也无模型。这与每个有限片段可满足相冲突。此处完备性把语义失败送到语法，证明的有限性截取前提，可靠性再把矛盾送回语义，三步各有作用。

大于每个标准数的元素 ​

取标准自然数结构的一阶理论，添加一个新常元 $c$，并加入 $c>\overline{n}$，对每个标准自然数 $n$ 各写一句。任何有限片段只提及有限多个数码；在通常的自然数结构中，把 $c$ 解释成比其中最大数更大的自然数，就能满足该片段。

整个句子集却不能在标准自然数结构中成立：若 $c$ 是通常的自然数 $m$，片段中总有一句 $c>\overline{m}$。紧致性仍保证存在另一个模型，其中 $c$ 超过所有标准数码。它不是通常意义的“最大自然数”：原有理论仍断言每个数有更大的数，所以模型中也有元素大于 $c$。

为什么不能刻画全部有限结构 ​

设某个一阶理论 $F$ 恰好以所有有限非空结构为模型。对每个 $n\ge 1$，令 ${\sigma }_n$ 断言存在 $n$ 个两两不同的元素。$F\cup \{{\sigma }_n:n\ge 1\}$ 的任意有限片段都有足够大的有限模型，紧致性便给出一个满足全部 ${\sigma }_n$ 的无限模型，同时它还满足 $F$，矛盾。

因此有限性不能由一阶句子集在全部结构中刻画。若只允许有限模型，这个例子本身就展示紧致性失败；换成完整二阶语义也不再享有一般紧致性。定理同样不保证模型可计算，或给出寻找模型的有限程序。

非标准模型展示了“全部一阶约束相同”与“就是原来的结构”之间的距离。紧致性还参与向上 Löwenheim–Skolem 构造公理库Löwenheim–Skolem 定理Löwenheim–Skolem theorem有无限模型的一阶理论在适当基数上存在较小或较大的模型。：加入大量两两不同的新常元，逐个有限片段验证可满足，再得到足够大的模型；精确控制基数还需其他步骤。

若还要保留给定结构的全部带参数公式，可以把它的初等图表一并加入约束。参数类型公理库模型论中的参数类型Model-theoretic type · Partial type · Complete type · 参数类型用带参数的一阶公式描述一个可能的元素，借初等图表实现类型，并以有理数上的无理割区分有限可满足、实现与省略。据此把有限可满足的条件清单放进一个初等扩张：有理数上的无理割在每次有限检查中都有有理数见证，整份清单却需要扩张中的新元素来实现。

有限到无限的图论转移也可借此表达。例如固定有限颜色数，把每个顶点选色与相邻顶点异色写成约束；若所有有限子图都可着色，每次有限检查都能满足，于是得到全图着色。关键是先写清统一语言和局部约束，不能只凭“每个小例子都成立”就套用定理。