一阶理论

语言规定能问哪些问题，公理排除不允许的结构，后承则收集剩下所有结构一致给出的答案。增加公理会缩小模型类、扩大后承集合：若 $T\subseteq T^{\prime }$，则 $\mathrm{Mod}(T^{\prime })\subseteq \mathrm{Mod}(T)$。

完备理论要求所有模型对每个句子意见一致，并不要求它们是同一个结构或彼此同构。句子能观察到的结构信息少于一个逐元素同构所保留的信息；把这两种“确定程度”分开，才能理解非标准模型和模型论中的分类问题。

用一个句子检验群论的不完备性 ​

群语言含单位元 $e$、乘法与逆元，群公理形成理论 $T_{\mathrm{grp}}$。令

整数加法群满足 $\phi$，而三字母置换群 $S_3$ 不满足：按从右向左复合，$(12)(23)=(123)$，$(23)(12)=(132)$。因此群公理既不蕴涵 $\phi$，也不蕴涵 $\mathrm{\neg }\phi$，所以不完备。这里关键是找到对同一句子给出相反答案的两个模型；仅有两个非同构模型并不足够。

完备不等于唯一模型或可计算 ​

无端点稠密线性序理论是完备的，其可数模型都与 $(\mathbb{Q},<)$ 同构，但 $(\mathbb{R},<)$ 也是模型。两者基数不同，当然不同构。这个例子同时区分完备性与给定基数上的范畴性。它的完备性可由稠密线性序的量词消去公理库稠密线性序的量词消去Quantifier elimination for dense linear orders · DLO 量词消去在无端点稠密线性序中，以所有下界小于所有上界消去存在量词，并构造避开有限禁点的见证。直接验证：纯序语言中的句子消去后化为真或假，因而所有模型答案一致。一般的量词消去公理库量词消去Quantifier elimination在固定语言和理论的全部模型中，把任意公式化为保持参数真值的无量词公式。还须检查无量词句是否已被理论决定，才能推出完备性。

通常算术语言下的 $\mathrm{Th}(\mathbb{N})$ 包含全部自然数真句，所以完备，却不可递归枚举；若它可有效公理化，就会与算术不完备性结论冲突。Peano 算术是另一回事：它有有效公理表示，但不决定所有算术句子，也有非标准模型。

空理论允许该语言的所有结构，它的后承正是逻辑有效句。不相容的理论则没有模型，因而语义上蕴涵每个句子及其否定；这就是定义完备性时保留可满足性条件的理由。若一个句子独立于一致理论，则加入它或加入其否定都会给出一致扩张，但任一次加入未必已经使理论完备。

结构公理库一阶结构First-order structure · Interpretation为一阶语言中的常元、函数符号和关系符号指定集合上解释的数学结构。只有满足所选公理后才是该理论的模型。公理化把代数、序与算术问题转为对模型类的研究；消去量词、紧致性和模型谱进一步描述哪些结构信息能由句子固定。

一阶可靠性公理库一阶逻辑可靠性定理Soundness theorem for first-order logic一阶证明系统中可证的公式在每个模型中都语义有效。给出 $T⊢\phi \Rightarrow T\models \phi$，经典一阶完备性公理库一阶逻辑完备性定理Gödel completeness theorem · Completeness theorem for first-order logic每个语义有效的一阶公式都可在合适证明系统中形式证明。给出反方向。这是演算与语义的对应，不能与“某个 $T$ 是否决定每个句子”的理论完备性混淆。