1.2 命题逻辑与谓词逻辑

1.2 命题逻辑与谓词逻辑

本节摘要：命题逻辑研究联结词（非、且、或、蕴含、等值）对真值的运算，谓词逻辑再加上量词，使"所有""存在"可以精确化。本节从真值表讲到范式，从三段论讲到量词消去，最后用 SymPy 的 SAT 求解器做一次完整实战：把一段自然语言论证翻译成符号、机器判定其有效性，并顺路理解 SAT 为什么是 NP 完全问题的代表。

一道 logic puzzle 引出的机器推理

三类经典的逻辑谜题（骑士与骗子、 scheduling 排班、电路化简）背后都是同一个计算问题：给定一堆命题变元和约束，问是否存在一组真值赋值让所有约束同时满足——可满足性问题 SAT。计算机能"推理"，靠的正是把推理化归为这类组合搜索。但在把问题交给机器之前，得先有一套没有歧义的语言，这就是命题逻辑与谓词逻辑的本职工作。

命题逻辑：真值的代数

命题逻辑的基本单位是能判断真假的陈述句。一个自然数命题"7 是素数"不可再分，记作 p；复合命题用五个联结词搭建。蕴含是最反直觉的一个："如果 p 则 q"只在 p 真 q 假时为假——空承诺不算撒谎。很多"悖论感"其实来自把日常语言的"如果"与逻辑蕴含混为一谈。真值表是这套代数的乘法口诀：

from itertools import product

def implies(p, q):
    return (not p) or q      # 蕴含的真值定义：仅 p 真 q 假时为假

# 打印 (p 蕴含 q) 等值于 (非 p 或 q) 的完整真值表验证
print(f"{'p':^6}{'q':^6}{'p->q':^8}{'~p|q':^8}")
for p, q in product([True, False], repeat=2):
    left, right = implies(p, q), (not p) or q
    print(f"{str(p):^6}{str(q):^6}{str(left):^8}{str(right):^8}")
    assert left == right
# 输出四行，两列完全一致：蕴含确实可以改写为析取形式
​

这个改写不是技巧而是范式化：任何命题公式都能等值改写为合取范式（子句的 AND，子句是文字的 OR），而合取范式正是 SAT 求解器的输入格式。逻辑与计算在这里第一次握手。

有效性与可满足性是一枚硬币的两面："前提推出结论"等价于"前提与结论的否定合在一起不可满足"。因此检验一段论证是否有效，可以转化成检查一个公式是否无解：

from sympy import symbols, satisfiable, Not, And, Implies

p, q, r = symbols('p q r')

# 经典三段论：若 p 蕴含 q，且 p，则 q（肯定前件式）
argument = Implies(And(Implies(p, q), p), q)
print(satisfiable(Not(argument)))   # 输出 False：否定论证不可满足，论证有效

# 交换前提位置的谬误：若 p 蕴含 q，且 q，则 p（肯定后件谬误）
fallacy = Implies(And(Implies(p, q), q), p)
print(satisfiable(Not(fallacy)))    # 输出 {p: False, q: True}：存在反例赋值，论证无效
​

第二段代码给出的是反例：p 假 q 真时两个前提都成立但结论不成立。机器在这里扮演的角色是"谬误探测器"——日常辩论里大量错误论证都属于肯定后件，值得亲手跑一遍加深印象。

谓词逻辑：给语言装上量词

命题逻辑的表达力不够刻画数学陈述。"每个素数都大于 1"在命题逻辑里只是一个整体 p，无法拆开论证。谓词逻辑引入三件新工具：个体变元（论域中的对象）、谓词（对象的性质或关系）、量词（全称与存在）。于是"每个素数都大于 1"翻译成"对任意 x，若 x 是素数则 x 大于 1"，量词的辖域、变元的约束与自由这些细节决定推理的合法性。

量词否定律是日常推理最常用的等值式："并非所有 x 都满足 P"等价于"存在 x 不满足 P"。医生说"不是所有药都有效"，与"存在无效的药"说的是同一件事。数轴语言里有个经典警告：交换两个量词的顺序会改变含义——"对任意 epsilon 存在 delta"（连续性定义）与"存在 delta 对任意 epsilon"（一致连续的弱化版）天差地别，分析学的严谨性常就严谨在这一格。

从自然语言到谓词公式再到机器检查

用 SymPy 做有限论域上的量词消去实战：

from sympy import symbols, Or, And, Not, satisfiable

# 有限论域量化：全称量词展开为合取，存在量词展开为析取
domain = [1, 2, 3, 4]
def for_all(pred): return And(*[pred(x) for x in domain])
def exists(pred):  return Or(*[pred(x) for x in domain])

even = lambda x: (x % 2 == 0) == True
# 论断：存在偶数 且 并非所有数都是偶数
claim = And(exists(even), Not(for_all(even)))
print(claim)               # 直接给出 True 的布尔结果
# 全称展开与存在展开的规模随论域指数增长——这正是 SAT 难度的直观来源
​

命题逻辑与谓词逻辑的表达力阶梯

NP 完全：推理的价格标签

合取范式的可满足性是 NP 完全问题（Cook-Levin 定理）：解一旦给出可以在多项式时间验证，但已知算法最坏需要指数时间。这不是坏消息的终点——现代 SAT 求解器靠冲突驱动子句学习等技术，在实践中能处理百万变元的工业实例。工程启示有两层：其一，把验证问题编码成 SAT 是一条成熟路线（硬件验证、排班、密码分析都在用）；其二，理论上"不可高效"不代表实践上做不动，复杂度与工程之间永远隔着启发式的空间。

⚠️ 常见坑：把蕴含当因果。"如果下雨则地湿"为真，不意味着下雨导致地湿，只意味着"下雨且地没湿"这个组合被排除。逻辑只承诺真值关系，因果是另一套语义。

本节要点回顾

• 五个联结词的真值语义中，蕴含最反直觉：仅"真前件假结论"为假；
• 有效性与可满足性互补：检验论证等价于检查其否定的可满足性，这是机器推理的入口；
• 谓词逻辑用量词突破命题逻辑的表达力天花板，量词顺序不可随意交换；
• 有限论域上量词可展开为合取与析取，规模指数爆炸正是 NP 完全性的直观形态；
• 实践层面，SAT 编码是硬件验证与约束求解的主流手段，复杂度理论划界但工程仍大有可为。

语言备齐了，下一节回到推理的骨架本身：数学归纳法如何让"无穷多个命题"被有限步骤证明。