谓词逻辑初步

发表于 更新于 Waline： 阅读次数： 本文字数： 862 阅读时长 ≈ 3 分钟

∀n(isEven⁡(n)∧(n>2)→∃m∃k(isPrime⁡(m)∧isPrime⁡(k)∧(n=m+k)))\forall n\biggl(\operatorname{isEven}(n) \land\bigl(n>2\bigr) \rightarrow \exists m \exists k\Bigl(\operatorname{isPrime}(m) \land \operatorname{isPrime}(k) \land\bigl(n=m+k\bigr)\Bigr)\biggr)

哥德巴赫猜想无法用命题逻辑表达，因为 nn 等是变量。

谓词（Predicate）

  • 一元谓词 P(x)P(x)：给定 xx，P(x)P(x) 为真或假。
  • 二元谓词 Q(x,y)Q(x,y)：给定 xx 和 yy，Q(x,y)Q(x,y) 为真或假。
  • ……

原子陈述

  • P(t1,⋯ ,tn)P(t_1, \cdots, t_n)
  • 其中 PP 是 nn 元谓词，t1,⋯ ,tnt_1, \cdots, t_n 是常量、变量或函数取值

逻辑公式（陈述，Formula）

  • 原子陈述是逻辑公式
  • 若 PP 是逻辑公式，xx 是自由变量，则 ∀x P\forall x\, P 和 ∃x P\exists x\, P 是逻辑公式
  • 若 PP 和 QQ 是逻辑公式，则 ¬P, P∧Q, P∨Q, P→Q\lnot P,\, P \land Q,\, P \lor Q,\, P \to Q 是逻辑公式

量词的优先级高于其它逻辑运算符。

  • 约束变元
    • ∀x∃y(y>x)\forall x \exists y (y > x)（即 ∀x(∃y(y>x))\forall x (\exists y (y > x))）中，x,yx, y 是约束变元
  • 自由变元
    • ∃(y>x)∧(x+2>y)\exists (y > x) \land (x + 2 > y) 中，xx 与后面的 yy 是自由变元（后面是自由变元，因为前面的 ∃\exists 作用不到后面的 yy）
  • 量词作用域
    • ∀x∃y(y>x)\forall x \exists y (y > x) 中，∀x\forall x 的作用域是 (∃y(y>x))(\exists y (y > x))，∃y\exists y 的作用域是 (y>x)(y > x)
  • 重命名（对约束变元）
    ∃(y>x)∧(x+2>y)≡∃z(z>x)∧(x+2>y)\exists (y > x) \land (x + 2 > y) \equiv \exists z (z > x) \land (x + 2 > y)

量词：

  • 全称量词 ∀x P(x)\forall x \, P(x)：对所有 xx，P(x)P(x) 为真
  • 存在量词 ∃x P(x)\exists x \, P(x)：存在 xx，使得 P(x)P(x) 为真

多个量词并用：

  • ∀x∀y P(x,y)≡∀y∀x P(x,y)\forall x \forall y \, P(x, y) \equiv \forall y \forall x \, P(x, y)
  • ∃x∃y P(x,y)≡∃y∃x P(x,y)\exists x \exists y \, P(x, y) \equiv \exists y \exists x \, P(x, y)
  • ∀x∃y P(x,y)≢∃y∀x P(x,y)\forall x \exists y \, P(x, y) \not\equiv \exists y \forall x \, P(x, y)

常用逻辑等价式/蕴含式（RR 中不含自由变量 xx）

  • ¬∀x P(x)≡∃x ¬P(x)\lnot \forall x \, P(x) \equiv \exists x \, \lnot P(x)
  • ¬∃x P(x)≡∀x ¬P(x)\lnot \exists x \, P(x) \equiv \forall x \, \lnot P(x)
  • ∀x(P(x)∧Q(x))≡∀x P(x)∧∀x Q(x)\forall x \bigl(P(x) \land Q(x)\bigr) \equiv \forall x \, P(x) \land \forall x \, Q(x)
  • ∃x(P(x)∨Q(x))≡∃x P(x)∨∃x Q(x)\exists x \bigl(P(x) \lor Q(x)\bigr) \equiv \exists x \, P(x) \lor \exists x \, Q(x)
  • ∀x P(x)∨∀x Q(x)⊨∀x(P(x)∨Q(x))\forall x \, P(x) \lor \forall x \, Q(x) \models \forall x \bigl(P(x) \lor Q(x)\bigr)（奇偶）
  • ∃x(P(x)∧Q(x))⊨∃x P(x)∧∃x Q(x)\exists x \bigl(P(x) \land Q(x)\bigr) \models \exists x \, P(x) \land \exists x \, Q(x)
  • ∀x(P(x)∨R)≡(∀x P(x))∨R\forall x \bigl(P(x) \lor R\bigr) \equiv \bigl(\forall x \, P(x)\bigr) \lor R
  • ∃x(P(x)∧R)≡(∃x P(x))∧R\exists x \bigl(P(x) \land R\bigr) \equiv \bigl(\exists x \, P(x)\bigr) \land R
  • ∀x(R→P(x))≡R→∀x P(x)\forall x \bigl(R \to P(x)\bigr) \equiv R \to \forall x \, P(x)（即 ∀x(¬R∨P(x))≡¬R∨(∀x P(x))\forall x \bigl(\lnot R \lor P(x)\bigr) \equiv \lnot R \lor \bigl(\forall x \, P(x)\bigr)）
  • ∃x(R→P(x))≡R→∃x P(x)\exists x \bigl(R \to P(x)\bigr) \equiv R \to \exists x \, P(x)
  • ∀x(P(x)→R)≡(∃x P(x))→R\forall x \bigl(P(x) \to R\bigr) \equiv \bigl(\exists x \, P(x)\bigr) \to R
  • ∃x(P(x)→R)≡(∀x P(x))→R\exists x \bigl(P(x) \to R\bigr) \equiv \bigl(\forall x \, P(x)\bigr) \to R（即 ∃x(P(x)→R)≡(∃x¬P(x))∨R≡¬(∀x P(x))∨R\exists x \bigl(P(x) \to R\bigr) \equiv \bigl(\exists x \lnot P(x)\bigr) \lor R \equiv \lnot \bigl(\forall x \, P(x)\bigr) \lor R）

前束范式（Prenex Normal Form）

∀x(x≤0∨∃y(y>0∧x=y2))≡∀x∃y(x≤0∨(y>0∧x=y2))\forall x\left(x \leq 0 \lor \exists y\left(y>0 \land x=y^{2}\right)\right) \equiv \forall x \exists y\left(x \leq 0 \lor\left(y>0 \land x=y^{2}\right)\right)

量词相关自然演绎规则

引入 消去
全称量词 ∀\forall x0⋮φ[x0/x]∀x φ  ∀x i. \begin{aligned} \boxed{\begin{aligned} &\kern{1.2em}x_0\\ &\kern{1.6em}\vdots\\ &\varphi[x_0 / x] \end{aligned}}\\ \hline \forall x \,\varphi \kern{1em} \end{aligned} \; \nobreak \raisebox{-2.4em}{\(\forall x \, \nobreak \mathrm{i.}\)} ∀x φφ[t/x]  ∀x e. \begin{aligned} \forall x \,\varphi \hspace{0.25em}\\ \hline \varphi[t / x] \end{aligned} \; \nobreak \forall x \, \nobreak \mathrm{e.}
存在量词 ∃\exists φ[t/x]∃x φ ∃x i. \begin{aligned} \varphi[t / x] \\ \hline \exists x \,\varphi \kern{0.25em} \end{aligned} \, \nobreak \exists x \, \nobreak \mathrm{i.} ∃x φx0φ[x0/x]⋮χχ  ∃x e. \begin{aligned} \exists x \,\varphi\quad\boxed{\begin{aligned} &x_0\quad \varphi[x_0 / x] \\ &\kern{2.7em}\vdots \\ &\kern{2.45em}\chi \end{aligned}} \\ \hline \chi \kern{3.7em} \end{aligned} \; \nobreak \raisebox{-2.25em}{\(\exists x \, \nobreak \mathrm{e.}\)}