一阶谓词逻辑深度指南

文档概述

本文档系统阐述一阶谓词逻辑（First-Order Logic, FOL）的理论基础，涵盖语法构造、语义解释、推理规则及重要元定理，为人工智能中的知识表示与自动推理提供坚实的形式化基础。

关键词速览

关键词	英文术语	核心含义
项	Term	表示对象的语法表达式
原子公式	Atomic Formula	谓词 applied to 项
量词	Quantifier	∀（全称）、∃（存在）
合一	Unification	寻找替换使公式相同
最一般合一	MGU	最通用的合一替换
斯科伦化	Skolemization	消除存在量词
归结原理	Resolution	自动定理证明核心
模型	Model	满足公式的结构
前束范式	Prenex Normal Form	量词前置的标准形式

---

一、一阶逻辑的语法结构

1.1 基本符号表

一阶逻辑的形式语言包含以下基本符号：

$\Sigma =⟨\text{Variables},\text{Constants},\text{FunctionSymbols},\text{PredicateSymbols},\text{LogicalSymbols}⟩$

变量集 $\text{VAR}=\{x,y,z,x_1,y_2,\dots \}$：取值范围为论域中的元素

常量符 $\text{CON}=\{a,b,c,c_1,\dots \}$：表示论域中的特定对象

函数符 $\text{FUN}=\{f,g,h,f_1,\dots \}$：$n$元函数符记作$f/n$

谓词符 $\text{PRED}=\{P,Q,R,P_1,\dots \}$：$n$元谓词符记作$P/n$

逻辑符号：命题联结词 $\neg ,\wedge ,\vee ,\to ,\leftrightarrow$；量词 $\forall ,\exists$；辅助符号 $(,),,$

1.2 项的构造

定义（项，Term）：

1. 变量是项
2. 常量是项
3. 若 $f/n$ 是 $n$ 元函数符，$t_1,t_2,\dots ,t_n$ 是项，则 $f(t_1,t_2,\dots ,t_n)$ 是项
4. 只有有限次应用上述规则产生的表达式才是项

示例：

• $x$（变量）
• $Alice$（常量）
• $father(x)$（一元函数）
• $plus(multiply(x,2),y)$（嵌套函数）

1.3 公式的构造

定义（原子公式，Atomic Formula）：

若 $P/n$ 是 $n$ 元谓词符，$t_1,t_2,\dots ,t_n$ 是项，则 $P(t_1,t_2,\dots ,t_n)$ 是原子公式。

定义（合式公式，Well-Formed Formula）：

1. 原子公式是合式公式
2. 若 $\phi$ 是合式公式，则 $\neg \phi$ 是合式公式
3. 若 $\phi$ 和 $\psi$ 是合式公式，则 $(\phi \wedge \psi )$、$(\phi \vee \psi )$、$(\phi \to \psi )$、$(\phi \leftrightarrow \psi )$ 是合式公式
4. 若 $\phi$ 是合式公式，$x$ 是变量，则 $\forall x\phi$ 和 $\exists x\phi$ 是合式公式
5. 只有有限次应用上述规则产生的表达式才是合式公式

1.4 量词的作用域与自由/绑定变量

定义（自由变量与约束变量）：

• 变量 $x$ 在公式 $\phi$ 中自由，当且仅当它在 $\phi$ 中出现且不在任何 $\forall x$ 或 $\exists x$ 的作用域内
• 变量 $x$ 在公式 $\phi$ 中约束，当且仅当它在 $\forall x$ 或 $\exists x$ 的作用域内

示例：

在公式 $\forall x(P(x)\to Q(x,y))$ 中：

• $x$ 是约束变量
• $y$ 是自由变量

---

二、一阶逻辑的语义理论

2.1 结构与解释

定义（结构，Structure）：

一阶结构 $\mathcal{M}$ 由以下组成：

$\mathcal{M}=⟨\text{Dom}(\mathcal{M}),\text{Interp}⟩$

其中：

• $\text{Dom}(\mathcal{M})$ 是论域（非空集合）
• $\text{Interp}$ 是解释函数，将：
  • 常量映射到论域中的元素：$c^{\mathcal{M}}\in \text{Dom}(\mathcal{M})$
  • $n$ 元函数映射到论域上的 $n$ 元函数：$f^{\mathcal{M}}:\text{Dom}(\mathcal{M}{)}^n\to \text{Dom}(\mathcal{M})$
  • $n$ 元谓词映射到论域上的 $n$ 元关系：$P^{\mathcal{M}}\subseteq \text{Dom}(\mathcal{M}{)}^n$

2.2 项的解释

给定结构 $\mathcal{M}$ 和变量赋值 $\sigma :\text{VAR}\to \text{Dom}(\mathcal{M})$，项的解释定义为：

• $\sigma (x)=\sigma (x)$（变量）
• $\sigma (c)=c^{\mathcal{M}}$（常量）
• $\sigma (f(t_1,\dots ,t_n))=f^{\mathcal{M}}(\sigma (t_1),\dots ,\sigma (t_n))$（函数）

2.3 公式的真值语义

设 $\mathcal{M}$ 为结构，$\sigma$ 为变量赋值：

原子公式：$\mathcal{M}{\models }_{\sigma }P(t_1,\dots ,t_n)$ 当且仅当 $(\sigma (t_1),\dots ,\sigma (t_n))\in P^{\mathcal{M}}$

布尔联结词：

• $\mathcal{M}{\models }_{\sigma }\neg \phi$ 当且仅当 $\mathcal{M}/{\models }_{\sigma }\phi$
• $\mathcal{M}{\models }_{\sigma }\phi \wedge \psi$ 当且仅当 $\mathcal{M}{\models }_{\sigma }\phi$ 且 $\mathcal{M}{\models }_{\sigma }\psi$
• $\mathcal{M}{\models }_{\sigma }\phi \vee \psi$ 当且仅当 $\mathcal{M}{\models }_{\sigma }\phi$ 或 $\mathcal{M}{\models }_{\sigma }\psi$
• $\mathcal{M}{\models }_{\sigma }\phi \to \psi$ 当且仅当 $\mathcal{M}/{\models }_{\sigma }\phi$ 或 $\mathcal{M}{\models }_{\sigma }\psi$

量词：

• $\mathcal{M}{\models }_{\sigma }\forall x\phi$ 当且仅当对所有 $d\in \text{Dom}(\mathcal{M})$，$\mathcal{M}{\models }_{\sigma [x/d]}\phi$
• $\mathcal{M}{\models }_{\sigma }\exists x\phi$ 当且仅当存在 $d\in \text{Dom}(\mathcal{M})$，使得 $\mathcal{M}{\models }_{\sigma [x/d]}\phi$

2.4 模型与可满足性

定义（模型）：

若 $\mathcal{M}{\models }_{\sigma }\phi$ 对所有赋值 $\sigma$ 成立，则称 $\mathcal{M}$ 是 $\phi$ 的模型，记作 $\mathcal{M}\models \phi$。

定义（有效性）：

公式 $\phi$ 是有效的（记作 $\models \phi$），当且仅当每个结构都是其模型。

定义（可满足性）：

公式集 $\Gamma$ 是可满足的，当且仅当存在结构 $\mathcal{M}$ 和赋值 $\sigma$ 使得对所有 $\gamma \in \Gamma$，$\mathcal{M}{\models }_{\sigma }\gamma$。

---

三、推理规则与证明系统

3.1 自然演绎系统

自然演绎是一种接近人类推理风格的证明系统，包含以下核心规则：

命题层规则：

规则名称	符号表示	描述
肯定前件	MP	从 $\phi \to \psi$ 和 $\phi$ 推出 $\psi$
否定后件	MT	从 $\phi \to \psi$ 和 $\neg \psi$ 推出 $\neg \phi$
合取引入	$\wedge$I	从 $\phi$ 和 $\psi$ 推出 $\phi \wedge \psi$
合取消去	$\wedge$E	从 $\phi \wedge \psi$ 推出 $\phi$（或 $\psi$）
析取引入	$\vee$I	从 $\phi$ 推出 $\phi \vee \psi$
双重否定消去	DNE	从 $\neg \neg \phi$ 推出 $\phi$

量词规则：

规则名称	符号表示	描述
全称量词消去	∀E	从 $\forall x\phi$ 推出 $\phi [t/x]$（$t$ 对 $x$ 可代入）
全称量词引入	∀I	从 $\phi$ 推出 $\forall x\phi$（$x$ 不在假设中自由）
存在量词引入	∃I	从 $\phi [t/x]$ 推出 $\exists x\phi$
存在量词消去	∃E	从 $\exists x\phi$ 和 $\phi \to \psi$ 推出 $\psi$（$x$ 不在 $\psi$ 中自由）

3.2 合一算法与最一般合一

定义（合一，Unification）：

给定两个项或原子公式，寻找一个替换 $\theta$ 使得应用 $\theta$ 后两者相同。

定义（最一般合一，MGU）：

合一子 $\sigma$ 是最一般的，当且仅当对任何其他合一子 $\theta$，存在替换 $\tau$ 使得 $\theta =\tau \circ \sigma$。

合一算法（Robinson 1965）：

UNIFY(θ, s, t):
    θ <- 应用当前替换到 s, t
    if s = t: return θ
    if s = f(s1,...,sn) and t = f(t1,...,tn):
        for i = 1 to n:
            θ <- UNIFY(θ, si, ti)
        return θ
    if s = x and t is not containing x:
        return compose(x -> t, θ)
    if t = x and s is not containing x:
        return compose(x -> s, θ)
    return failure

3.3 前束范式与斯科伦化

定义（前束范式）：

公式 $\phi$ 是前束范式，当且仅当它形如 $Q_1{x}_1{Q}_2{x}_2\dots Q_n{x}_n\cdot \psi$，其中 $Q_i\in \{\forall ,\exists \}$，$\psi$ 不含量词。

定理（前束化）：

任意一阶公式都可等价地转化为前束范式。

定义（斯科伦化）：

将存在量词用斯科伦函数替换，消去所有存在量词的过程。设 $\exists y\forall x\phi (x,y)$ 转化为 $\forall x\phi (x,f(x))$，其中 $f$ 是新引入的斯科伦函数。

斯科伦化的影响

斯科伦化后的公式与原公式在可满足性上等价，但有效性不等价。需注意反例 Skolemization 可能丢失。

---

四、哥德尔定理与一阶逻辑的局限性

4.1 哥德尔完备性定理

定理（哥德尔完备性定理，1930）：

一阶逻辑的自然演绎系统是完备的，即： $\Gamma \models \phi ⟺\Gamma ⊢\phi$

这意味着：如果 $\phi$ 是 $\Gamma$ 的语义后承，则存在从 $\Gamma$ 到 $\phi$ 的形式证明。

4.2 紧致性定理

定理（紧致性定理）：

公式集 $\Gamma$ 是可满足的，当且仅当 $\Gamma$ 的每个有限子集是可满足的。

推论应用：

• 从 $\Gamma \models \phi$ 可推出存在有限子集 $\Delta \subseteq \Gamma$ 使得 $\Delta \models \phi$
• 用于证明某些理论没有有限模型

4.3 Lowenheim-Skolem 定理

定理（下Lowenheim-Skolem）：

若一阶理论有无穷模型，则它在每个无穷基数上都有模型。

推论（Skolem悖论）：

一阶理论可以有可数模型，即使其实质上描述的是不可数结构（如实数）。

4.4 一阶逻辑的表达力局限

一阶逻辑存在以下局限：

1. 不能表达良基性：无法在二阶逻辑外形式化”没有无穷下降链”
2. 不能完全公理化算术：Peano算术的真算术不可公理化
3. 直觉主义拒绝排中律：$\phi \vee \neg \phi$ 不总是可证明
4. 模型论复杂性：紧致性等元定理的证明依赖集合论工具

---

五、与其他逻辑系统的关系

5.1 与命题逻辑的关系

一阶逻辑是命题逻辑的严格扩展：

• 命题逻辑是一阶逻辑中不含量词和谓词的子语言
• 一阶逻辑的判定问题比命题逻辑更复杂（命题逻辑可判定，一阶逻辑不可判定）

5.2 与高阶逻辑的关系

二阶逻辑允许量化谓词和函数： $\forall P(P(x)\to P(x))$

高阶逻辑表达力更强，但失去可判定性和完备性。

5.3 与模态逻辑的关系

一阶模态逻辑在一阶逻辑基础上增加模态算子 $\square ,◊$，应用于可能世界语义学。详见 模态逻辑详解。

---

六、在人工智能中的应用

6.1 知识表示

一阶逻辑是知识表示与推理的重要工具：

• 描述状态：$On(BlockA,BlockB)$ 表示积木A在积木B上
• 描述动作：$\forall x\forall y(Holding(x)\to \neg Holding(y))$
• 描述约束：使用全称量词表达物理定律

6.2 自动定理证明

归结原理（Resolution）是一阶逻辑自动定理证明的核心方法：

1. 将公式转化为子句形式
2. 应用归结规则进行推理
3. 通过反证法证明目标定理

详见 自动定理证明。

6.3 逻辑编程

Prolog 语言基于一阶逻辑的子集（霍恩子句），实现自动回溯和查询。

---

参考文献

1. Enderton, H. B. (2001). A Mathematical Introduction to Logic (2nd ed.). Academic Press.
2. Mendelson, E. (2015). Introduction to Mathematical Logic (6th ed.). Chapman and Hall/CRC.
3. Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1), 23-41.
4. 郝兆宽, 杨睿之. (2014). 《数理逻辑：证明及其限度》. 复旦大学出版社.
5. 王浩. (2019). 《一阶逻辑与自动定理证明》. 清华大学出版社.

---

相关文档

• 模态逻辑详解 — 扩展到模态算子的一阶逻辑
• 自动定理证明 — 一阶逻辑的自动证明方法
• 非经典逻辑 — 直觉主义、模糊等非经典逻辑
• 知识表示与推理 — 逻辑在知识工程中的应用