人工智能知识库

一阶谓词逻辑深度指南

55分钟阅读

一阶谓词逻辑深度指南

文档概述

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

关键词速览

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

一、一阶逻辑入门：从命题逻辑到一阶逻辑的飞跃

1.1 为什么需要一阶逻辑？

学一阶逻辑之前，你可能已经学过命题逻辑。命题逻辑处理的是整个命题，比如”今天下雨”、“小明喜欢编程”这样的完整陈述。命题逻辑能够处理”与”、“或”、“非”这些基本联结词，也能做简单的推理。

但命题逻辑有个根本性的缺陷：它没法表达内部结构。

举个例子。命题逻辑可以表达”苏格拉底是人”和”所有人是会死的”这两个命题，但它没办法表达”所有人是会死的”这个一般性陈述到底在说什么。它只能把”所有人是会死的”当作一个原子命题，而无法进一步拆解”人”和”会死的”这两个概念之间的关系。

这就好比编程语言只有布尔类型，没有整型、字符串、数组——你当然能用true和false表达一些东西，但稍微复杂点的应用就抓瞎了。

一阶逻辑的出现，就是为了解决这个问题。它允许我们谈论对象（人、桌子、数字）、对象的属性（是人、会死、红色）、以及对象之间的关系（比…大、喜欢、在…上面）。这样我们就能精确地表达”苏格拉底是人，并且所有人是会死的，所以苏格拉底是会死的”这样的推理链条。

1.2 一阶逻辑到底是个什么东西？

一阶逻辑，也叫一阶谓词逻辑，是一种用来精确表达 statements about objects and their relationships 的形式语言。

“一阶”这个词可能会让初学者困惑。说白了，一阶逻辑只允许我们量化（quantify）对象。也就是说，你可以说什么”存在一个人…”、“所有人都…”这样的话。但你不能说”所有性质都…”或者”存在一个规则…”——后者是对性质或规则本身进行量化，这属于二阶逻辑的范畴。

举个例子感受一下区别：

  • 一阶逻辑可以说：∃x (Human(x) ∧ Mortal(x)) —— 存在一个人，这个人是会死的
  • 二阶逻辑可以说：∃P P(Socrates) —— 存在一个性质P，苏格拉底具有这个性质

二阶逻辑的表达力更强，但代价是失去了很多好用的性质（比如完备性）。对于绝大多数AI应用来说，一阶逻辑已经足够了，这也是为什么它是AI知识表示的基石。

二、谓词与量词：∀和∃到底在说啥？

2.1 谓词：给对象贴标签

谓词（Predicate）本质上就是给对象附加属性或者描述对象之间的关系。

零元谓词其实就是命题逻辑里的原子命题，比如Rain()表示”下雨”这个命题成立。它不涉及任何对象，纯粹是个事实陈述。

一元谓词描述对象的单个属性。比如Human(x)表示x是人，Red(y)表示y是红色的，Prime(n)表示n是质数。这些就像给对象贴标签。

多元谓词描述对象之间的关系。比如Loves(x, y)表示x爱y，Bigger(x, y)表示x比y大，On(a, b)表示积木a在积木b上面。

这里有个地方容易搞错：谓词符号本身不等于属性或关系，它只是个占位符。真正决定”是红色”还是”是蓝色”的，是我们对谓词的解释（interpretation）。同一个谓词符号，在不同语境下可以解释成完全不同的意思。这是一阶逻辑语义学的核心——符号和它代表的东西是分开的。

2.2 量词：全称与存在

量词是理解一阶逻辑最关键的地方。中文里说”所有的”、“每一个”、“存在”、“有些”——这些都是量词在自然语言里的体现。

全称量词 ∀ 读作”对所有”、“对每一个”。∀x P(x)的意思是：对于论域里的每一个对象x，P(x)都为真。比如在人类世界里，∀x (Human(x) → Mortal(x))说的是”对于所有x，如果x是人，那么x是会死的”。

注意这里用的是蕴含 → 而不是合取 ∧。差别很大。∀x (Human(x) ∧ Mortal(x))要求世界上每一个东西既是人又会死，这显然太严格了。而∀x (Human(x) → Mortal(x))只要求：如果某样东西是人，那它就必须会死——不要求世界上只有人。这才是我们真正想表达的意思。

存在量词 ∃ 读作”存在”、“有些”、“至少有一个”。∃x P(x)的意思是：论域里至少有一个对象x使得P(x)为真。

比如∃x (Human(x) ∧ Likes(x, IceCream))说的是”有一个人喜欢冰淇淋”。注意这里用的是合取，不是蕴含——我们要找的是这么一个人，它同时满足”是人”和”喜欢冰淇淋”这两个条件。

2.3 量词对偶：德·摩根定律在一阶逻辑里的推广

命题逻辑里有个德·摩根定律：¬(P ∧ Q) 等价于 ¬P ∨ ¬Q。

这个定律在一阶逻辑里推广成：

¬∀x P(x)  等价于  ∃x ¬P(x)   （不是所有人都...)
¬∃x P(x)  等价于  ∀x ¬P(x)   （没有人的...)

反过来：

¬∀x ¬P(x)  等价于  ∃x P(x)    （不是所有人都不...）
¬∃x ¬P(x)  等价于  ∀x P(x)    （没有...是不...的）

理解这个对偶性特别重要。做推理或者化简公式的时候，经常需要在∀和∃之间来回切换，同时把否定词往里推或者往外拉。

三、变量与常量：逻辑中的”代词”是什么？

3.1 常量：固定的指代

常量（Constant）就像自然语言里的专有名词。Alice、Beijing、3、π这些都是常量——它们指代论域里某个固定的、具体的东西。

在一阶逻辑里，我们用小写字母开头表示常量：a、b、alice、number3都行。常量本身没有含义，它的含义来自我们对它的解释。比如在某个论域里，我们可以把常量alice解释为”Alice Zhang”，但在另一个论域里可能解释成别的什么。

3.2 变量：灵活的占位

变量（Variable）就像自然语言里的代词或者未知数。当我说”某个人喜欢冰淇淋”，这里的”某个人”就是个变量——它指代的对象还没有确定，需要根据上下文来确定。

变量用小写字母x、y、z等表示（或者加下标如x1、y2）。变量的值取决于变量赋值（variable assignment），这就像是给代词找到它指代的对象。

3.3 函数：复合对象的表示

函数（Function）在一阶逻辑里是个容易被忽视但超级有用的工具。

比如要表达”John的父亲”这个概念，用常量john不够，因为我们需要引用一个具体的值。引入函数father(john)就可以——它表示John的父亲这个对象。

函数可以嵌套：father(father(john))表示John的祖父。plus(multiply(x, 2), y)表示2x + y这样一个复杂表达式。

有个重要的约束：函数必须返回论域里的元素。这意味着你不能把一个不存在的对象作为函数值。比如mother(Socrates)必须解释为Socrates的母亲——如果Socrates在当前论域里，这个函数就是良定义的；如果我们讨论的古希腊人物里没有记录Socrates的母亲，这个函数值可能就不存在。这种情况怎么处理，一阶逻辑本身没有内置解决方案，需要通过添加额外的约束条件来处理。

3.4 项：对象的无歧义表达

项（Term）是一阶逻辑里表示对象的语法结构。定义很递归也很简洁：

  • 变量是项
  • 常量是项
  • 如果t1, ..., tn是项，f/n是n元函数符，那么f(t1, ..., tn)也是项

说白了，项就是用常量、变量和函数任意组合出来的表达式，它的值永远是论域里的某个对象。

四、一阶逻辑语法：如何正确地写逻辑表达式

4.1 原子公式：最基础的陈述

原子公式（Atomic Formula）由一个谓词符号后面跟上若干项组成：

P(t1, t2, ..., tn)

这里P是n元谓词，t1, ..., tn都是项。原子公式就是最基础的陈述，比如Loves(alice, bob)表示”Alice爱Bob”。

原子公式没有内部结构，不能用联结词拆开——就像原子是物质的最小单位一样。

4.2 合式公式：递归构造的完整陈述

合式公式（Well-Formed Formula, WFF），顾名思义就是符合语法规则的公式。一阶逻辑的公式构造遵循一套递归规则：

基本规则：

  1. 所有原子公式都是合式公式
  2. 如果φ是合式公式，那么¬φ也是
  3. 如果φ和ψ是合式公式，那么(φ ∧ ψ)、(φ ∨ ψ)、(φ → ψ)、(φ ↔ ψ)也都是
  4. 如果φ是合式公式，x是变量，那么∀x φ和∃x φ也是

括号省略规则（为了可读性）：

  • 最外层括号可以省略
  • 联结词的优先级通常是：¬ > ∧/∨ > → > ↔
  • 但写复杂公式时，建议还是把括号加上，避免歧义

例子：把”如果所有学生都通过了考试，那么小明通过了考试或者存在学生没通过考试”翻译成一阶逻辑：

(∀x (Student(x) → Passed(x, exam))) → (Passed(Xiaoming, exam) ∨ ∃y (Student(y) ∧ ¬Passed(y, exam)))

4.3 量词的作用域与绑定

量词后面紧跟的部分就是量词的作用域（scope）。比如在∀x (P(x) → Q(x, y))里，量词∀x的作用域是P(x) → Q(x, y)。

变量被量词”抓住”了，就是被绑定的（bound）。变量不被任何量词约束，就是自由的（free）。

为什么要区分这个？因为自由的变量才是真正”未确定”的部分。一个公式如果含有自由变量，它的真值取决于自由变量的取值。比如P(x)——x是自由的还是被绑定的，表达的意思完全不同。

  • P(x)：关于x的某个陈述，x还没确定
  • ∀x P(x)：对所有x，P(x)都成立
  • ∃x P(x)：存在某个x使得P(x)成立

一个句子（sentence）是不含自由变量的公式——所有变量都被绑定了。这样的公式才有确定的真值，不依赖于”还有什么变量没确定”。

4.4 自由/约束变量的判断技巧

给你一个公式，怎么快速判断哪些变量是自由的？

诀窍是：从里往外看，遇到量词就”抓住”它管辖范围内的同名变量。

看个复杂例子：

∀x (P(x, y) → ∃y Q(x, y)) → ∃z R(y, z)
  • 最左边的∀x绑定了第一个x
  • 里面的∃y绑定了第二个y（在Q(x,y)里）
  • 最后的∃z绑定了z
  • 第一个y（在P(x,y)里）是自由的——它没有被∃y绑定，因为∃y只管Q(x,y)里的那个y
  • 第二个y（在R(y,z)里）也是自由的——因为∃y的作用域不包括这里

所以这个公式的自由变量是：{y}。

五、一阶逻辑语义：什么叫”满足”？

5.1 结构：逻辑世界里的”模型”

一阶逻辑的语义回答的是：给定一个公式，它到底是什么意思？什么时候为真？

这需要引入结构（Structure）这个概念。结构就像一个”小宇宙”，包含：

  • 论域（Domain）：结构里”存在”的所有对象的集合。比如要讨论人类社会，论域就是所有人类；要讨论自然数，论域就是{0, 1, 2, 3, …}。

  • 解释（Interpretation）：把符号映射到论域里的具体东西。常量解释成具体的对象，函数解释成具体的运算或关系，谓词解释成具体的关系或属性。

举个例子。论域是所有人类，结构M包含：

  • 常量alice解释为Alice这个人
  • 谓词Human(x)解释为”x是人类”这个属性
  • 谓词Loves(x, y)解释为”x爱y”这个关系

注意：一阶逻辑的语义是外延性的——我们不关心符号叫什么名字，只关心它解释成什么。两个结构只要”本质上一样”（同构），对公式的真值就是等价的。

5.2 赋值：给变量找具体对象

结构只告诉我们常量、函数、谓词是什么意思，但变量呢？变量本身还没指代任何具体对象。

变量赋值（Variable Assignment）就是给变量分配论域里的具体值。打个赋值σ，σ(x) = alice的意思是：在这个赋值下，变量x指代的对象是alice。

重要的是：给定一个结构，我们可以定义无数种赋值，因为变量的取值可以自由选择。公式的真值可能依赖于赋值，也可能不依赖。

5.3 真值定义：递归地判断公式是真是假

有了结构和赋值，我们就能递归地定义什么是一个公式为真。

原子公式：M ⊧σ P(t1, ..., tn) 当且仅当 (σ(t1), …, σ(tn)) ∈ P^M。换句话说，谓词P在解释下成立，当且仅当这些项解释后的对象满足这个关系。

联结词：和命题逻辑一样。

  • M ⊧σ ¬φ 当且仅当 M ⊭σ φ
  • M ⊧σ (φ ∧ ψ) 当且仅当 M ⊧σ φ 且 M ⊧σ ψ
  • M ⊧σ (φ ∨ ψ) 当且仅当 M ⊧σ φ 或 M ⊧σ ψ（或两者都）
  • M ⊧σ (φ → ψ) 当且仅当 M ⊭σ φ 或 M ⊧σ ψ

量词：这是关键部分。

  • M ⊧σ ∀x φ 当且仅当：对论域里所有对象d，M ⊧σ[x/d] φ都成立。这里σ[x/d]表示在σ的基础上把x的值改成d。
  • M ⊧σ ∃x φ 当且仅当：论域里存在某个对象d，使得M ⊧σ[x/d] φ成立。

这个递归定义完整地规定了一阶逻辑的语义学。

5.4 模型、可满足、有效性

基于上面的语义，我们定义几个核心概念：

模型（Model）：如果M ⊧ φ（对所有赋值σ都成立），就说M是φ的模型——M使得φ为真。

可满足（Satisfiable）：如果存在某个结构M和某个赋值σ，使得M ⊧σ Γ（Γ是一个公式集合），就说Γ是可满足的——至少在一个世界里，Γ里所有公式都能同时成立。

有效性（Valid）：如果公式φ在所有结构里都为真，就说φ是有效的（记作⊧ φ）。有效的公式也叫重言式——它们在任何可能的世界里都为真，比如P(x) ∨ ¬P(x)。

可满足性和有效性的关系：φ是有效的当且仅当¬φ是不可满足的。这个对偶关系在自动定理证明里特别有用——要证明φ成立，只需证明¬φ不可能成立（反证法）。

六、逻辑等价：德·摩根定律、分配律——那些恒成立的变形

6.1 命题层级的等价

在一阶逻辑里，命题逻辑的等价律仍然成立：

德·摩根定律：

  • ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
  • ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ

双重否定：

  • ¬¬φ ≡ φ

幂等律：

  • φ ∧ φ ≡ φ
  • φ ∨ φ ≡ φ

吸收律：

  • φ ∧ (φ ∨ ψ) ≡ φ
  • φ ∨ (φ ∧ ψ) ≡ φ

分配律：

  • φ ∧ (ψ ∨ χ) ≡ (φ ∧ ψ) ∨ (φ ∧ χ)
  • φ ∨ (ψ ∧ χ) ≡ (φ ∨ ψ) ∧ (φ ∨ χ)

蕴含的等价变形：

  • φ → ψ ≡ ¬φ ∨ ψ
  • φ → ψ ≡ ¬ψ → ¬φ（逆否）
  • φ → (ψ → χ) ≡ (φ ∧ ψ) → χ

6.2 量词相关的等价

量词的德·摩根定律（前面提过）：

  • ¬∀x φ ≡ ∃x ¬φ
  • ¬∃x φ ≡ ∀x ¬φ

量词的分配律：

  • ∀x (φ ∧ ψ) ≡ ∀x φ ∧ ∀x ψ
  • ∃x (φ ∨ ψ) ≡ ∃x φ ∨ ∃x ψ

注意：∀x (φ ∨ ψ) 不等于 ∀x φ ∨ ∀x ψ——左边只要求对每个x，要么φ成立要么ψ成立，不要求同一个φ对所有x都成立。类似地，∃x (φ ∧ ψ) 不等于 ∃x φ ∧ ∃x ψ。

量词的作用域交换：

  • ∀x ∀y φ ≡ ∀y ∀x φ
  • ∃x ∃y φ ≡ ∃y ∃x φ

注意：∀x ∃y φ 不等于 ∃y ∀x φ——这两个的意思完全不同。前者说对每个x都能找到某个y（y可以依赖于x），后者说存在一个固定的y使得对所有x都成立。这在数学里经常被搞混，要特别注意。

6.3 量词的提升

有时候我们想把量词”往外提”或者”往里推”。

量词前移（需要小心变量的冲突）：

  • ∀x φ ∧ ψ ≡ ∀x (φ ∧ ψ) （如果x不在ψ里自由出现）
  • ∃x φ ∧ ψ ≡ ∃x (φ ∧ ψ) （如果x不在ψ里自由出现）

如果变量在另一边自由出现，就不能直接提，需要用其他技巧（比如引入约束变量或者改名）。

七、自然语言到一阶逻辑的转换：把”所有人都爱某个人”翻译成逻辑

7.1 翻译的基本原则

把自然语言翻译成一阶逻辑，需要先确定论域是什么，然后逐层拆解。

比如”所有学生都通过了考试”：

  • 论域是所有人
  • 符号：Student(x)表示x是学生，Passed(x)表示x通过了考试
  • 翻译：∀x (Student(x) → Passed(x))

注意这里的蕴含→而不是合取∧。用合取的话，意思是”所有东西都既是学生又通过了考试”——这显然不是原意。

7.2 各种句式的翻译技巧

全称陈述：“每个X都是Y”

∀x (X(x) → Y(x))

存在陈述：“有些X是Y”

∃x (X(x) ∧ Y(x))

否定全称：“不是所有X都是Y” = “存在X不是Y”

¬∀x (X(x) → Y(x))  ≡  ∃x (X(x) ∧ ¬Y(x))

否定存在：“没有X是Y” = “所有X都不是Y”

¬∃x (X(x) ∧ Y(x))  ≡  ∀x (X(x) → ¬Y(x))

双重否定：“没有X不是Y” = “所有X都是Y”

¬∃x (X(x) ∧ ¬Y(x))  ≡  ∀x (X(x) → Y(x))

7.3 复杂句子的翻译示例

例子1：“所有老师都喜欢有些聪明的学生”

  • 符号：Teacher(x)、Student(x)、Intelligent(x)、Likes(x, y)
  • 翻译：∀x (Teacher(x) → ∃y (Student(y) ∧ Intelligent(y) ∧ Likes(x, y)))

例子2：“存在一个数，比所有其他数都大”（最大值）

  • 论域：所有自然数
  • 符号：Greater(x, y)
  • 翻译：∃x ∀y (x ≠ y → Greater(x, y))

例子3：“每个人都爱自己”

  • 翻译：∀x Loves(x, x)

例子4：“有些人不喜欢任何人”

  • 翻译：∃x (Human(x) ∧ ∀y (Human(y) → ¬Likes(x, y)))

例子5：“没有老师不喜欢聪明的学生”

  • 先翻译”老师不喜欢聪明的学生”：Teacher(x) ∧ Student(y) ∧ Intelligent(y) ∧ ¬Likes(x, y)
  • 整体否定：¬∃x (Teacher(x) ∧ ∃y (Student(y) ∧ Intelligent(y) ∧ ¬Likes(x, y)))
  • 或者：∀x (Teacher(x) → ∀y (Student(y) ∧ Intelligent(y) → Likes(x, y)))

八、前向链与后向链推理：逻辑推断的两条路

8.1 什么是逻辑推理？

逻辑推理就是从已知知识推出新知识。给定一组前提（公式集Γ），我们想知道某个结论φ能不能被推导出来。

这涉及到两个层面的”推出”：

  • 语义的推出（Γ ⊧ φ）：从语义上说，Γ的所有模型都是φ的模型——φ在Γ的所有可能世界里都为真
  • 语法的推出（Γ ⊢ φ）：从语法上说，存在一个从Γ到φ的形式证明——一系列推理步骤

哥德尔完备性定理告诉我们，在一阶逻辑里，语义推出和语法推出是等价的：Γ ⊧ φ 当且仅当 Γ ⊢ φ。这意味着我们可以安心地用形式证明系统来研究语义关系。

8.2 前向链：从事实到结论

前向链推理（Forward Chaining）是从已知事实出发，逐步应用推理规则产生新事实，直到达到目标或者无法继续。

这就像医生看病：已知病人发烧、咳嗽、有痰，医生根据医学知识（规则）推断可能是肺炎，然后进一步检查验证。

在逻辑里，前向链主要用的是肯定前件（Modus Ponens）：

如果 φ → ψ 和 φ 都已知，则可以推出 ψ

比如：

  • 规则1：∀x (Human(x) → Mortal(x))
  • 事实：Human(Socrates)
  • 前向推理：应用∀消去和MP，得到 Mortal(Socrates)

前向链的优点是数据驱动，从已知出发自然地探索；缺点是可能产生大量无关的事实，效率不高。

8.3 后向链：从目标回溯

后向链推理（Backward Chaining）是从目标结论出发，反向寻找支持它的证据。

这就像侦探破案：假设嫌疑人有罪（目标），然后寻找能证明犯罪动机、机会、能力的证据。

后向链经常用归结原理（Resolution）实现。归结原理的核心思想是反证法：要证明Γ ⊢ φ，只需证明Γ ∪ {¬φ}是不可满足的（矛盾）。

比如要证明”Socrates是会死的”：

  1. 把结论否定：¬Mortal(Socrates)
  2. 把前提和否定结论都转化为子句形式
  3. 归结产生新子句
  4. 如果归结出空子句（矛盾），就证明成功

8.4 哪种方式更好？

前向链和后向链各有适用场景：

特征前向链后向链
方向从前提到结论从目标到前提
适用场景数据丰富，结论未知目标明确，需验证
控制策略数据驱动目标驱动
优点自动发现新知识不探索无关分支
缺点可能产生大量无用结论可能重复探索

在专家系统里，通常后向链更常用，因为用户的查询往往很明确。但在自动定理证明里，前向链的变体（resolution-based）几乎是标准方法。

九、合一与统一算法：逻辑推理的核心工具

9.1 为什么需要合一？

在推理过程中，经常需要比较两个表达式是否”相同”，或者找到让它们”相同”的替换。

比如，规则是Parent(x, y) → Ancestor(x, y)，事实是Parent(John, Mary)。要把规则应用到事实上，需要把规则里的x替换成John、y替换成Mary。这个替换过程就是合一。

另一个例子。已知两个原子公式P(x, f(y))和P(g(z), f(w))，它们能合一吗？是的——只要让x = g(z)并且y = w。应用这个替换后，两个公式都变成P(g(z), f(w))，完全相同。

9.2 替换（Substitution）的概念

替换是从变量到项的映射：θ = {x1/t1, x2/t2, ..., xn/tn}

应用替换θ到表达式E上（记作Eθ），就是把E里所有xi都替换成ti。

比如：θ = {x/a, y/f(z)}，那么P(x, y)θ = P(a, f(z))

合成替换：先应用θ1再应用θ2，记作θ1θ2。比如θ1 = {x/y}，θ2 = {y/z}，则θ1θ2 = {x/z, y/z}。

9.3 合一算法

合一的问题：给定两个表达式s和t，找到一个替换θ使得sθ = tθ。

最一般合一（Most General Unifier, MGU）：如果存在合一θ，那么一定存在一个MGU σ，使得任何其他合一θ都可以写成θ = τ ∘ σ的形式。简单说，MGU是最”通用”的合一——它做的替换最少，保留了最大的灵活性。

Robinson合一算法（1965年）的基本思路：

function UNIFY(s, t, θ):
    θ <- 应用当前替换到s和t
    if s = t: return θ
    if s是变量: return {s/t} ∘ θ
    if t是变量: return {t/s} ∘ θ
    if s = f(s1,...,sn) and t = f(t1,...,tn):
        for i = 1 to n:
            θ <- UNIFY(si, ti, θ)
        return θ
    return failure  # 函子不同，无法合一

关键是：

  1. 如果两个表达式相同，不需要替换
  2. 如果一个是未被约束的变量，另一个是任意项，约束变量为那个项
  3. 如果函子（谓词符号或函数符号）不同，无法合一
  4. 递归处理复合表达式的每个子项

9.4 合一失败的例子

不是所有表达式都能合一：

  • P(x) 和 P(x, y) —— 函子P的元数不同，无法合一
  • P(x, x) 和 P(y, f(y)) —— 会导致x = f(x)，x出现在自己的定义里（occurs check），违反良基性
  • P(f(x)) 和 P(y) —— 可以合一，得到{x/f(y)}或者{y/f(x)}，两者都是MGU

Occurs Check（出现检查）是合一算法里必须做的一步：检查是否会导致x = f(x)这种循环定义。如果不检查，算法可能返回”合一成功”但实际上产生了不合理的替换。

十、一阶逻辑在AI中的应用：知识图谱、本体论、问答系统

10.1 知识图谱：把世界表示成图

知识图谱（Knowledge Graph）是这几年特别火的技术，Google、百度、阿里都在搞。简单说，它把知识表示成”实体-关系-实体”的三元组。

一阶逻辑和知识图谱有什么关系？实际上，知识图谱本质上是一阶逻辑知识库的可视化。

每个三元组Head Relation Tail可以翻译成一阶逻辑的原子公式：Relation(Head, Tail)

比如：

  • LocatedIn(Beijing, China) —— 北京位于中国
  • WorksAt(Elon_Musk, Tesla) —— Elon Musk在特斯拉工作
  • HasWife(Elon_Musk, Talulah_Riley) —— Elon Musk的妻子是Talulah Riley

更复杂的知识推理就用到一阶逻辑了。比如要推理”Elon Musk的妻子的国籍是什么”：

  1. HasWife(Elon_Musk, Talulah_Riley)
  2. Nationality(Talulah_Riley, Australian)（事实）
  3. 规则：∀x ∀y ∀z (HasWife(x, y) ∧ Nationality(y, z) → SpouseNationality(x, z))
  4. 应用规则得到：SpouseNationality(Elon_Musk, Australian)

10.2 本体论：定义概念和关系

本体论（Ontology）在AI里指的是对某个领域的概念体系进行形式化定义。

比如医学本体需要定义：什么是疾病、什么是症状、疾病和症状有什么关系、什么治疗方案适用于什么疾病…

OWL（Web Ontology Language）是目前最常用的本体描述语言，它本质上就是一阶逻辑的可判定子集。OWL的设计者们做了个聪明的选择：限制一阶逻辑的表达力，换取可判定性——这意味着我们可以写程序来自动检查本体是否一致、两个概念是否有包含关系。

10.3 问答系统：让机器理解并回答问题

现代问答系统（QA System）的背后，经常有一阶逻辑的身影。

简单问答：问”北京的首都是什么？“——系统从知识库查到CapitalOf(Beijing, China)，回答”中国”。这里不需要复杂推理。

复杂推理问答：问”特斯拉CEO的妻子的国籍是什么？”

  1. 先找到CEO：CEO(Tesla, Elon_Musk)
  2. 再找妻子：HasWife(Elon_Musk, Talulah_Riley)
  3. 最后找国籍：Nationality(Talulah_Riley, Australian)

这个过程涉及多步链式推理，本质上是把问题分解成多个原子查询，然后用一阶逻辑推理规则连接起来。

自然语言问题到逻辑形式的转换是个难题。用户的问法千变万化，系统需要理解”什么”指代什么、“谁”是主语、“的”表示什么关系。这涉及到语义解析（Semantic Parsing），把自然语言映射成一阶逻辑公式，然后查询推理。

10.4 一阶逻辑 vs 其他知识表示

一阶逻辑的优点：

  • 表达力强，能描述复杂的对象和关系
  • 有成熟的推理理论（完备性、紧致性等）
  • 可以做自动定理证明

一阶逻辑的缺点：

  • 计算上不可判定（停机问题的推广）
  • 对模糊、不确定知识的表达能力弱
  • 开放世界假设——未声明的不一定为假

因此，实践中经常混合使用多种表示：

  • 用描述逻辑（Description Logic）做本体——它是可判定的OWL基础
  • 用贝叶斯网络/马尔可夫网络表示不确定性
  • 用向量嵌入（Embedding）表示语义相似性

十一、Prolog语言入门：用逻辑编程实现推理

11.1 什么是逻辑编程？

逻辑编程（Logic Programming）是一种声明式的编程范式：你只描述”什么”是真的，不描述”怎么”去证明它。

传统编程的思维是：

for each x in persons:
    if x.age > 18:
        print x.name

逻辑编程的思维是：

adult(X) :- person(X), age(X, Age), Age > 18.
? adult(X).

你声明”如果X是一个人且年龄大于18岁，那么X是成年人”，然后问”谁是成年人？“——Prolog会自动找出答案。

11.2 Prolog基础

Prolog程序由事实（Facts）和规则（Rules）组成。

事实描述已知的真命题：

parent(pam, bob).
parent(tom, bob).
parent(tom, liz).
parent(bob, ann).
parent(bob, pat).
parent(pat, jim).
female(pam).
male(tom).
male(bob).
female(liz).
female(ann).
female(pat).
male(jim).

规则描述推导关系：

mother(X, Y) :- parent(X, Y), female(X).      % X是Y的母亲，如果X是Y的父母且X是女性
father(X, Y) :- parent(X, Y), male(X).        % X是Y的父亲
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).  % X是Z的祖父母
sibling(X, Y) :- parent(Z, X), parent(Z, Y), X \= Y.  % X和Y是兄弟姐妹

查询（Query）问问题：

?- mother(X, jim).
X = pat.
 
?- grandparent(X, jim).
X = bob.
 
?- sibling(ann, pat).
true.

11.3 Prolog的执行机制：合一 + 回溯

Prolog的执行基于两个核心机制：

合一（Unification）：Prolog会自动找变量和项的统一。比如查询parent(X, Y)，Prolog会匹配所有事实，依次返回X和Y的不同取值。

回溯（Backtracking）：当一个查询有多种解时，Prolog会依次返回。输入分号;可以要求下一个解。

?- parent(X, Y).
X = pam,
Y = bob ;   % 按分号获取下一个解
X = tom,
Y = bob ;
X = tom,
Y = liz ;
...

11.4 列表和递归

Prolog处理递归结构（比如列表）非常强大：

% 基础情况：空列表的长度是0
length([], 0).
 
% 递归情况：非空列表的长度 = 1 + 尾部的长度
length([_|T], N) :- length(T, M), N is M + 1.
 
% 成员检查
member(X, [X|_]).
member(X, [_|T]) :- member(X, T).
 
% 追加
append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).

11.5 Prolog的局限

Prolog很强大，但也有明显局限：

  1. 效率问题：Prolog的搜索策略（深度优先）可能导致指数级回溯
  2. 无穷递归：没有终止检测，可能陷入死循环
  3. 表达力受限：Prolog只支持霍恩子句（一阶逻辑的可判定子集）
  4. 否定为失败：Prolog的not/1不是真正的逻辑否定，而是”如果证明不了则为真”——这叫失败即否定（Negation as Failure），和真正的封闭世界假设语义有关

尽管如此，Prolog仍然是学习逻辑编程和自动推理的最佳入门工具。

十二、动手实验：用Python实现简单的逻辑推理

12.1 用Python做命题逻辑推理

先从简单的开始，用Python实现命题逻辑的推理：

from enum import Enum
from typing import Dict, Callable
 
class Expr:
    """命题逻辑表达式基类"""
    pass
 
class Var(Expr):
    """命题变量"""
    def __init__(self, name: str):
        self.name = name
    def evaluate(self, env: Dict[str, bool]) -> bool:
        return env.get(self.name, False)
    def __repr__(self):
        return self.name
 
class Not(Expr):
    """否定"""
    def __init__(self, e: Expr):
        self.e = e
    def evaluate(self, env: Dict[str, bool]) -> bool:
        return not self.e.evaluate(env)
    def __repr__(self):
        return f"¬{self.e}"
 
class And(Expr):
    """合取"""
    def __init__(self, left: Expr, right: Expr):
        self.left = left
        self.right = right
    def evaluate(self, env: Dict[str, bool]) -> bool:
        return self.left.evaluate(env) and self.right.evaluate(env)
    def __repr__(self):
        return f"({self.left} ∧ {self.right})"
 
class Or(Expr):
    """析取"""
    def __init__(self, left: Expr, right: Expr):
        self.left = left
        self.right = right
    def evaluate(self, env: Dict[str, bool]) -> bool:
        return self.left.evaluate(env) or self.right.evaluate(env)
    def __repr__(self):
        return f"({self.left} ∨ {self.right})"
 
class Implies(Expr):
    """蕴含"""
    def __init__(self, left: Expr, right: Expr):
        self.left = left
        self.right = right
    def evaluate(self, env: Dict[str, bool]) -> bool:
        return not self.left.evaluate(env) or self.right.evaluate(env)
    def __repr__(self):
        return f"({self.left} → {self.right})"
 
# 使用示例
p = Var("P")
q = Var("Q")
 
# (P → Q) ∧ P → Q
formula = Implies(And(Implies(p, q), p), q)
 
# 验证这是重言式（永真式）
def is_tautology(formula: Expr) -> bool:
    """检查公式是否对所有赋值都为真"""
    variables = collect_vars(formula)
    for assignment in product([False, True], repeat=len(variables)):
        env = dict(zip(variables, assignment))
        if not formula.evaluate(env):
            return False
    return True
 
def collect_vars(expr: Expr) -> set:
    """收集所有变量名"""
    if isinstance(expr, Var):
        return {expr.name}
    elif isinstance(expr, Not):
        return collect_vars(expr.e)
    elif isinstance(expr, (And, Or, Implies)):
        return collect_vars(expr.left) | collect_vars(expr.right)
    return set()

12.2 简单的合一算法实现

from typing import Optional, Dict, Set, Tuple
from dataclasses import dataclass, field
 
@dataclass
class Substitution:
    """替换：变量到项的映射"""
    bindings: Dict[str, 'Term'] = field(default_factory=dict)
    
    def apply_to_term(self, term: 'Term') -> 'Term':
        """应用替换到项"""
        if isinstance(term, Var):
            if term.name in self.bindings:
                return self.apply_to_term(self.bindings[term.name])
            return term
        elif isinstance(term, Function):
            return Function(term.name, [self.apply_to_term(a) for a in term.args])
        return term
    
    def compose(self, other: 'Substitution') -> 'Substitution':
        """合成两个替换"""
        new_bindings = {}
        for var, term in other.bindings.items():
            new_bindings[var] = self.apply_to_term(term)
        for var, term in self.bindings.items():
            if var not in new_bindings:
                new_bindings[var] = self.apply_to_term(term)
        return Substitution(new_bindings)
 
@dataclass
class Var:
    """变量"""
    name: str
 
@dataclass
class Function:
    """函数"""
    name: str
    args: list
    
    def __eq__(self, other):
        return isinstance(other, Function) and self.name == other.name and self.args == other.args
    
    def __hash__(self):
        return hash((self.name, tuple(self.args)))
 
@dataclass
class Atom:
    """原子公式 P(t1, ..., tn)"""
    predicate: str
    terms: list
    
    def apply(self, subst: Substitution) -> 'Atom':
        """应用替换"""
        return Atom(self.predicate, [subst.apply_to_term(t) for t in self.terms])
 
def occurs_check(var: Var, term: 'Term') -> bool:
    """检查变量是否出现在项中"""
    if isinstance(term, Var):
        return var.name == term.name
    elif isinstance(term, Function):
        return any(occurs_check(var, arg) for arg in term.args)
    return False
 
def unify(s: 'Term', t: 'Term', subst: Substitution = None) -> Optional[Substitution]:
    """合一算法"""
    if subst is None:
        subst = Substitution()
    
    # 应用当前替换
    s = subst.apply_to_term(s)
    t = subst.apply_to_term(t)
    
    # 相同则无需替换
    if s == t:
        return subst
    
    # 变量的情况
    if isinstance(s, Var):
        if occurs_check(s, t):
            return None  # 违反出现检查
        new_subst = Substitution({s.name: t})
        return subst.compose(new_subst)
    
    if isinstance(t, Var):
        if occurs_check(t, s):
            return None
        new_subst = Substitution({t.name: s})
        return subst.compose(new_subst)
    
    # 函数的情况
    if isinstance(s, Function) and isinstance(t, Function):
        if s.name != t.name or len(s.args) != len(t.args):
            return None  # 函数名或元数不匹配
        
        result = subst
        for arg_s, arg_t in zip(s.args, t.args):
            result = unify(arg_s, arg_t, result)
            if result is None:
                return None
        return result
    
    return None
 
# 测试
if __name__ == "__main__":
    # P(x, f(y)) 和 P(g(z), f(w)) 合一
    s = Atom("P", [Var("x"), Function("f", [Var("y")])])
    t = Atom("P", [Function("g", [Var("z")]), Function("f", [Var("w")])])
    
    result = unify(s, t)
    print(f"合一结果: {result.bindings if result else '失败'}")

12.3 真值表枚举

枚举所有可能赋值来验证重言式或矛盾式：

from itertools import product
 
def truth_table(formula):
    """生成真值表"""
    vars = collect_vars(formula)
    n = len(vars)
    
    print(" | ".join(vars + [str(formula)]))
    print("-" * (7 * n + len(str(formula))))
    
    for assignment in product([True, False], repeat=n):
        env = dict(zip(vars, assignment))
        val = formula.evaluate(env)
        row = " | ".join(["T" if env[v] else "F" for v in vars] + [str(val)])
        print(row)
        
        if not val:
            return False  # 发现假赋值，不是重言式
    return True
 
# 验证 P ∨ ¬P 是重言式
p = Var("P")
print(f"P ∨ ¬P 是重言式: {truth_table(Or(p, Not(p)))}")
 
# 验证 P ∧ ¬P 是矛盾式
print(f"P ∧ ¬P 是矛盾式: {not truth_table(And(p, Not(p)))}")

十三、一阶逻辑的局限：为什么有时候一阶逻辑不够用？

13.1 不可判定性

一阶逻辑的第一个重大局限是不可判定性。

命题逻辑是可判定的——给定一个命题公式，我们可以（在有限时间内）算法地判断它是否有效。这归功于真值表枚举：命题变量只有有限多个可能赋值，逐一检查总能得出结论。

但一阶逻辑没有这样的有限枚举方法。论域可能是无限的，而且量词要求我们考虑”对所有对象”或”存在某个对象”——这没法通过有限次检查来验证。

丘奇-图灵论题告诉我们：一阶逻辑的普遍有效性（validity）问题是不可判定的。也就是说，不存在一个算法，对任意一阶公式都能在有限步内判断它是否有效。

这个结论不是”目前没找到算法”，而是数学上证明了不存在算法。

13.2 表达力的局限

一阶逻辑的表达力也是有限的。有些东西一阶逻辑说不了。

无法表达良基性：假设论域是所有集合，你想说”不存在无穷下降链”——即”没有无限递减的集合序列x₁ ⊇ x₂ ⊇ x₃ …”。这需要说”对于任意有限序列x₁, …, xₙ，至少有一个i使得xᵢ ⊈ xᵢ₊₁”，这用一阶逻辑可以表达。

但更复杂的情况呢？比如想形式化”自然数”的概念——需要说”存在一个没有前驱的元素（0），并且每个元素都有后继，并且没有无穷下降链”。前两条一阶逻辑能表达，但第三条（良基性）一阶逻辑表达不了。这需要二阶逻辑或者额外的公理。

Peano算术的限制：一阶Peano算术（PA）有标准模型（自然数），但也有非标准模型。紧致性定理保证了：如果PA是一致的，那么它有非标准模型——包含无穷大的”自然数”。一阶逻辑没法把标准自然数和所有可能的结构区分开来。

13.3 实践中的挑战

即使忽略理论局限，实践中用一阶逻辑也有很多挑战。

知识获取问题：把领域知识编码成一阶逻辑公式非常耗时，而且容易出错。工程师必须和领域专家紧密合作，才能准确地用逻辑语言表达知识。

计算复杂性：即使归结原理是完备的，它的在最坏情况下的复杂度是指数级甚至超指数级的。对于大规模知识库，需要各种优化技术（子句集简化、启发式搜索、索引结构等）。

封闭世界 vs 开放世界：一阶逻辑默认开放世界假设——未声明的不一定为假。但实际应用经常需要封闭世界假设——未声明的就是假的。这导致一阶逻辑在某些场景下过于”保守”。

处理不确定性：一阶逻辑是二值的——每个命题要么真要么假，没有”可能真”或者”90%真”的概念。这对于很多现实世界的推理（比如医学诊断）是不够的。

十四、从一阶逻辑到描述逻辑：为语义网设计的知识表示

14.1 为什么要发明描述逻辑？

一阶逻辑太”强”了——它的普遍有效性问题是不可判定的。虽然归结原理在理论上是完备的，但在实际应用中可能跑不出结果。

于是，人们开始研究可判定的一阶逻辑子集——在表达力和计算可行性之间找平衡。

描述逻辑（Description Logic, DL）就是这种努力的结果。它在80年代被系统研究，广泛应用于知识表示、语义网、本体工程等领域。

14.2 描述逻辑的基本构件

描述逻辑的核心概念是概念（Concept）和角色（Role）。

概念描述对象的类：

  • Person —— 所有人
  • Mother —— 所有母亲
  • Mother ∧ Person —— 既是母亲又是人
  • Mother ⊔ Doctor —— 母亲或医生（或者两者都是）
  • ∃hasChild.Person —— 有孩子是人的人
  • ∀hasChild.Doctor —— 所有孩子都是医生的人

角色描述对象之间的关系：

  • hasChild —— …的孩子
  • marriedTo —— …的配偶

概念包含（Subsumption）表示类的包含关系：

  • Mother ⊆ Person —— 母亲是人的子集
  • Mother ⊆ ∃hasChild.Person —— 所有母亲都有孩子是人

14.3 ALC：最基本的描述逻辑

ALC（Attributive Language with Complement）是最基础的、可判定的描述逻辑之一。它的语法：

构造器语法含义
原子概念A概念名称
全集⊤所有对象
空集⊥无对象
合取C ⊓ DC和D的交集
析取C ⊔ DC或D的并集
否定¬CC的补集
存在限制∃R.C有R指向C的对象
全称限制∀R.C所有R指向的都是C

ALC的推理问题是可判定的，而且有多项式空间的算法。

14.4 从描述逻辑到OWL

OWL（Web Ontology Language）是W3C推荐的本体语言，用于语义网。OWL的三个子语言（OWL Lite、OWL DL、OWL Full）对应不同的描述逻辑表达能力。

OWL DL 基于 SHOIN(D) 描述逻辑：

  • S = ALC + transitive roles
  • H = role hierarchies（角色包含）
  • O = nominals（枚举）
  • I = inverse roles（逆关系）
  • N = cardinality restrictions（数量限制）
  • (D) = data types（数据类型）

OWL是现代知识图谱（如Wikidata、DBpedia）和语义网的理论基础。它让机器能够”理解”概念之间的包含、相等、相交等关系，从而支持自动推理。

14.5 描述逻辑 vs 一阶逻辑

总结一下两者的关系：

方面一阶逻辑描述逻辑
表达力更强有限但实用
判定性不可判定可判定
主要应用数学定理证明本体工程、知识图谱
语法风格谓词+量词概念+角色
推理复杂度高可控

描述逻辑不是要取代一阶逻辑，而是针对特定应用场景的专门化。对于需要自动推理的大规模知识库，描述逻辑的判定性和可实现性是更好的选择。

十五、总结与延伸

一阶逻辑是人工智能知识表示的基石。它提供了：

  • 精确的语法：递归地定义什么是合法的公式
  • 清晰的语义：基于结构和赋值的真值理论
  • 强大的推理系统：自然演绎、归结原理
  • 深刻的元理论：完备性、紧致性、Löwenheim-Skolem

理解一阶逻辑，对于学习知识图谱、本体论、自动定理证明、逻辑编程都是必备基础。

当然，一阶逻辑也有局限：不可判定性、不支持不确定性、表达力有限。因此，实际系统往往结合多种表示方法：用描述逻辑做本体，用概率模型处理不确定性，用向量嵌入捕捉语义相似性。

延伸阅读：

  • 王浩《一阶逻辑与自动定理证明》—— 中文经典教材
  • Enderton《A Mathematical Introduction to Logic》—— 英文标准教材
  • Baader《Description Logic Handbook》—— 描述逻辑权威参考

参考文献

  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). 《一阶逻辑与自动定理证明》. 清华大学出版社.
  6. Baader, F., et al. (2003). The Description Logic Handbook. Cambridge University Press.
  7. Brachman, R. & Levesque, H. (2004). Knowledge Representation and Reasoning. Morgan Kaufmann.

相关文档

关系图谱

反向链接