【面向計算機的數理邏輯/軟體理論基礎筆記】一階謂詞邏輯系統中一階語言的符号、項、公式、變元

一階語言 L \mathcal{L} L的符号

• 變元符号（變量符号）
  • 格式： x 1 , x 2 , . . . x_{1},x_{2},... x1​,x2​,...
  • 含義：可以看作程式中的變量，或者表示每天的平均溫度
• 謂詞符号
  • 格式：
    • A 1 1 , A 2 1 , . . . A_{1}^{1},A_{2}^{1},... A11​,A21​,...
    • A 1 2 , A 2 2 , . . . A_{1}^{2},A_{2}^{2},... A12​,A22​,...
    • …
    • A 1 n , A 2 n , . . . A_{1}^{n},A_{2}^{n},... A1n​,A2n​,...
  • 含義：謂詞符号表示進行判斷，結果為真或假，可以對一個變元進行判斷，比如判斷 x 1 x_1 x1​的值是否為零，可以用 A 1 1 ( x 1 ) A_1^1(x_1) A11​(x1​)表示；也可以對多個變元判斷，比如判斷 x 1 + x 2 x_1+x_2 x1​+x2​是否大于 x 3 x_3 x3​，可以用 A 2 1 ( x 1 , x 2 , x 3 ) A_2^1(x_1,x_2,x_3) A21​(x1​,x2​,x3​)表示。
  • 謂詞符号集用 p p p表示
• 函數符号
  • 格式：
    • f 1 1 , f 2 1 , . . . f_{1}^{1},f_{2}^{1},... f11​,f21​,...
    • f 1 2 , f 2 2 , . . . f_{1}^{2},f_{2}^{2},... f12​,f22​,...
    • …
    • f 1 n , f 2 n , . . . f_{1}^{n},f_{2}^{n},... f1n​,f2n​,...
  • 含義：函數符号表示對數值進行處理，比如對 x 1 x_1 x1​加一，可以用 f 1 1 ( x 1 ) f_1^1(x_1) f11​(x1​)表示；
  • 函數符号集用 F \mathcal{F} F表示
• 個體常元符号（常值符号）：
  • 格式： a 1 , a 2 , . . . a_{1},a_{2},... a1​,a2​,...
  • 含義：個體常元符号可以視為沒有任何變元的函數符号，可以看作程式中的常量，或者表示天空的顔色是藍色等含有
  • 常元符号集用 C C C表示
  • 因為常元可以看作0元函數，是以常元也叫零元函數
• 連接配接符： ¬ ∨ ∧ → \neg \vee \wedge \to ¬∨∧→
• 量詞符： ∀ , ∃ \forall,\exists ∀,∃

  ( ∃ x i ) A (\exist x_i)A (∃xi​)A等價于 ¬ ( ∀ x i ) ¬ A \neg(\forall x_i)\neg A ¬(∀xi​)¬A

• 輔助符： ) , ( ),( ),(
• 例題一：
  • 假設有一階自然數語言 L n \mathcal{L}_n Ln​：
    • 變元符： x 1 , x 2 , . . . x_{1},x_{2},... x1​,x2​,...表示自然數變元
    • 個體常元符号： a 1 a_{1} a1​表示自然數0
    • 謂詞符号：
      • A 1 1 A_{1}^{1} A11​ 表示非零判斷
      • A 1 2 A_{1}^{2} A12​ 表示相等判斷
      • A 1 1 A_{1}^{1} A11​ 表示小于等于判斷
      • A 1 1 A_{1}^{1} A11​ 表示大于等于判斷
    • 函數符：
      • f 1 1 f_{1}^{1} f11​ 表示後繼函數，比如 x 1 x_{1} x1​的後繼函數是 x 1 + 1 x_{1}+1 x1​+1
      • f 1 2 f_{1}^{2} f12​ 表示加法函數
      • f 2 2 f_{2}^{2} f22​ 表示乘法函數
  • 問題
    • 問題1： A 1 1 ( f 1 1 ( x 1 ) ) A_{1}^{1}(f_{1}^{1}(x_1)) A11​(f11​(x1​))的含義是什麼？
    • 問題2： ∀ x ∃ y ( A 1 2 ( f 1 1 ( x ) , y ) ) \forall x\exist y(A_{1}^{2}(f_{1}^{1}(x),y)) ∀x∃y(A12​(f11​(x),y))的含義是什麼？
  • 答案：
    • 問題1答案：自然數 x 1 x_1 x1​的後繼不為 0，即 x 1 + 1 ≠ 0 x_{1}+1\neq 0 x1​+1​=0
    • 問題2答案：任給自然數 x x x, 存在自然數 y y y, 使得 x + 1 = y x + 1 = y x+1=y

項

• L \mathcal{L} L中的項（用符号 t t t表示）由變元、個體常元和函數符構成：
  • 每個變元、個體常元都是項；
  • 設 f i n f_i^n fin​是 L \mathcal{L} L的 n n n元函數符号， t 1 , t 2 , . . . , t n t_{1},t_{2},...,t_{n} t1​,t2​,...,tn​是項，則 f i n ( t 1 , t 2 , . . . , t n ) f_i^n(t_{1},t_{2},...,t_{n}) fin​(t1​,t2​,...,tn​)是項；

  • L \mathcal{L} L中的項均是由上面兩種方式組成，由Backus Naur可以寫成：

    t : : = a ∣ x ∣ f i n ( t 1 , t 2 , . . . , t n ) t ::= a | x | f_i^n(t_{1},t_{2},...,t_{n}) t::=a∣x∣fin​(t1​,t2​,...,tn​)

    其中 x x x取遍每一個變元的集合 v a r var var， a a a取遍 F \mathcal{F} F中的零元函數符号， f f f取遍 F \mathcal{F} F中的元 n > 0 n>0 n>0的符号

  • : : = ::= ::=是“被定義為”的意思
  • 用符号 T L \mathcal{T}_{\mathcal{L}} TL​表示一階語言 L \mathcal{L} L的全體項之集

• 閉項：不含變元的項。
  • 範例：一階自然數語言 L N ： f 1 1 ( a ) , f 1 2 ( f 1 1 ( a ) , a ) , f 2 2 ( f 1 1 ( x 1 ) , f 1 2 ( x 2 , x 3 ) ) \mathcal{L}_{\mathcal{N}}：f_1^1(a),f_1^2(f_1^1(a),a),f_2^2(f_1^1(x_1),f_1^2(x_2,x_3)) LN​：f11​(a),f12​(f11​(a),a),f22​(f11​(x1​),f12​(x2​,x3​))都是項，而 f 1 1 ( a ) , f 1 2 ( f 1 1 ( a ) , a ) f_1^1(a),f_1^2(f_1^1(a),a) f11​(a),f12​(f11​(a),a)不含變元，稱為閉項。

項通常表示對象，可以作為句子的主語，也因為沒有謂詞，不能表示為命題

一階語言 L \mathcal{L} L的公式

• 定義：
  • 若 P ∈ P P \in P P∈P是 n ⩾ 1 n \geqslant 1 n⩾1元的謂詞符号， t 1 , t 2 , . . . , t n t_{1},t_{2},...,t_{n} t1​,t2​,...,tn​是 F \mathcal{F} F上的項，則 P ( t 1 , t 2 , . . . , t n ) P(t_{1},t_{2},...,t_{n}) P(t1​,t2​,...,tn​)是公式；
  • 若 ϕ \phi ϕ是公式，則 ( ¬ ϕ ) (\neg \phi) (¬ϕ)也是公式；
  • 若 ϕ \phi ϕ和 ψ \psi ψ是公式，則 ϕ ∨ ψ , ϕ ∧ ψ , ϕ → ψ \phi \vee \psi,\phi \wedge \psi,\phi \to \psi ϕ∨ψ,ϕ∧ψ,ϕ→ψ也是公式；
  • 若 ϕ \phi ϕ是公式， x x x是變元，則 ( ∀ x   ϕ ) (\forall x \ \phi) (∀x ϕ)和 ( ∃ x   ψ ) (\exist x \ \psi) (∃x ψ)也是公式；
• L \mathcal{L} L的公式分為兩種：
  • 原子公式（又叫做沒有子公式的公式）：
    • 定義：設 A n A_n An​是 n n n元謂詞， t 1 , t 2 , . . . , t n t_{1},t_{2},...,t_{n} t1​,t2​,...,tn​是項， A i n ( t 1 , t 2 , . . . , t n ) A_i^n(t_{1},t_{2},...,t_{n}) Ain​(t1​,t2​,...,tn​)稱為原子公式。
    • 範例： L N ： A 1 1 ( f 1 1 ( x 1 ) , a ) , A 2 2 ( f 1 1 ( x 1 ) , f 1 2 ( x 2 , x 3 ) ) \mathcal{L}_{\mathcal{N}}：A_1^1(f_1^1(x_1),a),A_2^2(f_1^1(x_1),f_1^2(x_2,x_3)) LN​：A11​(f11​(x1​),a),A22​(f11​(x1​),f12​(x2​,x3​))
  • 合式公式（又稱謂詞公式）：

    • 定義：（由BNF範式給出如下定義）

      A : : = 原 子 公 式 ∣ ¬ A ∣ A ∨ A ∣ A ∧ A ∣ A → A ∣ ( ∀ x i ) A ∣ ( ∃ x i ) A A ::= 原子公式 | \neg A | A \vee A | A \wedge A | A \to A | (\forall x_i)A | (\exist x_i)A A::=原子公式∣¬A∣A∨A∣A∧A∣A→A∣(∀xi​)A∣(∃xi​)A

      因為 ( ∃ x i ) A (\exist x_i)A (∃xi​)A可以簡寫為 ¬ ( ∀ x i ) ¬ A \neg (\forall x_i)\neg A ¬(∀xi​)¬A，是以 L \mathcal{L} L公式可以簡寫為：

      A : : = 原 子 公 式 ∣ ¬ A ∣ A → A ∣ ( ∀ x i ) A A ::= 原子公式 | \neg A | A \to A | (\forall x_i)A A::=原子公式∣¬A∣A→A∣(∀xi​)A

    • 範例： ( ∀ x 1 ) ¬ A 1 2 ( f 1 1 ( x 1 ) , f 2 2 ( x 1 , x 2 ) ) , ( ∀ x 1 ) ( ¬ A 2 1 ( x 1 , a ) → ( ∃ x 2 ) A 2 1 ( x 1 , f 1 1 ( x 2 ) ) ) (\forall x_1)\neg A_1^2(f_1^1(x_1),f_2^2(x_1,x_2)), (\forall x_1)(\neg A_2^1(x_1, a) \to (\exist x_2)A_2^1(x_1, f_1^1 (x_2))) (∀x1​)¬A12​(f11​(x1​),f22​(x1​,x2​)),(∀x1​)(¬A21​(x1​,a)→(∃x2​)A21​(x1​,f11​(x2​)))

  • 用 F ( L ) \mathcal{F}({\mathcal{L}}) F(L)表示全體公式集，包含所有可能的公式。以後講到的很多定理中經常用到，某一個公式 A A A滿足 A ∈ F ( L ) A \in \mathcal{F}({\mathcal{L}}) A∈F(L)，表示 A A A可以是任何一個公式，再由此推出其他定理。
  • 任何原子公式都是合式公式。

• 符号優先級約定：
  • ¬ , ∀ y , ∃ y \neg,\forall y,\exist y ¬,∀y,∃y優先級最高
  • 其次是 ∨ , ∧ \vee,\wedge ∨,∧
  • 然後是右結合 → \to →
• 範例：
  • 将下面的語言翻譯成謂詞邏輯公式：我父親的每個兒子都是我的兄弟。
  • 當我們将"父親"看作一個謂詞符号時：
    • 選擇常量 m m m表示為"我"，選擇謂詞集 { S , F , B } \{S,F,B\} {S,F,B}，其中， S ( x , y ) : x S(x,y):x S(x,y):x是 y y y的兒子， F ( x , y ) : x F(x,y):x F(x,y):x是 y y y的兄弟， B ( x , y ) : x B(x,y):x B(x,y):x是 y y y的父親
    • 謂詞邏輯公式為： ∀ x ∀ y ( F ( x , m ) ∨ S ( y , x ) → B ( y , m ) ) \forall x \forall y (F(x,m)\vee S(y,x)\to B(y,m)) ∀x∀y(F(x,m)∨S(y,x)→B(y,m))
    • 公式含義：對所有 x x x和 y y y，若 x x x是 m m m的父親， y y y是 x x x的兒子，則 y y y是 m m m的兄弟
  • 當我們将"父親"看作一個函數符号時：
    • m 、 S 、 B m、S、B m、S、B與上面保持一緻，用 f f f表示一個變元的函數，傳回值是該變元的父親，此時，因為父親存在且唯一，是以 f f f确實是要給函數，而不僅僅是一個關系
    • 謂詞邏輯公式為： ∀ x ( S ( x , f ( m ) ) → B ( x , m ) ) \forall x (S(x,f(m)) \to B(x,m)) ∀x(S(x,f(m))→B(x,m))
    • 公式含義：對所有的 x x x，若 x x x是 m m m的父親的兒子，則 x x x是 m m m的兄弟

限制變元與自由變元

• 定義：公式中出現 ( ∀ x i ) A (\forall x_i)A (∀xi​)A或者 ( ∃ x i ) A (\exist x_i)A (∃xi​)A時， A A A叫做 ∀ x i \forall x_i ∀xi​或者 ∃ x i \exist x_i ∃xi​的轄域, 此時 A A A中的變元 x i x_i xi​稱為 A A A的限制變元，不是限制變元的變元稱為自由變元。
• 例題二：
  • 問題：
    • 問題1： L N ： ( ∀ x 1 ) ¬ A 1 2 ( f 1 1 ( x 1 ) , f 2 2 ( x 1 , x 2 ) ) \mathcal{L}_{\mathcal{N}}：(\forall x_1)\neg A_1^2(f_1^1(x_1),f_2^2(x_1,x_2)) LN​：(∀x1​)¬A12​(f11​(x1​),f22​(x1​,x2​))，則公式中，有哪些變元以及他們出現的次數？
    • 問題2： L N ： A 1 2 ( x 1 , a ) ∧ ( ∃ x 1 ) A 1 1 ( f 1 1 ( x 1 ) , a ) \mathcal{L}_{\mathcal{N}}：A_1^2(x_1,a) \wedge (\exist x_1) A_1^1(f_1^1(x_1),a) LN​：A12​(x1​,a)∧(∃x1​)A11​(f11​(x1​),a)公式中， x 1 x_1 x1​每一次出現時，是什麼變元？
  • 答案
    • 問題1答案： x 1 x_1 x1​是限制變元，限制出現3次； x 2 x_2 x2​是自由變元，出現1次。
    • 問題2答案： x 1 x_1 x1​出現3次，第1次是自由變元，後2次是限制變元。
• 項的自由性
  • 定義：若 t t t對 A A A中的 x i x_i xi​的每一個自由出現代入都不會使得 t t t中的變元失去自由性，則項 t t t稱為對公式 A ( x i ) A(x_i) A(xi​)的自由變元 x i x_i xi​是自由的。
  • 例如：公式 ( ∀ x 1 ) ( ∀ x 2 ) ( A 2 1 ( x 1 , x 2 ) → A 1 1 ( x 2 ) ) (\forall x_1)(\forall x_2)(A_2^1(x_1, x_2) → A_1^1(x_2)) (∀x1​)(∀x2​)(A21​(x1​,x2​)→A11​(x2​))中無自由變元，對于任何項 t t t（比如 t = f 2 1 ( x 1 , x 2 ) , t ′ = f 2 3 ( x 1 ) t=f_2^1(x_1,x_2),t'=f_2^3(x_1) t=f21​(x1​,x2​),t′=f23​(x1​)）關于此公式中的 x 1 , x 2 x_1, x_2 x1​,x2​都是自由的，這就叫做項的自由性。
  • 例題三：
    • 問題：
      • 公式 ( ∀ x 1 ) ( A 1 3 ( x 1 , x 2 , x 3 ) → A 2 3 ( x 1 , x 2 , x 3 ) ) (\forall x_1)(A_1^3(x_1, x_2, x_3) \to A_2^3(x_1, x_2, x_3)) (∀x1​)(A13​(x1​,x2​,x3​)→A23​(x1​,x2​,x3​))中
        • （1） t 1 = f 1 2 ( x 1 , x 2 ) t_1= f_1^2(x_1,x_2) t1​=f12​(x1​,x2​)，項 t 1 t_1 t1​對 x 2 x_2 x2​是否是自由的？
        • （2） t 2 = f 1 2 ( x 1 , x 2 ) t_2 = f_1^2(x_1,x_2) t2​=f12​(x1​,x2​)，項 t 2 t_2 t2​對 x 3 x_3 x3​是否是自由的？
        • （3） t 3 = f 2 2 ( x 1 ) t_3 = f_2^2(x_1) t3​=f22​(x1​)，項 t 3 t_3 t3​對 x 1 x_1 x1​是否是自由的？
        • （4） t 4 = f 2 1 ( x 2 ) t_4 = f_2^1(x_2) t4​=f21​(x2​)，項 t 4 t_4 t4​對 x 2 x_2 x2​是否是自由的？
        • （5） t 5 = f 1 1 ( x 1 ) t_5 = f_1^1(x_1) t5​=f11​(x1​)，項 t 5 t_5 t5​對 x 2 x_2 x2​是否是自由的？
    • 答案：
      • 公式内具有自由變元 x 2 , x 3 x_2,x_3 x2​,x3​，限制變元 x 3 x_3 x3​
        • （1）若用項 t 1 t_1 t1​代入 x 2 x_2 x2​會得到如下的公式， ( ∀ x 1 ) ( A 1 3 ( x 1 , f 1 2 ( x 1 , x 2 ) , x 3 ) → A 2 3 ( x 1 , f 1 2 ( x 1 , x 2 ) , x 3 ) ) (\forall x_1)(A_1^3(x_1,f_1^2(x_1,x_2), x_3) \to A_2^3(x_1, f_1^2(x_1,x_2), x_3)) (∀x1​)(A13​(x1​,f12​(x1​,x2​),x3​)→A23​(x1​,f12​(x1​,x2​),x3​))，導緻公式原 x 2 x_2 x2​的位置産生了新的限制 x 1 x_1 x1​，是以項 t 1 t_1 t1​對 x 2 x_2 x2​是不自由的。
        • （2）若用項 t 2 t_2 t2​代入 x 3 x_3 x3​會得到如下的公式， ( ∀ x 1 ) ( x 1 , x 2 , f 1 2 ( x 1 , x 2 ) ) → A 2 3 ( x 1 , x 2 , f 1 2 ( x 1 , x 2 ) ) ) (\forall x_1)(x_1,x_2, f_1^2(x_1,x_2)) \to A_2^3(x_1,x_2, f_1^2(x_1,x_2))) (∀x1​)(x1​,x2​,f12​(x1​,x2​))→A23​(x1​,x2​,f12​(x1​,x2​)))，導緻公式原 x 3 x_3 x3​的位置産生了新的限制 x 1 x_1 x1​，是以項 t 2 t_2 t2​對 x 3 x_3 x3​是不自由的。
        • （3）若用項 t 3 t_3 t3​代入 x 1 x_1 x1​會得到如下的公式， ( ∀ x 1 ) ( A 1 3 ( f 1 2 ( x 1 ) , x 2 , x 3 ) → A 2 3 ( f 1 2 ( x 1 ) , x 2 , x 3 ) ) (\forall x_1)(A_1^3(f_1^2(x_1), x_2, x_3) \to A_2^3(f_1^2(x_1), x_2, x_3)) (∀x1​)(A13​(f12​(x1​),x2​,x3​)→A23​(f12​(x1​),x2​,x3​))，在公式原 x 1 x_1 x1​的位置上并沒有産生新的限制，是以 t 3 t_3 t3​對 x 1 x_1 x1​是自由的。
        • （4）若用項 t 4 t_4 t4​代入 x 2 x_2 x2​會得到如下的公式， ( ∀ x 1 ) ( A 1 3 ( x 1 , f 2 1 ( x 2 ) , x 3 ) → A 2 3 ( x 1 , f 2 1 ( x 2 ) , x 3 ) ) (\forall x_1)(A_1^3(x_1, f_2^1(x_2), x_3) \to A_2^3(x_1, f_2^1(x_2), x_3)) (∀x1​)(A13​(x1​,f21​(x2​),x3​)→A23​(x1​,f21​(x2​),x3​))，在公式原 x 2 x_2 x2​的位置上并沒有産生新的限制，是以 t 4 t_4 t4​對 x 2 x_2 x2​是自由的。
        • （5）若用項 t 5 t_5 t5​代入 x 2 x_2 x2​會得到如下的公式， ( ∀ x 1 ) ( A 1 3 ( x 1 , f 1 1 ( x 1 ) , x 3 ) → A 2 3 ( x 1 , f 1 1 ( x 1 ) , x 3 ) ) (\forall x_1)(A_1^3(x_1, f_1^1(x_1), x_3) \to A_2^3(x_1,f_1^1(x_1), x_3)) (∀x1​)(A13​(x1​,f11​(x1​),x3​)→A23​(x1​,f11​(x1​),x3​))，導緻公式原 x 2 x_2 x2​的位置産生了新的限制 x 1 x_1 x1​，是以項 t 5 t_5 t5​對 x 1 x_1 x1​是不自由的。