一、谓词与谓词公式

谓词：表示个体词性质或相互之间关系的词

量词：用来表示个体数量的词是

谓词的量化：给谓词加上量词

一元目谓词P(x)、n元目谓词P(x, y, z, ...)它们是命题形式而非命题

因为既没有指定谓词符号P的含义，而且个体词x、y等也是个体变项而不代表某个具体的事物，从而无法确定P(x)、P(x, y)的真值。

仅当赋予谓词确定含义，并且个体词取定为个体常项而非个体变项时，命题形式才化为命题。

设A为一个谓词公式，若A在任何解释下真值均为真，则称A为普遍有效的公式/逻辑有效式。例如(∀x) (P(x)∨┐P(x))

若A在任何解释下真值均为假，则称A为不可满足的公式/矛盾式，例如(∀x)P(x)∧(∃y) ┐P(y)

若至少存在一个解释使A为真，则称A为可满足的公式

Church-Turing定理：对任一谓词公式而言，没有一个可行的方法判明它是否是普遍有效的。即谓词逻辑是不可判定的

但是谓词公式的某些子类是可判定的

命题公式 p→q 的代换实例：如P(y)→Q(z)、(∀x)P(x)→(∃x)Q(x)般用谓词公式处处代替各个命题变项

命题公式中，重言式的代换实例都是逻辑有效式、矛盾式的代换实例都是矛盾式。

自然语言形式化

存在唯一的偶素数：∃x(Prime(x)∧Even(x))∧(∀y)(Prime(y)∧Even(y)→Equal(x, y))

G(x)表示x是金子、L(x)表示x会闪光：(∀x)(G(x)→L(x))∧(∃x)(L(x)∧┐G(x))

F(x)表示x是乌鸦、G(x, y)表示x与y一般黑：

(∀x)(∀y)(F(x)∧F(y)→G(x , y))

⟺(∀x)(∀y)(┐(F(x)∧F(y))∨G(x , y))

⟺(∀x)(∀y)┐((F(x)∧F(y))∧┐G(x , y))

⟺(∀x)┐(∃y)((F(x)∧F(y))∧┐G(x , y))

⟺┐(∃x)(∀y)((F(x)∧F(y))∧┐G(x , y))

∃x Even(x) ∧ ∃x Odd(x) 和∃x (Even(x)∧Odd(x))不等价，前者表示存在一个正奇数也存在一个正偶数，后者表示存在一个数既是正奇数又是正偶数

∀x Even(x) ∨ ∀x Odd(x) 和∀x (Even(x)∨Odd(x))不等价，前者表示所有数都是正偶数，或者所有数都是正奇数

后者表示所有数都是正奇数或正偶数

⭐️∀x∃yGreater(y, x) 和∃y∀xGreater(y, x)，前者表示对于任一个正整数而言，都存在比它大的正整数

后者表示存在一个正整数，大于任何正整数

谓词逻辑的等值演算

设论域 D={a₁, a₂, …, a_m} 是有限集合，则有(∀x)A(x)⟺A(a₁)∧A(a₂)∧…∧A(a_m) 、(∃x)A(x)⟺A(a₁)∨A(a₂)∨…∨A(a_m)

量词否定等值式/德摩根律：┐(∀x)A(x)⟺(∃x)┐A(x)、┐(∃x)A(x)⟺(∀x)┐A(x)

量词辖域收缩与扩张等值式：∀/∃x(A(x)∨/∧B)⟺∀/∃x(A(x))∨/∧B

量词分配等值式：∀x(A(x)∧B(x))⟺∀xA(x)∧∀xB(x)、∃x(A(x)∨B(x))⟺ ∃xA(x)∨∃xB(x)

例题：

∃x(P(x)→Q(x))

⟺∃x(┐P(x)∨Q(x))

⟺∃x┐P(x)∨∃xQ(x)

⟺┐∀xP(x)∨∃xQ(x)

⟺∀xP(x)→∃xQ(x)

反驳：

要证明∀x(P(x)→Q(x))为假的办法

┐∀x(P(x)→Q(x))

⟺∃x(P(x)∧┐Q(x))

就是要找到某个x，使得P(x)为真的同时Q(x)为假

二、前束范式

所有量词都位于该公式的最左边：∀xP(x)∨∀xQ(x)不是

所有量词前都不含否定词：┐∀xP(x , y)不是

量词的辖域都延伸到整个公式的末端：∀x(P(x)→Q(x))∨R(z)不是

化前束范式的方法：

┐((∀x)(∃y)P(a, x, y)→(∃x)(┐(∀y)Q(y, b)→R(x)))

（1）消去→

⟺┐(┐(∀x)(∃y)P(a, x, y)∨(∃x)(┐┐(∀y)Q(y, b)∨R(x)))

（2）┐右移

⟺(∀x)(∃y)P(a, x, y)∧┐(∃x)((∀y)Q(y, b)∨R(x)))

⟺(∀x)(∃y)P(a, x, y)∧(∀x)(┐(∀y)Q(y, b)∧┐R(x)))

⟺(∀x)(∃y)P(a, x, y)∧(∀x)((∃y)┐Q(y, b)∧┐R(x)))

（3）量词左移

⟺(∀x)((∃y)P(a, x, y)∧((∃y)┐Q(y, b)∧┐R(x)))

⟺(∀x)(∃y)(∃z)(P(a, x, y)∧┐Q(z, b)∧┐R(x)))

⟺(∀x)(∃y)(∃z)M(a, b, x, y, z)

三、谓词逻辑的推理

∀xF(x)∧∀yG(y)⟹∀xF(x)

∀xF(x)⟹∀xF(x)∨∀yG(y)

∀xA(x)∨∀xB(x)⟹∀x(A(x)∨B(x))

∃x(A(x)∧B(x))⟹∃xA(x)∧∃xB(x)

∀x(A(x)→B(x))⟹∀xA(x)→∀xB(x)以及∃xA(x)→∃xB(x)

全称推广规则/全称量词引入规则(UG)

P(y)⟹∀xP(x)，其中y是论域中任意个体

意指如果任意个体y∈D都具有性质P，那么D中所有个体x都具有性质P。

该规则使用的条件是： 无论P(y)中自由出现的个体变项y取何值，P(y)应该为真；取代自由出现的y的x不能在P(y)中约束出现

例如(∃x)G(x, y)对任意给定的y都成立，不能通过全称量词引入变为(∀x)(∃x)G(x, x)

全称举例规则/全称量词消去规则(US)

∀xP(x)⟹P(y)，其中y是论域中一个体

意指如果所有的x∈D都具有性质P，那么D中任一个体y必具有性质P

该规则使用的条件是：取代x的y应为任意的不在P(x)中约束出现的个体变项；用y取代P(x)中自由出现的x时，必须在x自由出现的一切地方进行取代

例如(∀x)(∃y)G(x, y)不能通过全称量词消去变为(∃y)G(y, y)

存在推广规则/存在量词引入规则(EG)

P(a)⟹(∃x)P(x)，其中a是论域中一个体常项。

意指如果有个体常项a具有性质P，那么(∃x)P(x)必真。

该规则使用的条件是： a是特定的个体常项 ；取代a的x不在P(a)中出现过

存在举例规则/存在量词消去规则(ES)

(∃x)P(x)⟹P(a)，其中a是论域中的一个个体常项。

意指如果论域D中存在某个体具有性质P，那么必有特定个体a具有该性质P。

该规则使用的条件是：a是使P为真的特定的个体常项；a不在P(x)中出现；P(x)中没有其它自由出现的个体变项；a是在推导中未曾使用过的

⭐例如(∃y)G(x, y)不能通过存在量词消去变为G(x, a)，因为哪个个体使其成立依赖于x，不是所有x都有同一个a使得G(x, a)成立

例题：

（1）(∃x)Q(x) （前提引入）

（2）(∃x)~Q(x) （前提引入）

（3）Q(a) （对(1)的存在量词消去）

（4）┐Q(a) （对(2)的存在量词消去）

（5）Q(a)∧┐Q(a) （(3)(4)合取）

（6）(∃x)(Q(x)∧┐Q(x)) （存在量词引入）

错误之处：（4）中做的是存在量词消去，a必须是在推导中未曾使用过的

例题：

（1）(∀x)(P(x)→Q(x)) （前提引入）

（2） (∃x)P(x) （前提引入）

（3）P(c)→Q(c) （对(1)的全称量词消去）

（4）P(c) （对(2)的存在量词消去）

（5）Q(c) （(3)(4)假言推理）

（6）(∃x)Q(x) （存在量词引入）

错误之处：(4)中使P(c)成立的c不一定就是(3)中使P(c)→Q(c) 成立的c

把(3)和(4)调换顺序即可，全称量词消去时c可以任意取

例题：∃xP(x)→∀xQ(x)，求证∀x(P(x)→Q(x))

证明：首先需要化为前束范式以及进行置换

⟺┐∃xP(x)∨∀xQ(x)

⟺∀x┐P(x)∨∀xQ(x)

⟺∀x┐P(x)∨∀yQ(y)

⟺∀x∀y(P(x)→Q(y))

全称量词消去得∀y(P(z)→Q(y))，其中z是论域中任意个体

全称量词消去得P(z)→Q(z)，其中z是论域中任意个体

全称量词引入得∀x(P(x)→Q(x))