前束范式流水线 + Skolem 化 · ¬(∀x∃y Q(x,y) → ∀x R(x))

🧳 把它想成一次搬家整理：拆家具（消 →）→ 给每件东西贴"不"字（¬ 内移）→ 同名箱子改名 → 量词统统搬到门口排队（前束范式）；最后把"存在箱"换成具体物件（Skolem 化）。前 5 步逻辑等值 =，Skolem 化后只保可满足性 ⇝。

¬( ∀x∃y Q(x,y) → ∀x R(x) ) 🏠 起点含 →、外层 ¬、量词内嵌

¬( ¬∀x∃y Q(x,y) ∨ ∀x R(x) ) 🔨 消去 →A→B ≡ ¬A∨B

∀x∃y Q(x,y) ∧ ¬∀x R(x) 🏷️ ¬ 内移德摩根 ¬(A∨B)≡¬A∧¬B；¬¬A≡A

∀x∃y Q(x,y) ∧ ∃x ¬R(x) 🏷️ 量词否定¬∀x P ≡ ∃x ¬P

∀x∃y Q(x,y) ∧ ∃z ¬R(z) 📦 改名第二个 x → z，避免前移时被捕获

∃z ∀x ∃y ( Q(x,y) ∧ ¬R(z) ) ✔ 前束范式 PNF 🚪 量词前移辖域扩张：首标 + 母式

⇝
可满足

∀x ∃y ( Q(x,y) ∧ ¬R(a) ) 🎁 Skolem ①∃z 左边无 ∀ → 换 Skolem 常元 a

⇝
可满足

∀x ( Q(x, f(x)) ∧ ¬R(a) ) ✔ Skolem 范式 ⚙️ Skolem ②∃y 左边有 ∀x → 换 Skolem 函数 f(x)

🧳 记住：量词全部搬到门口排队 ＝ 前束范式 PNF（仍等值 =）；再把每个 ∃ 换成常元 / 函数——看它左边有没有 ∀——＝ Skolem 化（只保可满足 ⇝）。

本步改动首标(量词前缀) Skolem 常元 / 函数 = 保逻辑等值 ⇝ 仅保可满足性