一阶逻辑

一阶逻辑（First-Order Logic，简称FOL），亦称谓词逻辑或量化逻辑，是数理逻辑的核心分支之一，也是现代逻辑学中研究最深入、应用最广泛的形式系统。它在命题逻辑的基础上引入了谓词（表示个体性质或关系）与量词（对个体变元进行约束），从而具备了远强于命题逻辑的表达能力。与命题逻辑只能处理命题间的关系不同，一阶逻辑能够深入分析命题的内部结构，从而刻画个体之间的复杂关系。一阶逻辑是现代数学基础、计算机科学理论、语言学以及人工智能中知识表示的核心形式工具。

语法构成

一阶逻辑的语言字母表包含：个体常元（如 $a, b, c$）、个体变元（如 $x, y, z$）、函数符号（如 $f, g, h$）、谓词符号（如 $P, Q, R$）、逻辑联结词（$\neg, \land, \lor, \rightarrow, \leftrightarrow$）、量词（$\forall, \exists$）以及可选的等号（$=$）。项由常元、变元和函数符号递归生成，代表论域中的个体对象——例如，若 $f$ 为一元函数符号而 $a$ 为常元，则 $f(a)$ 是一个项。原子公式是将谓词符号应用于适当数量的项所得，如 $P(a)$ 或 $R(x, f(y))$。原子公式经由逻辑联结词和量词组合即形成合式公式。量词的作用范围（即辖域）覆盖紧随其后的公式；被量词约束的变元称为约束变元，未被量词约束的变元则为自由变元。不包含自由变元的公式称为封闭公式（语句），它是逻辑评价和推理的基本单位。

语义与模型

一阶逻辑的语义建立在结构（亦称模型）之上。一个结构 $\mathcal{M}$ 包含一个非空论域 $D$，并为每个常元指派 $D$ 中的一个特定元素，为每个函数符号指派一个 $D$ 上的函数，为每个谓词符号指派一个 $D$ 上的关系。公式的真值通过塔斯基（Tarski）定义的满足关系递归给出：$\mathcal{M} \models \varphi$ 表示公式 $\varphi$ 在结构 $\mathcal{M}$ 下为真。

由此派生出两个关键概念：可满足性——存在某个结构使公式为真；有效性（普遍有效性）——公式在所有结构下皆为真。一阶逻辑最重要的元性质之一——紧致性定理断言：一个公式集是可满足的当且仅当其每个有限子集都是可满足的。这一定理是模型论大厦的基石，由此可以推出一系列深刻的结论，例如非标准模型的存在性。

推理系统与元逻辑

一阶逻辑拥有多种等价的推理系统，包括希尔伯特风格公理系统、自然演绎和相继式演算。这些系统通过公理模式和推理规则（如分离规则、全称引入规则）刻画语法上的推演关系。哥德尔于1929年在其博士论文中证明了完备性定理：一阶逻辑中，公式 $\varphi$ 是有效的当且仅当 $\varphi$ 是可证明的。换言之，语义上的真与语法上的可证完全吻合。这一结果彰显了一阶逻辑在元逻辑层面的优美自洽。

然而，哥德尔不完备定理同时指出：任何包含一阶算术的递归可公理化理论，如果是一致的，则必定是不完备的——存在既不可证明也不可否证的命题。此外，勒文海姆–斯科伦定理表明，如果一个一阶理论有无限模型，则它拥有任意大基数的模型，这也揭示了一阶逻辑在刻画无限结构方面的根本局限。

判定问题

丘奇和图灵各自独立证明了一阶逻辑的判定问题（可满足性问题）是不可判定的：不存在通用算法能在有限步内判定任意一阶公式是否可满足。这意味着，尽管一阶逻辑的表达力强于命题逻辑，但其推理问题在计算上本质上是不可解的。作为对比，命题逻辑的判定问题（如真值表法）是可判定的，而一阶逻辑的不可判定性来源于量词的无限展开可能性。

应用领域

在数学基础中，集合论（ZFC公理系统）和数学各分支的公理化均建立在一阶逻辑之上。在计算机科学中，一阶逻辑是程序验证（霍尔逻辑）、数据库查询语言（SQL的关系代数核心等价于一阶逻辑）、自动定理证明（归结原理与SLD归结）以及知识表示的基础。在人工智能中，一阶逻辑被用于语义网的本体语言（如OWL 2的底层描述逻辑）和规划系统。在语言学和分析哲学中，一阶逻辑为自然语言语义分析提供了精确的形式工具。

与高阶逻辑的对比

一阶逻辑仅允许对个体变元进行量化，而不允许对谓词或函数进行量化。高阶逻辑允许量化谓词和函数，表达力更强，但丧失了完备性和紧致性等理想元性质。这种表达力与可判定性之间的权衡，使得一阶逻辑成为实际应用中最广泛采用的逻辑系统。此外，一阶逻辑的常见扩展包括带等词的一阶逻辑、多类一阶逻辑以及模态一阶逻辑，这些扩展在保持一阶量化框架的同时增加了针对特定领域的表达能力。

综上，一阶逻辑以其恰到好处的表达力、完备的推理系统和深刻的元逻辑性质，成为逻辑学、数学、计算机科学和哲学交汇处的核心理论。它对"什么是严格证明"这一根本问题的形式化回答深刻影响了整个现代科学的面貌。