个体与谓词
个体常元与个体变元
个体常元（Individual Constant）是指指称特定个体的符号，通常用小写字母如 \(a, b, c\) 表示，例如“地球”可记作 \(e\)。个体变元（Individual Variable）则代表未指定的个体，常用 \(x, y, z\) 等字母表示，其取值范围构成论域。区分常元与变元是量化分析的基础：常元锁定具体对象，变元则用于构造量化命题。
谓词符号与元数
谓词符号（Predicate Symbol）描述个体间的关系或属性，通常用大写字母如 \(P, Q, R\) 表示。元数（Arity）指谓词所关联的个体数目：一元谓词表示性质（如“是红色”记作 \(R(x)\)），二元谓词表示二元关系（如“大于”记作 \(G(x, y)\)），以此类推。零元谓词可视为命题常元。
量词
全称量词
全称量词（Universal Quantifier）用符号 \(\forall\) 表示，意为“对于所有”。形如 \(\forall x \, P(x)\) 的公式读作“对于所有 \(x\)，\(P(x)\) 成立”。全称量词约束变元 \(x\)，表示论域中的每一个体均满足条件。
存在量词
存在量词（Existential Quantifier）用符号 \(\exists\) 表示，意为“存在某个”。形如 \(\exists x \, P(x)\) 读作“存在某个 \(x\)，使得 \(P(x)\) 成立”。存在量词要求论域中至少有一个体满足条件。
量词的辖域
量词的辖域（Scope）指量词所作用的子公式范围。例如在 \(\forall x (P(x) \land Q(x))\) 中，\(\forall x\) 的辖域是 \(P(x) \land Q(x)\)。若辖域中出现同一变元的不同量词，则需区分约束与自由出现。辖域的清晰界定避免了量化歧义。
项与公式
项的递归定义
项（Term）是表示个体的表达式，递归定义如下：
- 个体常元和个体变元是项。
- 若 \(f\) 是 \(n\) 元函数符号，且 \(t_1, \ldots, t_n\) 是项，则 \(f(t_1, \ldots, t_n)\) 是项。
- 只有有限次使用上述两条规则生成的表达式是项。
函数符号通常用小写字母 \(f, g, h\) 表示，例如 \(f(x, a)\) 是一个项。
原子公式与复合公式
原子公式（Atomic Formula）由 \(n\) 元谓词符号和 \(n\) 个项组成，形如 \(P(t_1, \ldots, t_n)\)。复合公式（Compound Formula）通过逻辑连接词（\(\neg, \land, \lor, \rightarrow, \leftrightarrow\)）和量词将原子公式连接而成。例如 \(\forall x \, (P(x) \rightarrow Q(f(x)))\) 是一个复合公式。
自由变元与约束变元
变元在公式中的出现可分为自由（Free）和约束（Bound）。若变元处于某个量词的辖域内且与量词中的变元相同，则称该出现为约束的；否则为自由的。例如在 \(\exists y \, (P(x) \land Q(y))\) 中，\(x\) 是自由的，\(y\) 是约束的。自由变元使得公式的真值依赖于赋值，而约束变元则被量化消除。
形式语言
字母表与语法规则
一阶逻辑的形式语言由以下成分构成：
- 逻辑符号：\(\neg, \land, \lor, \rightarrow, \leftrightarrow, \forall, \exists\)、括号及逗号。
- 非逻辑符号：个体常元符号集、函数符号集、谓词符号集（每个符号自带元数）。
- 变元符号集（可数无限）。
语法规则定义如何组合这些符号生成合式公式。规则采用递归方式，保证每个公式有唯一分解。
合式公式的递归定义
合式公式（Well-Formed Formula, WFF）递归定义如下：
- 原子公式是合式公式。
- 若 \(\varphi\) 是合式公式，则 \(\neg \varphi\) 是合式公式。
- 若 \(\varphi\) 和 \(\psi\) 是合式公式，则 \((\varphi \land \psi)\)、\((\varphi \lor \psi)\)、\((\varphi \rightarrow \psi)\)、\((\varphi \leftrightarrow \psi)\) 是合式公式。
- 若 \(\varphi\) 是合式公式，\(x\) 是个体变元，则 \(\forall x \, \varphi\) 和 \(\exists x \, \varphi\) 是合式公式。
- 只有有限次使用上述规则生成的表达式是合式公式。
解释与模型
论域与赋值
解释（Interpretation）为一个公式提供语义内容。它由如下要素组成：
- 非空集合 \(D\) 作为论域（Domain）。
- 每个个体常元 \(c\) 对应 \(D\) 中的一个元素 \(c^{\mathcal{I}}\)。
- 每个 \(n\) 元函数符号 \(f\) 对应 \(D^n\) 到 \(D\) 的函数 \(f^{\mathcal{I}}\)。
- 每个 \(n\) 元谓词符号 \(P\) 对应 \(D^n\) 上的一个子集 \(P^{\mathcal{I}}\)（即关系）。
赋值（Assignment）为每个个体变元指定 \(D\) 中的一个值，通常记作 \(s: \text{Var} \to D\)。
真值条件
在解释 \(\mathcal{I}\) 和赋值 \(s\) 下，公式的真值递归定义如下：
- 原子公式 \(P(t_1, \ldots, t_n)\) 为真当且仅当 \(\langle t_1^{\mathcal{I}, s}, \ldots, t_n^{\mathcal{I}, s} \rangle \in P^{\mathcal{I}}\)。
- \(\neg \varphi\) 为真当且仅当 \(\varphi\) 为假。
- \(\varphi \land \psi\) 为真当且仅当 \(\varphi\) 和 \(\psi\) 均为真；其余连接词类似。
- \(\forall x \, \varphi\) 为真当且仅当对于 \(D\) 中每个元素 \(d\)，将赋值 \(s\) 中 \(x\) 的值改为 \(d\) 后 \(\varphi\) 为真。
- \(\exists x \, \varphi\) 为真当且仅当存在 \(D\) 中某个元素 \(d\)，使得赋值修改后 \(\varphi\) 为真。
模型与可满足性
若公式 \(\varphi\) 在解释 \(\mathcal{I}\) 和所有赋值下均为真，则称 \(\mathcal{I}\) 是 \(\varphi\) 的一个模型（Model）。一组公式 \(S\) 有模型当且仅当存在一个解释同时满足 \(S\) 中所有公式，此时称 \(S\) 可满足（Satisfiable）。若公式在任何解释下均为真，则称其为有效式（Valid）。
等价与替换
逻辑等价式
两个公式 \(\varphi\) 和 \(\psi\) 逻辑等价（\(\varphi \equiv \psi\)）当且仅当它们在任意解释和任意赋值下具有相同真值。常见等价式包括：
- 量词否定：\(\neg \forall x \, \varphi \equiv \exists x \, \neg \varphi\)，\(\neg \exists x \, \varphi \equiv \forall x \, \neg \varphi\)。
- 量词分配：\(\forall x \, (\varphi \land \psi) \equiv \forall x \, \varphi \land \forall x \, \psi\)，\(\exists x \, (\varphi \lor \psi) \equiv \exists x \, \varphi \lor \exists x \, \psi\)。
- 量词与连接词：若 \(x\) 不在 \(\varphi\) 中自由出现，则 \(\forall x \, (\varphi \lor \psi) \equiv \varphi \lor \forall x \, \psi\)（类似公式成立）。
约束变元换名
约束变元换名（Renaming Bound Variable）是指将量词中的变元连同其辖域内所有该变元的约束出现替换为一个新变元，得到逻辑等价的公式。例如 \(\forall x \, P(x)\) 换名为 \(\forall y \, P(y)\)。换名时需避免与新引入的变元冲突，确保不改变自由变元的约束关系。
前束范式
前束范式（Prenex Normal Form）是指所有量词位于公式最前端（无嵌入），且辖域延伸到公式末尾。任何一阶公式均可通过等价变换化为前束范式，步骤包括：消去多余连接词、量词提至前端、换名避免冲突。例如 \(\forall x \, P(x) \land \exists y \, Q(y)\) 可化为 \(\forall x \exists y \, (P(x) \land Q(y))\)。
自然演绎
引入规则与消去规则
自然演绎（Natural Deduction）系统通过引入规则（Introduction Rules）和消去规则（Elimination Rules）刻画逻辑连接词和量词。连接词的经典规则包括：合取引入（\(\land I\)）、合取消去（\(\land E\)）、析取引入（\(\lor I\)）、析取消去（\(\lor E\)）、蕴含引入（\(\rightarrow I\)，即假设推理）、蕴含消去（\(\rightarrow E\)，即分离规则）、否定引入（\(\neg I\)，反证法）和否定消去（\(\neg E\)，双否消去）。
全称量词规则
全称量词引入（\(\forall I\)）：若从任意变元 \(c\)（未在前提中自由出现）推导出 \(\varphi(c)\)，则可推出 \(\forall x \, \varphi(x)\)。
全称量词消去（\(\forall E\)）：由 \(\forall x \, \varphi(x)\) 可推出 \(\varphi(t)\)，其中 \(t\) 是为任意项（需保证代入自由）。
存在量词规则
存在量词引入（\(\exists I\)）：由 \(\varphi(t)\) 可推出 \(\exists x \, \varphi(x)\)。
存在量词消去（\(\exists E\)）：由 \(\exists x \, \varphi(x)\) 和假设 \(\varphi(c)\) 推导出 \(\psi\)（其中 \(c\) 是新常元，不在 \(\psi\) 或已有前提中自由出现），则推出 \(\psi\)。
希尔伯特式公理系统
公理模式
希尔伯特式公理系统（Hilbert-style Axiom System）选取少量公理模式（Axiom Schemas）和推理规则。常见公理模式包括：
- \(\varphi \rightarrow (\psi \rightarrow \varphi)\)
- \((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi))\)
- \((\neg \varphi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \varphi)\)
- \(\forall x \, \varphi \rightarrow \varphi(t)\)（若 \(t\) 可自由代入）
- \(\forall x \, (\varphi \rightarrow \psi) \rightarrow (\forall x \, \varphi \rightarrow \forall x \, \psi)\)
- \(\varphi \rightarrow \forall x \, \varphi\)（若 \(x\) 不在 \(\varphi\) 中自由出现）
推理规则（分离规则与概括规则）
分离规则（Modus Ponens）：由 \(\varphi\) 和 \(\varphi \rightarrow \psi\) 推出 \(\psi\)。
概括规则（Generalization）：由 \(\varphi\) 推出 \(\forall x \, \varphi\)（需满足 \(x\) 不在任何前提中自由出现）。
归结原理
子句集与消去量词
归结原理（Resolution Principle）应用于自动推理，需先将公式化为子句集（Clause Set）。步骤包括：消去蕴含和等价、将否定内移、将量词前提化为斯柯伦范式（Skolemization）以消去存在量词，最后将结果化为合取范式并拆分为子句（子句是文字的析取）。
合一算法与归结法
合一算法（Unification）寻找两个原子公式的最一般代换，使它们变为相同。归结法对两个子句（含有互补文字，如 \(P\) 与 \(\neg P\)）应用合一，生成新子句。反复应用归结规则直至推出空子句（表示矛盾），即证明原公式不可满足。归结原理是自动定理证明的核心方法。
可靠性定理
可靠性定理（Soundness Theorem）宣称：若一阶公式 \(\varphi\) 在某个推理系统（如自然演绎或希尔伯特系统）中可证明，则 \(\varphi\) 是有效的（即在所有解释下为真）。证明通过对推导的长度进行归纳，验证每一条推理规则都保持真值（从前提的真推出结论的真）。可靠性保证了推理系统不会推出假结论。
完备性定理
完备性定理（Completeness Theorem）由哥德尔（Kurt Gödel）于1929年证明：对于一阶逻辑，任何有效公式都是可证明的。更一般地，任何一致的公式集都有模型。完备性确保了推理系统的表达能力足以捕获所有逻辑真理，是数理逻辑的基石之一。
紧致性定理与勒文海姆-斯科伦定理
紧致性定理（Compactness Theorem）：一阶公式集 \(S\) 有模型当且仅当 \(S\) 的任何有限子集有模型。该定理是完备性定理的推论，在模型论中应用广泛。
勒文海姆-斯科伦定理（Löwenheim–Skolem Theorem）：若一阶公式集 \(S\) 有无限模型，则对于任何无限基数 \(\kappa\) 不小于语言的大小，\(S\) 都有大小为 \(\kappa\) 的模型。特别地，一阶逻辑无法区分不同无穷基数的大小，导致“斯科伦悖论”：存在可数模型满足实数理论（尽管实数不可数）。
高阶谓词逻辑
高阶谓词逻辑（Higher-Order Logic）允许量词作用于谓词和函数符号，例如 \(\forall P \, (P(a) \rightarrow P(b))\)。它比一阶逻辑更具表达能力，但失去完备性（哥德尔不完备定理表明足够强的二阶逻辑不是递归可枚举的）。高阶逻辑常用于数学基础和类型论。
谓词逻辑与模态逻辑的结合
模态谓词逻辑（Modal Predicate Logic）将模态算子（\(\Box\) 必然、\(\Diamond\) 可能）与一阶逻辑结合，形成量化模态逻辑。其语义涉及可能世界和对应的个体域，需处理如“跨世界同一性”（Transworld Identity）等哲学难题。该扩展在哲学逻辑和计算机科学（如时态逻辑）中有应用。
一阶逻辑在计算机科学中的应用
自动定理证明
自动定理证明（Automated Theorem Proving）利用归结原理、表方法等算法，在计算机上自动验证一阶公式的有效性。典型系统包括OTTER、Vampire、E等，广泛应用于软件验证、数学定理自动推导等领域。
逻辑程序设计（Prolog）
Prolog（Programming in Logic）是一种基于一阶逻辑子集（Horn子句）的程序设计语言。程序由事实、规则和查询组成，执行通过SLD归结（选择性线性归结）实现。Prolog在人工智能、自然语言处理、专家系统中曾发挥重要作用，其简洁的声明式风格使其成为逻辑程序设计的典范。