命题逻辑与谓词逻辑

🧠 “如果天晴我就去操场”——逻辑的直觉

你说：“如果天晴我就去操场”。 室友说：“天晴了”。 你得出结论：“所以我去操场”。

这是人天生的推理能力——但计算机没有这种直觉。要让计算机对程序的正确性做严密的、没有漏洞的推理——需要把推理过程数学化。

这就是形式逻辑（Formal Logic） 的目的——用精确的符号语言表达”真”和”假”，以及”从一个真陈述怎么推出另一个真陈述”。

🏪 类比：法官断案

法官判案不是”觉得你有罪”——必须有证据链：已知事实A、法律规则B → 结论C。每一步都要有理有据。

形式逻辑就是”数学化的法官推理”——每个推理步骤有严格规则，没有任何”感觉”和”大概”。

---

📐 命题逻辑——“原子”的推理单位

命题逻辑是最基础的逻辑系统——研究命题（可以判断真假的陈述）之间的逻辑关系。

符号	读法	含义	真值表
¬P	非 P	P 不成立	P假→真, P真→假
P ∧ Q	P 且 Q	P 和 Q 都真	只有真∧真=真
P ∨ Q	P 或 Q	P 或 Q 至少一个真	只有假∨假=假
P → Q	如果 P 则 Q	P 蕴含 Q	假→任何=真
P ↔ Q	P 当且仅当 Q	P 和 Q 同真同假	P=Q时真

# 命题逻辑的推理示例
前提 1：如果下雨(P) → 地湿(Q)     [P → Q]
前提 2：下雨了(P)                   [P]
结论：地湿了(Q)                     [Q]

这就是"肯定前件"（Modus Ponens）——最基础的推理规则

常见推理规则：

肯定前件（Modus Ponens）：  P → Q, P  →  Q
否定后件（Modus Tollens）： P → Q, ¬Q → ¬P
假言三段论：                 P → Q, Q → R → P → R

---

🔬 谓词逻辑——更强大的表达能力

命题逻辑的局限：它只能处理”整个陈述”的真假——不能表达”所有学生都通过了考试”这种涉及”对象”和”范围”的陈述。

谓词逻辑（Predicate Logic） 引入：

• 谓词（Predicate）：带参数的命题——Student(x) 表示”x 是学生”
• 量词（Quantifier）：∀（所有）和 ∃（存在）

命题逻辑：P → "地球是圆的"（一个完整的真假陈述）

谓词逻辑：
Human(x) → "x 是人"（x 满足某种性质）
∀x (Human(x) → Mortal(x)) → "所有人都终有一死"
     ↑     ↑     ↑
   对所有  如果x是人  则 x会死

# 谓词逻辑的推理——经典三段论
# ∀x (Human(x) → Mortal(x))     — 所有人都会死
# Human(苏格拉底)                — 苏格拉底是人
# ∴ Mortal(苏格拉底)             — 所以苏格拉底会死

# 另一个例子
# ∀x (Student(x) → Passed(x))   — 所有学生都通过了
# Student(张三)                   — 张三是学生
# ∴ Passed(张三)                  — 张三通过了

量词的顺序很重要：

∀x ∃y (y > x)  → 对每个 x 存在更大的 y（真——因为整数无限）
∃y ∀x (y > x)  → 存在一个 y 大于所有 x（假——没有最大的数）

---

🧩 形式逻辑在程序验证中的角色

命题逻辑 → 简单的条件判断推理
谓词逻辑 → 表达"所有对象满足某种性质"

这两个系统是所有程序验证技术的逻辑基础——模型检验和程序验证都建立在它们之上。

---

📝 小结

概念	一句话
命题逻辑	真/假 + 与或非蕴含——最基础的推理系统
谓词逻辑	引入谓词(性质) + 量词(∀∃)——表达能力更强
Modus Ponens	如果 P→Q 且 P 为真，则 Q 为真
量词顺序	∀x ∃y 和 ∃y ∀x 含义不同

为什么先学这个？ 逻辑是形式化方法的基础。有了逻辑，才能用模型检验（Model Checking）自动验证系统。