Knowledge
谓词逻辑知识点
用于复习量词、解释、自由变元、前束范式和 Skolem 范式。
全称量词与存在量词
∀xP(x) 表示论域中所有对象都满足 P；∃xP(x) 表示至少存在一个对象满足 P。
重要公式
- ∃x∀yP(x,y) => ∀y∃xP(x,y)
- ∀xP(x) => ∃xP(x)（默认非空论域）
常见考法
判断量词公式真值、比较量词顺序变化后的公式强弱。
复习提示
- 先确定论域，再逐层读量词。
易错提醒
∀y∃x 与 ∃x∀y 通常不等价，后者要求同一个 x 适用于所有 y。
自由变元与约束变元
变量的一次出现若落在相应量词辖域内，就是约束出现；否则是自由出现。
常见考法
判断变量是否自由、公式是否为命题、量词辖域如何影响公式含义。
复习提示
- 判断时看变量的每一次出现，而不是只看变量名。
易错提醒
同一个变量符号在同一公式中可能既有自由出现，也有约束出现。
前束范式与 Skolem 范式
前束范式把量词移到公式前部；Skolem 化用新的常量或函数消去存在量词。
重要公式
- ∃xP(x) 可 Skolem 化为 P(a)
- ∀x∃yP(x,y) 可 Skolem 化为 ∀xP(x,f(x))
常见考法
求 Skolem 范式，判断 Skolem 范式与原公式的关系。
复习提示
- 存在量词前面有多少全称变元，Skolem 函数就依赖这些变元。
易错提醒
Skolem 范式保持可满足性，但一般不保持逻辑等价性。