一阶理论

理论是一组对同一类结构提出的句子约束；模型是满足全部约束的世界，理论的语义闭包则收集这些世界共同强制的所有结论。

一阶理论是一组在固定语言中的句子，可看成对允许模型施加的公理约束。理论不一定有限、完备或可判定；它可以只描述一类结构的共同性质，而不唯一确定某个模型。语义后果取所有模型的交，句法闭包则取所有可证明句子，完备性定理把两者连接。

群理论由群公理组成，有许多非同构模型，因而并不决定每个句子。固定结构 $\mathbb{N}$ 的完整理论决定每个算术句子，但其全部真句不可递归枚举。空理论的模型是该语言的所有结构。完备性与“证明系统完备”不同：前者是某个公理理论是否决定每个句子，后者是演算是否捕获所有语义后承。

群论由群公理组成，其模型是所有群；Peano 算术试图描述自然数，却还有非标准模型。稠密无端点线性序理论在可数模型间高度刚性，但仍有不同基数的模型。向理论加入某句或其否定可得到不同完备化，只要保持一致。

理论组织代数类、算术和组合结构，模型论研究其模型谱、完备性、消去量词和分类性质。公理化方式还决定自动推理和可判定性。

一阶逻辑公理库一阶逻辑First-order logic · Predicate logic在命题逻辑上加入对象、关系、函数与量词的形式语言和模型语义。提供语言与推理规则，结构公理库一阶结构First-order structure · Interpretation为一阶语言中的常元、函数符号和关系符号指定集合上解释的数学结构。成为理论的模型。可靠性公理库一阶逻辑可靠性定理Soundness theorem for first-order logic一阶证明系统中可证的公式在每个模型中都语义有效。和完备性刻画可证明后果，紧致性、模型完备性与可判定性则研究公理集合的全局性质。