【面向計算機的數理邏輯/軟體理論基礎筆記】一階謂詞邏輯系統的補充知識點：代換、自然演繹規則

沖突

• 公式樣例：類似于 r ∧ ¬ r r\wedge \neg r r∧¬r或者 ¬ p ∧ p \neg p\wedge p ¬p∧p這樣的表達式
• 符号： ⊥ \perp ⊥
• 不沖突：符号 ⊤ \top ⊤，與沖突的關系： ⊥ : = ¬ ⊤ \perp := \neg \top ⊥:=¬⊤

等價

如果 p ⊣ q , p ⊢ q p \dashv q,p \vdash q p⊣q,p⊢q，則 p ⊣ ⊢ p p \dashv \vdash p p⊣⊢p

代換

• 定義：給定變元 x x x、項 t t t、公式 A ( x ) A(x) A(x)，定義 A ( t ) A(t) A(t)為用 t t t代替 A A A中的變量 x x x的每個自由出現而得到的公式。

有些教材用 ϕ \phi ϕ表示公式，用 ϕ [ t / x ] \phi[t/x] ϕ[t/x]表示用 t t t代換 A A A中的變量 x x x

自然演繹規則

• 相等的證明規則
  • i i i規則
    • 定義：任何項 t t t必然和它本身相等

    • 公式表示：

      i = t = t i = \frac{}{t=t} i=t=t​

    分母為空表示這個規則不需要任何前提條件，對于不需要前提條件的規則，我們稱之為公理。

  • e e e規則
    • 範例：

      • 因為 y ∗ ( w + 2 ) y * (w +2) y∗(w+2)等于 y ∗ w + y ∗ 2 y * w + y * 2 y∗w+y∗2

        是以由 z ⩾ y ∗ ( w + 2 ) z \geqslant y * ( w + 2 ) z⩾y∗(w+2)

        可以推出 z ⩾ y ∗ w + y ∗ 2 z \geqslant y * w + y * 2 z⩾y∗w+y∗2

    • 公式定義

      e = t 1 = t 2 ∧ A ( t 1 ) A ( t 2 ) e = \frac{t_1=t_2\wedge A(t_1)}{A(t_2)} e=A(t2​)t1​=t2​∧A(t1​)​

    表示當 t 1 = t 2 t_1=t_2 t1​=t2​和 t 1 t_1 t1​代換公式 A A A中 x x x的結果可以得到 t 2 t_2 t2​代換公式 A A A中 x x x的。

  • 基本的證明過程：

    ( x + 1 ) = ( 1 + x ) 前 提 ( x + 1 > 1 ) → ( x + 1 > 0 ) 前 提 ( 1 + x > 1 ) → ( 1 + x > 0 ) = e 1 , 2 \begin{aligned} &(x+1)=(1+x)&& 前提 \\ &(x+1>1)\to (x+1>0)&& 前提 \\ &(1+x>1)\to (1+x>0)&& =e1,2 \\ \end{aligned} ​(x+1)=(1+x)(x+1>1)→(x+1>0)(1+x>1)→(1+x>0)​​前提前提=e1,2​

    • 由上述證明過程确定了下列矢列的有效性：
      • x + 1 = 1 + x x+1 = 1+x x+1=1+x
      • ( x + 1 > 1 ) → ( x + 1 > 0 ) ⊢ ( 1 + x > 1 ) → ( 1 + x > 0 ) > 0 (x+1>1)\to (x+1>0)\vdash (1+x>1)\to (1+x>0)>0 (x+1>1)→(x+1>0)⊢(1+x>1)→(1+x>0)>0
    • 在此證明情況下，我們假設 t 1 t_1 t1​是 ( x + 1 ) (x+1) (x+1)， t 2 t_2 t2​是 ( 1 + x ) (1+x) (1+x)， A ( x ) A(x) A(x)是 ( x > 1 ) → ( x > 0 ) (x>1)\to(x>0) (x>1)→(x>0)。我們使用了規則 = e =e =e，消去了 t 1 = t 2 t_1=t_2 t1​=t2​這個等式，然後将 t 1 t_1 t1​或 t 2 t_2 t2​代換公式 A A A中 x x x後即可得到證明結論
• 全稱量詞的證明規則：
  • ∀ x   e \forall x \ e ∀x e規則：若 ∀ x   A ( x ) \forall x \ A(x) ∀x A(x)是真的，可以将 A ( x ) A(x) A(x)中的 x x x用任何項 t t t去替換（ t t t關于 A ( x ) A(x) A(x)中的 x x x是自由的），并且可以得出 A ( t ) A(t) A(t)也是真的。

    • 公式表示：

      ∀ x   e = ∀ x   A ( x ) A ( t ) \forall x \ e = \frac{\forall x \ A(x)}{A(t)} ∀x e=A(t)∀x A(x)​

• 例題一：
  • 證明： ∀ x ( P ( x ) → Q ( x ) ) , ∀ x P ( x ) ⊢ ∀ x Q ( x ) \forall x (P(x)\to Q(x)),\forall x P(x) \vdash \forall x Q(x) ∀x(P(x)→Q(x)),∀xP(x)⊢∀xQ(x)

  • 答案：

    ( 1 ) ∀ x ( P ( x ) → Q ( x ) ) 前 提 ( 2 ) ∀ x   P ( x ) 前 提 ( 3 ) P ( x 0 ) → Q ( x 0 ) ∀ x   e 1 ( 4 ) P ( x 0 ) ∀ x   e 2 ( 5 ) Q ( x 0 ) → e 3 , 4 ( 6 ) ∀ x Q ( x ) ∀ x   i 3 − 5 \begin{aligned} &(1)\forall x (P(x)\to Q(x))&&前提\\ &(2)\forall x \ P(x)&&前提\\ &(3)P(x_0)\to Q(x_0)&&\forall x \ e_1\\ &(4)P(x_0)&&\forall x \ e_2\\ &(5)Q(x_0)&&\to e_{3,4}\\ &(6)\forall x Q(x)&&\forall x \ i_{3-5}\\ \end{aligned} ​(1)∀x(P(x)→Q(x))(2)∀x P(x)(3)P(x0​)→Q(x0​)(4)P(x0​)(5)Q(x0​)(6)∀xQ(x)​​前提前提∀x e1​∀x e2​→e3,4​∀x i3−5​​

  • 解釋：
    • 題目要求根據前提 ∀ x ( P ( x ) → Q ( x ) ) \forall x (P(x)\to Q(x)) ∀x(P(x)→Q(x))和 ∀ x P ( x ) \forall x P(x) ∀xP(x)推導出結論 ∀ x Q ( x ) \forall x Q(x) ∀xQ(x)，我們的主要思路為通過證明 Q ( x 0 ) Q(x_0) Q(x0​)成立來證明 ∀ x Q ( x ) 成 立 \forall x Q(x)成立 ∀xQ(x)成立，為了證明後者，我們隻需要證明 P ( x 0 ) → Q ( x 0 ) P(x_0)\to Q(x_0) P(x0​)→Q(x0​)和 P ( x 0 ) P(x_0) P(x0​)成立，而他們本身就是兩個前提的執行個體（對項 x 0 x_0 x0​使用 ∀ x   e \forall x \ e ∀x e規則）實作；
    • 我們根據第一個前提 ∀ x ( P ( x ) → Q ( x ) ) \forall x (P(x)\to Q(x)) ∀x(P(x)→Q(x))和規則 ∀ x   e \forall x \ e ∀x e、任意變元 x 0 x_0 x0​可以得到第三個公式 P ( x 0 ) → Q ( x 0 ) P(x_0)\to Q(x_0) P(x0​)→Q(x0​)，表明對于任意一個 x 0 x_0 x0​，都滿足推導公式 P ( x 0 ) → Q ( x 0 ) P(x_0)\to Q(x_0) P(x0​)→Q(x0​)；
    • 再根據第二個前提 ∀ x   P ( x ) \forall x \ P(x) ∀x P(x)和規則 ∀ x   e \forall x \ e ∀x e、任意變元 x 0 x_0 x0​可以得到第四個公式 P ( x 0 ) P(x_0) P(x0​)，表明對于任意一個 x 0 x_0 x0​，都滿足推導公式 P ( x 0 ) P(x_0) P(x0​)；
    • 根據規則 e e e，我們将公式4帶入公式3，可以得到公式5： Q ( x 0 ) Q(x_0) Q(x0​)
• 例題二：
  • 證明： P ( t ) , ∀ x ( P ( x ) → ¬ Q ( x ) ) ⊢ ¬ Q ( t ) P(t),\forall x(P(x)\to \neg Q(x)) \vdash \neg Q(t) P(t),∀x(P(x)→¬Q(x))⊢¬Q(t)

  • 答案：

    ( 1 ) P ( t ) 前 提 ( 2 ) ∀ x ( P ( x ) → ¬ Q ( x ) ) 前 提 ( 3 ) P ( t ) → ¬ Q ( t ) ∀ x   e 2 ( 4 ) ¬ Q ( t ) → e 3 , 1 \begin{aligned} &(1)P(t)&&前提\\ &(2)\forall x (P(x) \to \neg Q(x))&&前提\\ &(3)P(t)\to \neg Q(t)&&\forall x \ e_2\\ &(4)\neg Q(t)&&\to e_{3,1}\\ \end{aligned} ​(1)P(t)(2)∀x(P(x)→¬Q(x))(3)P(t)→¬Q(t)(4)¬Q(t)​​前提前提∀x e2​→e3,1​​

• 存在量詞的證明規則：
  • ∃ x   i \exist x \ i ∃x i規則：隻要對某項 t t t，有 A ( t ) A(t) A(t)，那麼，我們可以推導出 ∃ x   A ( x ) \exist x \ A(x) ∃x A(x)
• 例題三：
  • 證明： ∀ x   A ( x ) ⊢ ∃ x   A ( x ) \forall x \ A(x) \vdash \exist x \ A(x) ∀x A(x)⊢∃x A(x)

  • 答案：

    ( 1 ) ∀ x A ( x ) 前 提 ( 2 ) A ( x ) ∀ x   e 1 ( 3 ) ∃ x   A ( x ) ∃ x   i 2 \begin{aligned} &(1)\forall x A(x)&&前提\\ &(2)A(x)&&\forall x \ e_1\\ &(3) \exist x \ A(x)&&\exist x \ i_2\\ \end{aligned} ​(1)∀xA(x)(2)A(x)(3)∃x A(x)​​前提∀x e1​∃x i2​​

  • 解釋：公式2表示把 x x x看作參數帶入到 A ( x ) A(x) A(x)中，推出 A ( x ) A(x) A(x)成立
• 例題四：
  • 證明： ∀ x ( P ( x ) → Q ( x ) ) , ∃ x   P ( x ) ⊢ ∃ x   Q ( x ) \forall x (P(x)\to Q(x)),\exist x \ P(x) \vdash \exist x \ Q(x) ∀x(P(x)→Q(x)),∃x P(x)⊢∃x Q(x)

  • 答案：

    ( 1 ) ∀ x ( P ( x ) → Q ( x ) ) 前 提 ( 2 ) ∃ x   P ( x ) 前 提 ( 3 ) P ( x 0 ) 假 設 ( 4 ) P ( x 0 ) → Q ( x 0 ) ∀ x   e 1 ( 5 ) Q ( x 0 ) → e 3 , 4 ( 6 ) ∃ x   Q ( x ) ∃ x   i 5 ( 7 ) ∃ x   Q ( x ) ∃ x   e 2 , 3 − 6 \begin{aligned} &(1)\forall x (P(x)\to Q(x))&&前提\\ &(2)\exist x \ P(x)&&前提\\ &(3)P(x_0)&&假設\\ &(4)P(x_0)\to Q(x_0)&&\forall x \ e_1\\ &(5)Q(x_0)&&\to e_{3,4}\\ &(6)\exist x \ Q(x)&&\exist x \ i_5\\ &(7)\exist x \ Q(x)&&\exist x \ e_{2,3-6}\\ \end{aligned} ​(1)∀x(P(x)→Q(x))(2)∃x P(x)(3)P(x0​)(4)P(x0​)→Q(x0​)(5)Q(x0​)(6)∃x Q(x)(7)∃x Q(x)​​前提前提假設∀x e1​→e3,4​∃x i5​∃x e2,3−6​​

• 例題五：
  • 證明： ∀ x ( Q ( x ) → R ( x ) ) , ∃ x ( P ( x ) ∧ Q ( x ) ) ⊢ ∃ x ( P ( x ) ∧ R ( x ) ) \forall x(Q(x)\to R(x)),\exist x (P(x)\wedge Q(x)) \vdash \exist x (P(x)\wedge R(x)) ∀x(Q(x)→R(x)),∃x(P(x)∧Q(x))⊢∃x(P(x)∧R(x))

  • 答案：

    ( 1 ) ∀ x ( Q ( x ) → R ( x ) ) 前 提 ( 2 ) ∃ x ( P ( x ) ∧ Q ( x ) ) 前 提 ( 3 ) P ( x 0 ) ∧ Q ( x 0 ) 假 設 ( 4 ) Q ( x 0 ) → R ( x 0 ) ∀ x   e 1 ( 5 ) Q ( x 0 ) ∧ e 2 , 3 ( 6 ) R ( x 0 ) → e 4 , 5 ( 7 ) P ( x 0 ) ∧ e 1 , 3 ( 8 ) P ( x 0 ) ∧ R ( x 0 ) ∧ i 7 , 6 ( 9 ) ∃ x ( P ( x ) ∧ R ( x ) ) ∃ x   i 8 ( 10 ) ∃ x ( P ( x ) ∧ R ( x ) ) ∃ x   e 2 , 3 − 9 \begin{aligned} &(1)\forall x (Q(x)\to R(x))&&前提\\ &(2)\exist x (P(x)\wedge Q(x))&&前提\\ &(3)P(x_0)\wedge Q(x_0)&&假設\\ &(4)Q(x_0)\to R(x_0)&&\forall x \ e_{1}\\ &(5)Q(x_0)&&\wedge e_{2,3}\\ &(6)R(x_0)&&\to e_{4,5}\\ &(7)P(x_0)&&\wedge e_{1,3}\\ &(8)P(x_0)\wedge R(x_0)&&\wedge i_{7,6}\\ &(9) \exist x (P(x)\wedge R(x))&&\exist x \ i_8\\ &(10) \exist x (P(x)\wedge R(x))&&\exist x \ e_{2,3-9}\\ \end{aligned} ​(1)∀x(Q(x)→R(x))(2)∃x(P(x)∧Q(x))(3)P(x0​)∧Q(x0​)(4)Q(x0​)→R(x0​)(5)Q(x0​)(6)R(x0​)(7)P(x0​)(8)P(x0​)∧R(x0​)(9)∃x(P(x)∧R(x))(10)∃x(P(x)∧R(x))​​前提前提假設∀x e1​∧e2,3​→e4,5​∧e1,3​∧i7,6​∃x i8​∃x e2,3−9​​

• 例題六：
  • 證明： ∃ x   P ( x ) , ∀ x ∀ y ( P ( x ) → Q ( x ) ) ⊢ ∀ y   Q ( y ) \exist x \ P(x),\forall x \forall y(P(x)\to Q(x))\vdash \forall y \ Q(y) ∃x P(x),∀x∀y(P(x)→Q(x))⊢∀y Q(y)

  • 答案：

    ( 1 ) ∃ x P ( x ) 前 提 ( 2 ) ∀ x ∀ y ( P ( x ) → Q ( x ) ) 前 提 ( 3 ) P ( x 0 ) 假 設 ( 4 ) ∀ y ( P ( x 0 ) → Q ( y ) ) ∀ x   e 2 ( 5 ) P ( x 0 ) → Q ( y 0 ) ∀ y   e 4 ( 6 ) Q ( y 0 ) → e 5 , 3 ( 7 ) Q ( y 0 ) ∃ x   e 1 , 3 − 6 ( 8 ) ∀ y   Q ( y ) ∀ y   i 3 − 7 \begin{aligned} &(1)\exist x P(x)&&前提\\ &(2)\forall x \forall y (P(x)\to Q(x))&&前提\\ &(3)P(x_0)&&假設\\ &(4)\forall y (P(x_0)\to Q(y))&&\forall x \ e_{2}\\ &(5)P(x_0)\to Q(y_0)&&\forall y \ e_{4}\\ &(6)Q(y_0)&&\to e_{5,3}\\ &(7)Q(y_0)&&\exist x \ e_{1,3-6}\\ &(8) \forall y \ Q(y)&&\forall y \ i_{3-7}\\ \end{aligned} ​(1)∃xP(x)(2)∀x∀y(P(x)→Q(x))(3)P(x0​)(4)∀y(P(x0​)→Q(y))(5)P(x0​)→Q(y0​)(6)Q(y0​)(7)Q(y0​)(8)∀y Q(y)​​前提前提假設∀x e2​∀y e4​→e5,3​∃x e1,3−6​∀y i3−7​​