一阶逻辑

命题逻辑把句子看成不可拆分的真假块，一阶逻辑则进入句子内部，量化个体并描述它们之间的关系，例如“每个节点都有一条出边”。这种量化并不直接越级到集合、性质或函数本身；语言中的函数与关系符号也只提供语法接口，具体含义仍由结构解释，所以同一个公式可以在不同模型中一真一假。量词与变量作用域由此显著提升表达力，同时仍保留完备性与紧致性。

若 $<$ 是严格全序，$\mathrm{\forall }x\mathrm{\exists }y(x<y)$ 表示没有最大元素。在一般严格偏序中，它实际要求没有极大元；仅仅没有最大元更弱，例如两个不可比元素都极大，却没有最大元。若 $<$ 只是任意关系符号，公式只能读成“每个对象都有一个 $<$ 后继”。一阶逻辑只能量化论域中的对象，不能直接量化所有子集或关系；后者属于二阶逻辑。

群公理可写成一阶句子，例如 $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z((xy)z=x(yz))$。在只含邻接关系的通常图语言中，连通性不能由单个一阶句子完整刻画；有限性与“标准自然数结构”本身也有这一限制，说明表达力有边界。公式 $\mathrm{\forall }x\mathrm{\exists }yR(x,y)$ 与 $\mathrm{\exists }y\mathrm{\forall }xR(x,y)$ 一般不同，量词次序不能交换。

群、序、图和集合论都可用一阶语言公理化；在计算机科学中，数据库查询、程序验证与 SMT 求解也大量使用它的可控片段。具体而言，关系演算理路关系演算Relational calculus · Domain relational calculus用一阶公式的满足条件定义关系查询，并以域独立性区分仅依赖数据库事实的查询与依赖外部论域的公式。用公式界定答案，合取查询理路合取查询Conjunctive query · CQ · Select-project-join query用关系事实的匹配定义集合答案，并以规范数据库与反向同态判定所有有限实例上的查询包含。用存在量词和事实的合取匹配选课、授课等关系；域独立条件说明为何加入表外对象不应改变查询结果。一阶语法理路一阶逻辑语法First-order syntax以符号表、项、原子公式、联结词和量词归纳生成一阶公式的语法系统。规定项、公式与自由变量，一阶结构理路一阶结构First-order structure · Interpretation为一阶语言中的常元、函数符号和关系符号指定集合上解释的数学结构。和 满足关系理路满足关系Satisfaction relation · Tarski semantics用对公式构造的递归定义刻画结构与赋值何时满足一阶公式。赋予语义；可靠性理路一阶逻辑可靠性定理Soundness theorem for first-order logic一阶证明系统中可证的公式在每个模型中都语义有效。、完备性理路一阶逻辑完备性定理Gödel completeness theorem · Completeness theorem for first-order logic每个语义有效的一阶公式都可在合适证明系统中形式证明。、紧致性理路一阶逻辑紧致性定理First-order compactness theorem · Compactness theorem一阶理论可满足，当且仅当它的每个有限子理论都可满足。与 Löwenheim–Skolem 定理理路Löwenheim–Skolem 定理Löwenheim–Skolem theorem有无限模型的一阶理论在适当基数上存在较小或较大的模型。则共同标出这种语言的证明能力和模型边界。