Sherfiter's wiki for fun

第 3 章 · 谓词逻辑

命题逻辑有个致命局限:「所有人都会死」没法表达——它需要谈论「每一个 x」。谓词逻辑(一阶逻辑)补上两件武器:谓词(描述对象的性质/关系)与量词(∀ 所有、∃ 存在),推理能力从「命题之间」深入到「对象层面」。程序验证、数据库查询语言(第 1 章 SQL 的 EXISTS)、定理证明器,全是它的后代。

3.1 谓词与量词:把句子拆到对象层

谓词 = 带空位的命题模板。P(x):「x 是素数」,L(x, y):「x 大于 y」。填上对象(常量或变量)才得到有真值的命题:P(3) 真,P(4) 假。这和编程的函数直觉完全一致:谓词是「返回 boolean 的函数」(SQL 里就叫谓词,WHERE price > 100 的整条语句就是一个谓词)。

全称量词 ∀x P(x):对定义域里每一个 x,P(x) 都真。存在量词 ∃x P(x):至少有一个 x 使 P(x) 真。两个关键约定:量词的作用域(管辖到公式结尾或括号为止)、变量绑定(∀x 与 ∃x 里的 x 是「哑变量」,换名不影响含义,类似函数参数)。

定义域(论域)必须明确:「∀x P(x)」在「x 遍历所有实数」和「x 遍历全体程序员」下真值不同。写形式化语句的第一步永远是声明论域。

3.2 翻译:自然语言与形式语言互转

把中文翻译成谓词公式,是本章的核心技能(考试的主观题,工程里的「把需求写严谨」)。要点:量词顺序敏感、否定穿越量词要变号。

例:设 I(x) =「x 有互联网思维」,F(x, y) =「x 认识 y」:

  • 「所有人都认识某个人」:∀x ∃y F(x, y)(每个人有自己的 y);
  • 「有一个人所有人都认识」:∃y ∀x F(x, y)(同一个 y 是交际花)。

两个公式不等价(量词顺序在 ∀∃ 混用时有意义),这个差别在数学定义里致命:「对每个 ε 存在 δ」(函数连续)与「存在 δ 对每个 ε」(天差地别)。

否定穿越(量词版德摩根):

  • ¬∀x P(x) ≡ ∃x ¬P(x)(「不是所有人」=「有人不」);
  • ¬∃x P(x) ≡ ∀x ¬P(x)(「没有人」=「所有人都不」)。

数据库课第 2 章的除法运算(「选了所有课的学生」)在 SQL 里写成双重否定 NOT EXISTS,依据正是第二条:¬∃course(没选它)。形式逻辑直接变成高效 SQL 的写法指南。

3.3 推理:量词的进出规则

谓词逻辑的推理 = 命题逻辑的规则(第 2 章 MP/MT 照用)+ 量词进出规则:

  • 全称实例化(UI):∀x P(x) ⊢ P(a)(对所有成立的,对任一个成立);
  • 存在概括(EG):P(a) ⊢ ∃x P(x)(具体例子可上泛化);
  • 全称概括(UG):P(a) 对任意选取的 a 成立 ⊢ ∀x P(x)(这个 a 必须是「随便挑的」,挑了特殊的就犯法);
  • 存在实例化(EI):∃x P(x) ⊢ P(a)(a 是「新引入的名字」,代表那个未知者)。

规则顺序有讲究:UI 和 EI 连用时,先 EI 后 UI(先给存在者起名,再对全员用规则),倒过来就推出错误结论:

存在一个人爱打篮球(∃x B(x))
所有人都是人(∀x H(x))
错误推理:由 EI 设「那个人」叫 a,B(a);由 UI 用「那个人」a 推 H(a)……
→ 看似得出「爱打篮球的都是人」没问题,但若继续滥用 a 会推出「所有人爱打篮球」

考试重点就在「哪一步的 a 不是随便挑的」。严格推理序列的书写(每行:前提/依据)是形式化训练的基本功,它是后来「程序证明」「协议验证」的推理骨架。

3.4 谓词逻辑的表达力:几个经典形式化

练手的经典翻译,每个都是程序/数学里的真实概念:

  • 「每把钥匙能开某扇门」:∀k ∃d Opens(k, d);
  • 「存在一把万能钥匙」:∃k ∀d Opens(k, d);
  • 「函数 f 有界」:∃M ∀x (f(x) ≤ M);
  • 「a 是 f 的不动点」:f(a) = a,即 ∀x (x = a ↔ f(x) = x) 的特化;
  • 哥德巴赫猜想的骨架:∀n(n > 2 ∧ Even(n) → ∃p ∃q (Prime(p) ∧ Prime(q) ∧ p + q = n))。

最后这个值得一提:一个至今未解的世界级难题,形式化只要一行。「把非形式猜想变成精确公式」本身就是有价值的技能——错译的猜想研究下去全白费。

3.5 局限与展望:一阶逻辑的边界

一阶逻辑量词只管对象,不管谓词的谓词(「所有性质 P,若 P 对所有人成立则……」需要二阶逻辑)。它还有两个深层事实:有效性不可判定(不存在算法判定任意公式是否永真,Church-Turing,和停机问题同源,计算理论课的主角);但可满足性半可判定(存在的会找到)。工程上的回应:SMT 求解器(Z3)在限定片段里高效自动推理,程序验证(形式化验证 Rust/SeL4 内核)、测试用例生成都在用。逻辑作为「可计算的推理」,正是计算机科学的心脏地带。

常见错误

  • 量词顺序随手写。∀∃ 与 ∃∀ 的语义差(3.2 的两个「认识」句);翻译完自问一句「每个/同一个」。
  • 否定穿越不变号。¬∀x P(x) 写成 ∀x ¬P(x)(「不是所有都真」≠「所有都假」);三秒钟能查,数据库双重否定全靠它。
  • EI 之后乱用 UI。3.3 的名字纪律;推理题每一步自问「这个 a 是随便挑的吗」。
  • 论域忘了声明。∀x(x > 0) 在自然数论域真、在实数论域假;形式化第一句写「设论域为……」。

练习

  1. 翻译:用 P(x) =「x 会出错」,F(x) =「x 是机器」翻译:「所有机器都会出错」「并非所有机器都会出错」「有不出错的机器」「没有任何机器不出错」,并指出哪两对等价。
  2. 手算:判断推理是否有效并说明:「没有青蛙是诗人;有些两栖动物是诗人;所以有些两栖动物不是青蛙。」(形式化后走推理序列,注意 EI/UI 的次序。)
  3. 动手:用 SQL 验证 3.2 的双重否定:建学生-选课表,分别用 NOT EXISTS 写「选了全部课程的学生」和「一门课都没选的学生」,跑通。
  4. 思考:「∀∃ 与 ∃∀ 的区别」在程序验证里对应「对任意输入存在一个算法」与「存在一个万能算法」的区别。结合你学过的算法课内容(如「NP 问题验证器」),解释为什么这个看似语言学的区分,其实是计算复杂度的分水岭。
豫ICP备2026027944号