一阶逻辑

形式陈述 ​

本页是总览：一阶逻辑在命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。的联结词上增加项、谓词和对象量词，并由语言、结构、满足关系与证明演算四层组成。它们共同构成一个形式系统公理库形式系统Formal system · Formal calculus由符号、形成规则、公理与推导规则组成的精确定义系统。，但句法对象、语义解释和可推导性不能混成同一层。

语言 ​

一阶语法公理库一阶逻辑语法First-order syntax以符号表、项、原子公式、联结词和量词归纳生成一阶公式的语法系统。从签名出发。签名指定常元符号，以及各个带有限元数的函数符号和关系符号；项由变量、常元和函数应用递归生成，公式则由关系式、等式、逻辑联结词与量词 $\mathrm{\forall }x,\mathrm{\exists }x$ 递归生成。变量的出现分为自由与受约束两类，没有自由变量的公式称为句子。代入必须避开变量捕获，具体递归条款由语法条目展开。

结构 ​

一个结构 $\mathcal{M}$ 给出非空论域 $M$，并把常元解释为 $M$ 中元素、$n$ 元函数符号解释为函数 $M^n\to M$、$n$ 元关系符号解释为 $M^n$ 的子集。变量赋值 $s$ 把变量送到论域元素；项 $t$ 在 $\mathcal{M},s$ 下的取值记为 $t^{\mathcal{M}}[s]$，由变量、常元和函数符号递归求得。

同一签名可以有许多结构公理库一阶结构First-order structure · Interpretation为一阶语言中的常元、函数符号和关系符号指定集合上解释的数学结构。。例如群语言中的乘法符号只规定一个二元函数位置，究竟解释为整数加法、矩阵乘法还是别的运算，要由具体结构决定；语法本身不携带这些数学含义。

满足 ​

满足关系公理库满足关系Satisfaction relation · Tarski semantics用对公式构造的递归定义刻画结构与赋值何时满足一阶公式。必须同时带结构与赋值，写作 $\mathcal{M},s\models \phi$。它沿公式结构递归定义：原子式先解释项和关系，联结词沿用真值条件，而量词通过改变一个变量的赋值来遍历论域。例如

$$\begin{array}{rl}\mathcal{M},s\models R(t_1,\dots ,t_n)& ⟺(t_1^{\mathcal{M}}[s],\dots ,t_n^{\mathcal{M}}[s])\in R^{\mathcal{M}},\\ \mathcal{M},s\models \mathrm{\exists }x\phi & ⟺\text{存在 }a\in M\text{ 使 }\mathcal{M},s[x\mapsto a]\models \phi .\end{array}$$

等式按两个项的取值相等解释，否定、合取和全称量词采用相应的递归真值条件。若 $\phi$ 是句子，其真假与 $s$ 无关，才简写为 $\mathcal{M}\models \phi$。

语义与证明 ​

若存在结构和赋值满足 $\phi$，称 $\phi$ 可满足；若每个结构和赋值都满足它，称其有效。若每个满足公式集 $\mathrm{\Gamma }$ 的结构与赋值也满足 $\phi$，记作 $\mathrm{\Gamma }\models \phi$。相对固定证明演算的句法可推导关系写作 $\mathrm{\Gamma }⊢\phi$；可靠性与完备性连接二者，但两种关系在定义上不能混同。

直觉

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

例子与边界

$\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 求解也大量使用它的可控片段。一阶语法公理库一阶逻辑语法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有无限模型的一阶理论在适当基数上存在较小或较大的模型。则共同标出这种语言的证明能力和模型边界。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001, Chapter 2.
• Wilfrid Hodges, A Shorter Model Theory, Cambridge University Press, 1997, Chapter 1.