Skip to main content

数理逻辑

参考资料

引入

数理逻辑(Mathematical Logic)用数学方法研究 推理:什么样的论证是「站得住脚」的,跟内容无关,只看形式。它是计算机科学的基础——电路设计、程序验证、数据库查询、人工智能里的知识表示,本质上都是在跟逻辑打交道。

可以这样理解:逻辑把日常语言里的「因为……所以……」抽象成符号运算,于是「论证是否正确」就变成了「公式是否恒为真」这种可以机械检验的问题。这正是计算机擅长的事。

本章先讲 命题逻辑(只关心整句的真假),再讲 谓词逻辑(深入到句子内部的「对象」和「性质」)。

命题逻辑

命题

判断真假 的陈述句称为 命题(Proposition)。真值用 11(真)或 00(假)表示。

「明天会下雨」「1+1=21+1=2」是命题;「请关门!」「x+1=3x+1=3」不是命题——前者是祈使句无所谓真假,后者的真假取决于 xx,本身不确定。

不能再拆分的命题叫 原子命题,用 p,q,rp,q,r命题变元 表示;由联结词组合而成的叫 复合命题

联结词

联结词(Connective)是把命题粘起来的「运算符」,就像算术里的 +×÷+\,-\,\times\,\div

符号名称读法
¬p\neg p否定pp
pqp\land q合取ppqq
pqp\lor q析取ppqq
pqp\to q蕴含ppqq
pqp\leftrightarrow q等价pp 当且仅当 qq

直觉上:

  • 合取 pqp\land q 是「两个都要成立」,像电路里的 串联开关——全通才通。
  • 析取 pqp\lor q 是「至少一个成立」(注意是 可兼或,不是「二选一」),像 并联开关——有一个通就通。
  • 蕴含 pqp\to q 表达「承诺」:只要 pp 成立,就保证 qq 成立。它最容易让人困惑,下面单独说。
  • 等价 pqp\leftrightarrow q 是「两者真值一样」,即 p,qp,q 同真同假。

真值表

把所有变元的取值组合穷举一遍,列出复合命题的真值,就是 真值表(Truth Table)。nn 个变元有 2n2^n 行。

ppqq¬p\neg ppqp\land qpqp\lor qpqp\to qpqp\leftrightarrow q
0010011
0110110
1000100
1101111
tip

蕴含 pqp\to q 只有「前真后假」时为假,其余情形都真。

最反直觉的是 00\to 任何 = 真,对应「错误前提可以推出任何结论」。想象承诺「如果考一百分,就请你吃饭」——只要没考到一百分,无论我请不请,这句承诺都没被违背,所以算真。逻辑里的蕴含是这种「空泛成立」(vacuously true)的承诺,跟日常语言里隐含的因果关系并不一样。

联结词的完备性

一个有意思的事实:所有联结词都能用 ¬\neg\land(或 ¬\neg\lor)表示出来,比如 pq¬pqp\to q\Leftrightarrow\neg p\lor q。更进一步,单独一个 与非 \uparrow(NAND)或 或非 \downarrow(NOR)就能表示一切——这就是为什么数字电路里用 NAND 门可以搭出任何逻辑电路。

pq¬(pq),pq¬(pq)p\uparrow q\Leftrightarrow\neg(p\land q),\qquad p\downarrow q\Leftrightarrow\neg(p\lor q)

命题公式

由命题变元、联结词、括号按规则组成的式子称为 命题公式(合式公式,well-formed formula)。按真值情况分类:

  • 永真式(重言式,Tautology):在所有赋值下恒为真。
  • 永假式(矛盾式,Contradiction):恒为假。
  • 可满足式(Satisfiable):至少存在一种赋值使其为真。

判断一个公式属于哪类,最朴素的办法就是列真值表。「公式是否可满足」这个问题(SAT)是计算机科学里第一个被证明 NP-完全的问题,地位很特殊。

例:判断 (pq)(¬q¬p)(p\to q)\to(\neg q\to\neg p) 是哪类公式。逐行列真值表(记 A=pqA=p\to qB=¬q¬pB=\neg q\to\neg p):

ppqqpqp\to q¬q¬p\neg q\to\neg pABA\to B
00111
01111
10001
11111

最后一列恒为 11,故它是 重言式——这正是逆否等价 pq¬q¬pp\to q\Leftrightarrow\neg q\to\neg p 的另一种说法。

例:用真值表判断 p(qr)p\to(q\to r)(pq)r(p\land q)\to r 是否等值。两式各有 23=82^3=8 行,只需比较输出列。对照后会发现两列逐行相同(如 p=q=1,r=0p=q=1,r=0 时,左边 1(10)=10=01\to(1\to0)=1\to0=0,右边 (11)0=10=0(1\land1)\to0=1\to0=0;其余各行同理),故二者 等值。这条规律叫 输出律(exportation),编程里「嵌套 if 等价于条件用 && 连起来」就是它。

重要等值式

ABA\leftrightarrow B 是重言式,称 A,BA,B 等值,记 ABA\Leftrightarrow B。等值式是公式化简的「运算法则」,相当于代数里的恒等式。

双重否定¬¬pp\neg\neg p\Leftrightarrow p
幂等律pppp\land p\Leftrightarrow ppppp\lor p\Leftrightarrow p
交换律pqqpp\land q\Leftrightarrow q\land ppqqpp\lor q\Leftrightarrow q\lor p
结合律(pq)rp(qr)(p\land q)\land r\Leftrightarrow p\land(q\land r)
分配律p(qr)(pq)(pr)p\land(q\lor r)\Leftrightarrow(p\land q)\lor(p\land r)
德摩根律¬(pq)¬p¬q\neg(p\land q)\Leftrightarrow\neg p\lor\neg q
吸收律p(pq)pp\lor(p\land q)\Leftrightarrow p
零一律p11p\lor 1\Leftrightarrow 1p00p\land 0\Leftrightarrow 0
同一律p0pp\lor 0\Leftrightarrow pp1pp\land 1\Leftrightarrow p
排中律p¬p1p\lor\neg p\Leftrightarrow 1
矛盾律p¬p0p\land\neg p\Leftrightarrow 0
蕴含等价pq¬pqp\to q\Leftrightarrow\neg p\lor q
逆否等价pq¬q¬pp\to q\Leftrightarrow\neg q\to\neg p
等价展开pq(pq)(qp)p\leftrightarrow q\Leftrightarrow(p\to q)\land(q\to p)
tip

蕴含等价 pq¬pqp\to q\Leftrightarrow\neg p\lor q 是化简里最常用的一步:它把不好处理的 \to 消成 ¬\neg\lor,剩下的就能套德摩根律和分配律了。

等值演算

不列真值表、纯靠等值式一步步替换来证明等值或化简,称 等值演算。每一步都把局部子式换成等值的形式,整体真值不变。

例:化简 (pq)(p¬q)(p\lor q)\land(p\lor\neg q)

(pq)(p¬q)p(q¬q)分配律(提取 pp0矛盾律p同一律\begin{aligned} (p\lor q)\land(p\lor\neg q) &\Leftrightarrow p\lor(q\land\neg q) &&\text{分配律(提取 }p\text{)}\\ &\Leftrightarrow p\lor 0 &&\text{矛盾律}\\ &\Leftrightarrow p &&\text{同一律} \end{aligned}

例:证明 ¬(pq)p¬q\neg(p\to q)\Leftrightarrow p\land\neg q,这是「否定一个蕴含」的标准结果。

¬(pq)¬(¬pq)蕴含等价¬¬p¬q德摩根律p¬q双重否定\begin{aligned} \neg(p\to q) &\Leftrightarrow\neg(\neg p\lor q) &&\text{蕴含等价}\\ &\Leftrightarrow\neg\neg p\land\neg q &&\text{德摩根律}\\ &\Leftrightarrow p\land\neg q &&\text{双重否定} \end{aligned}

直觉上「并非『若 ppqq』」就是「pp 成立却 qq 不成立」——承诺被违背的唯一情形。

例:证明 (pq)(pr)p(qr)(p\to q)\land(p\to r)\Leftrightarrow p\to(q\land r)

(pq)(pr)(¬pq)(¬pr)蕴含等价¬p(qr)分配律p(qr)蕴含等价\begin{aligned} (p\to q)\land(p\to r) &\Leftrightarrow(\neg p\lor q)\land(\neg p\lor r) &&\text{蕴含等价}\\ &\Leftrightarrow\neg p\lor(q\land r) &&\text{分配律}\\ &\Leftrightarrow p\to(q\land r) &&\text{蕴含等价} \end{aligned}

化简到最后若得到 11 就是重言式、得到 00 就是矛盾式,所以等值演算也能用来判别公式类型。

范式

直接比较两个公式是否等值很麻烦,于是约定一种 标准写法,让等值的公式长得一样,这就是 范式(Normal Form)。

先约定两个词:

  • 文字(Literal):命题变元 pp 或其否定 ¬p\neg p
  • 简单合取式 / 简单析取式:若干文字的合取(如 p¬qp\land\neg q)/ 析取(如 ¬pq\neg p\lor q)。

两种基本范式:

  • 析取范式(Disjunctive Normal Form,DNF):若干 简单合取式之析取,形如 (pq)(¬pr)(p\land q)\lor(\neg p\land r)
  • 合取范式(Conjunctive Normal Form,CNF):若干 简单析取式之合取,形如 (pq)(¬pr)(p\lor q)\land(\neg p\lor r)

任何公式都能化成 DNF 和 CNF,步骤是:

  1. 蕴含等价 消去 \to\leftrightarrow
  2. 德摩根律¬\neg 一直内推到变元前。
  3. 分配律 展开成需要的形状。

主范式

普通范式不唯一(p(pq)p\lor(p\land q)pp 都是 DNF),不便于比较。主范式 通过「每个变元在每个子式里恰好出现一次」消除了这种自由度,于是 每个公式的主范式唯一

  • 极小项(minterm):每个变元恰出现一次的简单合取式,如 p¬qrp\land\neg q\land r。它在真值表里 恰有一行为真
  • 极大项(maxterm):每个变元恰出现一次的简单析取式,如 ¬pq¬r\neg p\lor q\lor\neg r。它 恰有一行为假
  • 主析取范式(principal DNF):把真值表里所有取值为 的行对应的极小项析取起来。
  • 主合取范式(principal CNF):把所有取值为 的行对应的极大项合取起来。

直觉很简单:每个极小项「点亮」真值表里的一行,主析取范式就是把所有该真的行点亮、其余保持假。这也说明了为什么它唯一——真值表唯一,对应的极小项集合就唯一。

tip

记口诀:主析取看真行、用极小项主合取看假行、用极大项。两者互补,知道一个就能写出另一个。

极小项与极大项的编号

约定一个变元顺序(如 p,q,rp,q,r),把每个极小项里的变元 正则号为 11、否定号为 00,读成二进制就是它的编号 mim_i。极大项相反:变元正则号为 00、否定号为 11

例:三变元下 m5=m101=p¬qrm_5=m_{101}=p\land\neg q\land r(它只在 p=1,q=0,r=1p=1,q=0,r=1 这行为真);M5=M101=¬pq¬rM_5=M_{101}=\neg p\lor q\lor\neg r(它只在 p=1,q=0,r=1p=1,q=0,r=1 这行为假)。同一编号的极小项与极大项互为否定:¬miMi\neg m_i\Leftrightarrow M_i

由此有一条对偶关系:若真值表里真的行编号集合是 SS,则

主析取范式=iSmi,主合取范式=iSMi\text{主析取范式}=\bigvee_{i\in S}m_i,\qquad \text{主合取范式}=\bigwedge_{i\notin S}M_i

求主范式完整算例

例:求 p(qr)p\to(q\land r) 的主析取范式与主合取范式。先列真值表(变元序 p,q,rp,q,r,编号 070\sim7):

编号ppqqrrqrq\land rp(qr)p\to(q\land r)
000001
100101
201001
301111
410000
510100
611000
711111

真的行是 {0,1,2,3,7}\set{0,1,2,3,7},假的行是 {4,5,6}\set{4,5,6}。于是主析取范式取这五行的极小项:

m0m1m2m3m7=¬p¬q¬r    pqrm_0\lor m_1\lor m_2\lor m_3\lor m_7 =\neg p\land\neg q\land\neg r\ \lor\ \dots\ \lor\ p\land q\land r

主合取范式取另外三行的极大项(编号 4=1004=1005=1015=1016=1106=110):

M4M5M6=(¬pqr)(¬pq¬r)(¬p¬qr)M_4\land M_5\land M_6 =(\neg p\lor q\lor r)\land(\neg p\lor q\lor\neg r)\land(\neg p\lor\neg q\lor r)

两者所用的编号正好互补({0,1,2,3,7}\set{0,1,2,3,7}{4,5,6}\set{4,5,6} 并起来是全部 88 个),这是检验有没有写漏的好办法。也可不画真值表、直接由等值演算化成主析取范式:把公式化成析取范式后,对每个缺变元的简单合取式补上 (x¬x)(x\lor\neg x) 再展开即可。

推理

推理形式

从一组 前提 A1,,AnA_1,\dots,A_n 推出 结论 BB,记为:

A1A2AnBA_1\land A_2\land\dots\land A_n\Rightarrow B

推理 有效(Valid)当且仅当 (A1An)B(A_1\land\dots\land A_n)\to B重言式——也就是说,只要前提全真,结论就不可能假。注意「有效」只管形式对不对,前提本身是真是假它不负责。

常用推理规则

名称规则
假言推理(pq)pq(p\to q)\land p\Rightarrow q
拒取式(pq)¬q¬p(p\to q)\land\neg q\Rightarrow\neg p
析取三段论(pq)¬pq(p\lor q)\land\neg p\Rightarrow q
假言三段论(pq)(qr)pr(p\to q)\land(q\to r)\Rightarrow p\to r
化简律pqpp\land q\Rightarrow p
附加律ppqp\Rightarrow p\lor q
构造性二难(pq)(rs)(pr)qs(p\to q)\land(r\to s)\land(p\lor r)\Rightarrow q\lor s

证明方法

实际证明一个推理有效,除了列真值表,更常用的是 构造证明:从前提出发,每一步引用一条推理规则或等值式,逐行推到结论。常见策略有三种:

  • 直接证法:从前提出发,正向逐步推出结论。
  • 附加前提法(CP 规则):当结论形如 ABA\to B 时,把 AA 当作额外前提加进去,只要能推出 BB,原结论即成立。依据是 (ΓA)B(\Gamma\land A)\to BΓ(AB)\Gamma\to(A\to B) 等值。
  • 归谬法(反证法):把结论的 否定 ¬B\neg B 加入前提,若能推出 矛盾(如 r¬rr\land\neg r,即 00),则说明 ¬B\neg B 与前提不相容,故 BB 成立。
tip

结论是 蕴含式 时优先用附加前提法,能把目标拆小;结论是 否定式 或难以正面下手时用归谬法。两者本质都是把「难证的目标」换成「好证的等价命题」。

直接证法算例

例:前提 pqp\to qqrq\to rpp,证结论 rr。从前提正向推:

(1) p前提(2) pq前提(3) q(1)(2) 假言推理(4) qr前提(5) r(3)(4) 假言推理\begin{aligned} &(1)\ p &&\text{前提}\\ &(2)\ p\to q &&\text{前提}\\ &(3)\ q &&(1)(2)\ \text{假言推理}\\ &(4)\ q\to r &&\text{前提}\\ &(5)\ r &&(3)(4)\ \text{假言推理} \end{aligned}

附加前提法算例

例:前提 p(qr)p\to(q\to r)pp,证结论 qrq\to r。结论是蕴含式,把前件 qq 当附加前提加入:

(1) q附加前提(2) p前提(3) p(qr)前提(4) qr(2)(3) 假言推理(5) r(1)(4) 假言推理\begin{aligned} &(1)\ q &&\text{附加前提}\\ &(2)\ p &&\text{前提}\\ &(3)\ p\to(q\to r) &&\text{前提}\\ &(4)\ q\to r &&(2)(3)\ \text{假言推理}\\ &(5)\ r &&(1)(4)\ \text{假言推理} \end{aligned}

推出 rr,故附加前提下结论成立,由 CP 规则原结论 qrq\to r 得证。

归谬法算例

例:前提 pqp\lor qprp\to rqrq\to r,证结论 rr(这正是「构造性二难」的一个特例)。把结论的否定 ¬r\neg r 加入前提找矛盾:

(1) ¬r否定结论(2) pr前提(3) ¬p(1)(2) 拒取式(4) qr前提(5) ¬q(1)(4) 拒取式(6) ¬p¬q(3)(5) 合取(7) pq前提(8) ¬(pq)(6) 德摩根律(9) (pq)¬(pq)(7)(8) 矛盾\begin{aligned} &(1)\ \neg r &&\text{否定结论}\\ &(2)\ p\to r &&\text{前提}\\ &(3)\ \neg p &&(1)(2)\ \text{拒取式}\\ &(4)\ q\to r &&\text{前提}\\ &(5)\ \neg q &&(1)(4)\ \text{拒取式}\\ &(6)\ \neg p\land\neg q &&(3)(5)\ \text{合取}\\ &(7)\ p\lor q &&\text{前提}\\ &(8)\ \neg(p\lor q) &&(6)\ \text{德摩根律}\\ &(9)\ (p\lor q)\land\neg(p\lor q) &&(7)(8)\ \text{矛盾} \end{aligned}

得到矛盾 00,故 ¬r\neg r 与前提不相容,结论 rr 成立。

谓词逻辑

命题逻辑把整句话当成一个不可分的真值,于是无法刻画「所有人都会死」与「苏格拉底是人」推出「苏格拉底会死」这种推理——因为这里的关键是句子内部的「所有」和「是人」。谓词逻辑(Predicate Logic,又称一阶逻辑)深入句子内部,引入 谓词量词

谓词与量词

  • 个体词:被研究的对象,用 a,b,ca,b,c 表示 常元x,y,zx,y,z 表示 变元;它们的取值范围叫 个体域(论域)。
  • 谓词:刻画对象的性质或对象间的关系,记 P(x)P(x)(「xx 是人」)、R(x,y)R(x,y)(「xx 大于 yy」)。代入具体个体后才有真假。
  • 全称量词 x\forall x:「对所有 xx」,是一种「无限的合取」。
  • 存在量词 x\exists x:「存在 xx」,是一种「无限的析取」。

于是开头那个推理可写成 x(P(x)D(x))\forall x\,(P(x)\to D(x))P(a)P(a),推出 D(a)D(a)

tip

量词与个体域 紧密绑定,翻译时容易出错:

  • 全称量词通常配 蕴含:「所有学生都努力」是 x(S(x)H(x))\forall x\,(S(x)\to H(x)),而不是 x(S(x)H(x))\forall x\,(S(x)\land H(x))(后者意思是「万物都既是学生又努力」)。
  • 存在量词通常配 合取:「有学生努力」是 x(S(x)H(x))\exists x\,(S(x)\land H(x)),而不是 x(S(x)H(x))\exists x\,(S(x)\to H(x))

翻译算例

设个体域为全体人,S(x)S(x):「xx 是学生」,P(x)P(x):「xx 用功」,M(x,y)M(x,y):「xx 认识 yy」。

例:「所有学生都用功」译为 x(S(x)P(x))\forall x\,(S(x)\to P(x))。若误写成 x(S(x)P(x))\forall x\,(S(x)\land P(x)),意思变成「每个人既是学生又用功」——把非学生也卷进来了,错。

例:「有的学生用功」译为 x(S(x)P(x))\exists x\,(S(x)\land P(x))。若误写成 x(S(x)P(x))\exists x\,(S(x)\to P(x)),因为蕴含「前件假即真」,只要存在 任何一个非学生(让 S(x)S(x) 假)整句就为真,跟「有学生用功」毫无关系,错得离谱。

例:「没有学生不用功」。先直译为 ¬x(S(x)¬P(x))\neg\exists x\,(S(x)\land\neg P(x)),再用量词否定律推进否定:

¬x(S(x)¬P(x))x¬(S(x)¬P(x))x(S(x)P(x))\neg\exists x\,(S(x)\land\neg P(x)) \Leftrightarrow\forall x\,\neg(S(x)\land\neg P(x)) \Leftrightarrow\forall x\,(S(x)\to P(x))

化回了「所有学生都用功」——两种说法等值,这也验证了翻译没错。

例:「每个学生都认识某个用功的人」译为 x(S(x)y(P(y)M(x,y)))\forall x\,\bigl(S(x)\to\exists y\,(P(y)\land M(x,y))\bigr)。注意 y\exists yx\forall x 的辖域内,所以「某个用功的人」可以因学生而异——这正是 \forall\exists 次序的含义。

约束变元与自由变元

落在某个量词辖域内、被该量词「管住」的变元称 约束变元(Bound Variable),其余称 自由变元(Free Variable)。含自由变元的公式真假未定,像命题里的 x+1=3x+1=3;闭式(无自由变元)才有确定真假。

换名规则:约束变元可以改名(xP(x)yP(y)\forall x\,P(x)\Leftrightarrow\forall y\,P(y)),但新名字不能与辖域内已有的其他变元冲突,否则会改变含义。这跟编程里函数局部变量改名同理——只要不撞名,叫什么都行。

谓词的等值演算

命题逻辑的所有等值式在谓词逻辑里依然成立,此外还有专门处理量词的规则:

量词否定(量词的德摩根律)

¬xP(x)x¬P(x),¬xP(x)x¬P(x)\neg\forall x\,P(x)\Leftrightarrow\exists x\,\neg P(x),\qquad \neg\exists x\,P(x)\Leftrightarrow\forall x\,\neg P(x)

含义直白:「不是所有都满足」等于「存在一个不满足」;「不存在满足的」等于「所有都不满足」。否定一个量词,就是把它换成另一个量词、并把否定推进去。

量词辖域收缩与扩张(设 QQ 中不含 xx,故 xxQQ 中自由出现与否不影响):

x(P(x)Q)xP(x)Q,x(P(x)Q)xP(x)Q\forall x\,(P(x)\land Q)\Leftrightarrow\forall x\,P(x)\land Q,\qquad \exists x\,(P(x)\lor Q)\Leftrightarrow\exists x\,P(x)\lor Q

量词分配

x(P(x)Q(x))xP(x)xQ(x)\forall x\,(P(x)\land Q(x))\Leftrightarrow\forall x\,P(x)\land\forall x\,Q(x) x(P(x)Q(x))xP(x)xQ(x)\exists x\,(P(x)\lor Q(x))\Leftrightarrow\exists x\,P(x)\lor\exists x\,Q(x)
tip

分配只在「\forall\land」「\exists\lor」时是等值;交叉情形 只能单向蕴含,不能划等号。例如:

xP(x)xQ(x)  x(P(x)Q(x))\forall x\,P(x)\lor\forall x\,Q(x)\ \Rightarrow\ \forall x\,(P(x)\lor Q(x))

反过来不成立——「每个数要么正要么负」是真的,但「所有数都正」和「所有数都负」都假。

多重量词的次序

同类量词可以交换次序,异类量词 不能随便交换

xyP(x,y)yxP(x,y),xyP(x,y)yxP(x,y)\forall x\,\forall y\,P(x,y)\Leftrightarrow\forall y\,\forall x\,P(x,y),\qquad \exists x\,\exists y\,P(x,y)\Leftrightarrow\exists y\,\exists x\,P(x,y)

\forall\exists 的次序事关重大:

yxP(x,y)  xyP(x,y)\exists y\,\forall x\,P(x,y)\ \Rightarrow\ \forall x\,\exists y\,P(x,y)

只能这样单向推,反向不成立。设 P(x,y)P(x,y) 为「yyxx 的母亲」:

  • xyP(x,y)\forall x\,\exists y\,P(x,y):每个人都有母亲(母亲可以因人而异)——真。
  • yxP(x,y)\exists y\,\forall x\,P(x,y):存在一个人是 所有人 共同的母亲——假。

关键在于:后置量词依赖前置量词时,y\exists y 选的 yy 是否允许随 xx 变。xy\forall x\,\exists y 允许 yyxx 变,yx\exists y\,\forall x 要求一个 yy 通吃——后者强得多。极限定义里 εN\forall\varepsilon\,\exists N 的次序之所以不能调换,正是这个道理。

前束范式

把所有量词 提到公式最前面、辖域覆盖其后整个式子的形式,称 前束范式(Prenex Normal Form):

(Q1x1)(Q2x2)(Qkxk)M(Q_1 x_1)(Q_2 x_2)\cdots(Q_k x_k)\,M

其中每个 QiQ_i\forall\existsMM不含量词 的公式(母式)。任何谓词公式都能化成前束范式,步骤:

  1. 消去 \to\leftrightarrow
  2. 用量词否定律把 ¬\neg 推到谓词前。
  3. 必要时 换名,避免不同量词用了同一变元而提取时冲突。
  4. 用辖域扩张律把量词逐个提到最前。

前束范式把「量词结构」和「命题结构」彻底分开,是判定、模型论里进一步处理(如 Skolem 化)的标准起点。

例:求 xP(x)xQ(x)\forall x\,P(x)\to\exists x\,Q(x) 的前束范式。两个量词都用了 xx,直接提取会冲突,所以先换名再提取:

xP(x)xQ(x)¬xP(x)xQ(x)蕴含等价x¬P(x)xQ(x)量词否定x¬P(x)yQ(y)换名xy(¬P(x)Q(y))辖域扩张\begin{aligned} \forall x\,P(x)\to\exists x\,Q(x) &\Leftrightarrow\neg\forall x\,P(x)\lor\exists x\,Q(x) &&\text{蕴含等价}\\ &\Leftrightarrow\exists x\,\neg P(x)\lor\exists x\,Q(x) &&\text{量词否定}\\ &\Leftrightarrow\exists x\,\neg P(x)\lor\exists y\,Q(y) &&\text{换名}\\ &\Leftrightarrow\exists x\,\exists y\,(\neg P(x)\lor Q(y)) &&\text{辖域扩张} \end{aligned}

母式 ¬P(x)Q(y)\neg P(x)\lor Q(y) 已不含量词,前缀 xy\exists x\,\exists y 即为所求。若中途不换名、把两个 x\exists x 直接合并,会错误地强迫「不用功」和「用功」指同一个 xx,含义就变了——这是求前束范式最常见的错。