第七课：谓词逻辑、FC、ND¶
Page 2 — 量词复习¶
- 量词的辖域：量词所作用的谓词或复合谓词表达式
- ∀xP(x)和∃xP(x)对一元谓词都是命题
- 有限个体域：∀等价于∧，∃等价于∨
Page 3 — 谓词公式定义¶
- 原子公式：谓词填式、命题常元（零元谓词）
- 若A,B是公式，x为任一变元，则¬A、A→B、∀xA、∃xA都是公式
- 注意：∀xA中A可以不包含x，此时∀xA ≡ A（多余量词可去掉）
Page 4 — 谓词公式成为命题的条件¶
需同时满足： 1. 给定个体域 2. 所有谓词有明确意义（解释） 3. 所有自由变元取定个体
例：个体域为实数域，E(x,y)表示x=y，L(x,y)表示x<y - ∀xL(0,x²+1) 为真（0小于任何实数的平方加1） - ∃xE(x²+x+1,0) 为假（x²+x+1=0在实数域无解） - 若个体域换成复数域，真值会变！
Page 5 — 语句形式化例子¶
- "有人勇敢，但不是所有人都勇敢" → ∃xBrave(x) ∧ ¬∀xBrave(x)
- "勇敢者未必是成功者" → ¬∀x(Brave(x)→Success(x)) ≡ ∃x(Brave(x)∧¬Success(x))
- "君子坦荡荡，小人常戚戚" → ∀x(P(x)→Q(x)) ∧ ∀x(R(x)→S(x))
Page 7-8 — 四个层次的永真¶
- 在自由变元的某个取值下为真
- 在给定解释I下，自由变元任何取值都为真
- 在给定个体域D上，每个解释I下都为真（D上永真）
- 在任何个体域D、任何解释I下都为真（永真） - 可满足式：存在某个个体域、解释和变元取值使其为真
Page 9 — 谓词公式的逻辑等价与蕴涵¶
- A≡B：对一切个体域、解释和变元取值，A和B真值相同
- A⊨B：对一切个体域、解释，使A成真的变元取值也使B成真
Page 10 — 谓词演算永真式 ⭐考试重点¶
- 所有命题逻辑的重言式
- 当A不含变元x时：∀xA≡A, ∃xA≡A
- ∀xA(x) ⊨ A(x)（全称消去）
- A(x) ⊨ ∃xA(x)（存在引入）
- 量词否定（⭐必记）：
- ¬∃x¬A(x) ≡ ∀xA(x)
- ¬∀x¬A(x) ≡ ∃xA(x)
- ¬∃xA(x) ≡ ∀x¬A(x)
- ¬∀xA(x) ≡ ∃x¬A(x)
💡 人话：量词否定就像把"所有"和"存在"互换，同时把后面的谓词取反。"不是所有都……"等于"存在一个不……"，"不存在……"等于"所有都不……"。
Page 11 — 量词分配 ⭐考试重点¶
| 条件 | 公式 |
|---|---|
| B不含x | ∀x(A(x)∨B) ≡ ∀xA(x)∨B |
| B不含x | ∀x(A(x)∧B) ≡ ∀xA(x)∧B |
| B不含x | ∃x(A(x)∨B) ≡ ∃xA(x)∨B |
| B不含x | ∃x(A(x)∧B) ≡ ∃xA(x)∧B |
| B含x | ∀x(A(x)∧B(x)) ≡ ∀xA(x)∧∀xB(x) |
| B含x | ∀xA(x)∨∀xB(x) ⊨ ∀x(A(x)∨B(x))（⚠单向） |
| B含x | ∃x(A(x)∧B(x)) ⊨ ∃xA(x)∧∃xB(x)（⚠单向） |
| B含x | ∃x(A(x)∨B(x)) ≡ ∃xA(x)∨∃xB(x) |
💡 人话：量词对∧和∅的分配要注意：∀对∧可以双向，∃对∨可以双向。但∀对∨、∃对∧只是单向蕴涵。
Page 12 — 量词组合与顺序 ⭐考试重点¶
- ∀x∀yA ≡ ∀y∀xA（全称可交换） - ∃x∃yA ≡ ∃y∃xA（存在可交换） - 从∀∀到∃∃是蕴涵链，反过来不成立！当C中无变元x时： - ∀x(C→A(x)) ≡ C→∀xA(x) - ∃x(C→A(x)) ≡ C→∃xA(x)
💡 人话："对所有x存在y……"比"存在x对所有y……"弱。"班上每个人都有同学"不等于"有一个人是全班所有人的同学"。
Page 13-15 — 一阶谓词演算形式系统FC¶
- 比PC多了：个体变元/常元、函数符号、谓词符号、量词∀
- FC的公理：PC的三条公理 + 新公理
- A4: ∀xA(x) → A(t)（t对x可代入）
- A5: ∀x(A→B) → (A→∀xB)（x在A中不自由出现）
- 推理规则：分离规则 + 全称引入规则
Page 22 — PC与FC的不足¶
- 为了追求简洁，只用2个联结词、1个量词、1条推理规则
- 证明过程过于繁复
- 需要更自然的推理系统
Page 23-34 — 自然推理系统ND¶
- ND特点：5个联结词、2个量词、少数公理、更多规则
- ND公理：Γ;A ⊢ A（假设本身可推出）
- ND推理规则：
| 规则 | 形式 | 说明 |
|---|---|---|
| 假设引入 | Γ⊢B ⇒ Γ;A⊢B | 加额外假设仍成立 |
| 假设消除 | Γ;A⊢B且Γ;¬A⊢B ⇒ Γ⊢B | 穷举法 |
| ∨引入 | Γ⊢A ⇒ Γ⊢A∨B | |
| ∨消除 | Γ;A⊢C, Γ;B⊢C, Γ⊢A∨B ⇒ Γ⊢C | 分情况证明 |
| ∧引入 | Γ⊢A, Γ⊢B ⇒ Γ⊢A∧B | |
| ∧消除 | Γ⊢A∧B ⇒ Γ⊢A | |
| →引入 | Γ;A⊢B ⇒ Γ⊢A→B | 演绎定理 |
| →消除 | Γ⊢A→B, Γ⊢A ⇒ Γ⊢B | 分离规则 |
| ¬引入 | Γ;A⊢B, Γ;A⊢¬B ⇒ Γ⊢¬A | |
| ¬消除 | Γ⊢A, Γ⊢¬A ⇒ Γ⊢B | 矛盾可推一切 |
| ∀引入 | Γ⊢A(v) ⇒ Γ⊢∀vA(v) | v在Γ中无自由出现 |
| ∀消除 | Γ⊢∀vA(v) ⇒ Γ⊢A(t) | t对v可代入 |
| ∃引入 | Γ⊢A(t) ⇒ Γ⊢∃vA(v) | |
| ∃消除 | Γ⊢∃vA(v), Γ;A(e)⊢C ⇒ Γ⊢C | 不妨设 |
- ND同时满足：合理性、一致性、完备性
💡 人话：ND就像给数学证明用的"工具箱"——要证A→B就假设A推出B，要证∀xP(x)就对任意x证明P(x)，要证∃xP(x)就找一个具体的例子。