Skip to content

Logic and Structure - 2. 述詞邏輯

Posted on:2024年2月21日 at 下午09:25
Logic and Structure - 2. 述詞邏輯

目錄

Open 目錄

結構

定義 2.1.1 結構 structure

結構是一個序列 A=A,R1,...,Rn,F1,...,Fm,{ciiI}\mathfrak{A} = \langle A, R_1, ..., R_n, F_1, ...,F_m, \{ c_i|i\in I \} \rangle,其中 AA 是非空集合、R1,...,RnR_1, ..., R_nAA 上的關係、F1,...,FmF_1, ..., F_mAA 上的函數、ci(iI)c_i(i \in I)AA 的常元。

定義 2.1.2 相似類型 similarity type

A=A,R1,...,Rn,F1,...,Fm,{ciiI}\mathfrak{A} = \langle A, R_1, ..., R_n, F_1, ...,F_m, \{ c_i|i\in I \} \rangle 的相似類型是一個序列 r1,...,rn;a1,...,am;κ\langle r_1, ..., r_n; a_1, ..., a_m; \kappa \rangle,其中 RiAri,Fj:AajA,κ=IR_i \subset A^{r_i}, F_j: A^{a_j} \rightarrow A, \kappa=| I |

相似類型的語言

以下,我們給定 r1,...,rn;a1,...,am;κ\langle r_1, ..., r_n; a_1, ..., a_m; \kappa \rangle 是一個相似類型,假定 ri0r_i \geq 0aj>0a_j > 0

以下是我們使用的符號:

定義 2.2.1 詞項集

TERMTERM(詞項集)是滿足下述性質的最小集合 XX

  1. 常元 ConstConstciˉX(iI)\bar{c_i}\in X(i\in I)
  2. 變元 VarVarxiX(iN)x_i \in X(i \in \mathbb{N})
  3. 函數封閉性:若 t1,...,taiXt_1, ..., t_{a_i} \in X,則 fi(t1,...,tai)Xf_i(t_1, ..., t_{a_i}) \in X

定義 2.2.2 構句集

FORMFORM(構句集)是滿足下述性質的最小集合 XX

  1. X\bot \in X
  2. ri=0r_i = 0,則 PiXP_i \in X(即 PiP_i 是命題符號);
  3. t1,...,triTERMt_1,...,t_{r_i} \in TERM,則 Pi(t1,...,tri)XP_i(t_1,...,t_{r_i}) \in X
  4. t1,t2TERMt_1, t_2 \in TERM,則 (t1=t2)X(t_1 = t_2) \in X
  5. ϕ,ψX\phi,\psi \in X,則 (ϕψ)X(\phi \square \psi) \in X
  6. ϕX\phi \in X,則 (¬ϕ)X(\neg \phi) \in X
  7. ϕX\phi \in X,則 xiϕ,xiϕX\forall x_i \phi, \exists x_i \phi \in X

定理 2.2.3 歸納法與遞迴性

參考命題邏輯的定理 1.1.31.1.6,不難證明 TERMTERMFORMFORM 都滿足一般與遞迴的歸納法原理。

詞項集的歸納法原理

A(t)A(t) 為詞項的性質。若 A(t)A(t) 對變數或常數 tt 成立,且若對所有函數 ff 都有 A(t1),A(t2),...,A(tn)A(f(t1,...,tn))A(t_1), A(t_2), . . . , A(t_n) \Rightarrow A(f (t_1, . . . , t_n)),則 A(t)A(t) 對所有 tTERMt \in TERM 成立。

構句集的歸納法原理

A(φ)A(φ) 為構句的性質。若

  1. 對原子句 φφA(φ)A(φ) 成立,
  2. A(φ),A(ψ)A(φψ)A(φ),A(ψ)⇒A(φ \land ψ)
  3. A(φ)A(¬φ)A(φ)⇒A(¬φ)
  4. 對所有 iiA(φ)A((xi)φ),A((xi)φ)A(φ)⇒A((∀xi)φ),A((∃xi)φ)

A(φ)A(φ) 對所有 φFORMφ∈FORM 成立。

詞項集的遞迴性

H0:VarConstAH_0: Var \cup Const \rightarrow AH1:AaiAH_1: A^{a_i} \rightarrow A,則存在唯一的函數 H:TERMAH: TERM \rightarrow A 使得:

  1. 對於變元或常元 ttH(t)=H0(t)H(t) = H_0(t)
  2. 對於函數 fif_iH(fi(t1,...,tai))=H1(H(t1),...,H(tai))H(f_i(t_1, ..., t_{a_i})) = H_1(H(t_1), ..., H(t_{a_i}))

構句集的遞迴性

Hat:ATOMAH_{at}: ATOM \rightarrow AH:A2AH_\square : A^2\rightarrow AH¬:AAH_{\neg}: A \rightarrow AH:AAH_{\forall}: A \rightarrow AH:AAH_{\exists}: A \rightarrow A,則存在唯一的函數 H:FORMAH: FORM \rightarrow A 使得:

  1. 對於所有的原子式 ttH(t)=Hat(t)H(t) = H_{at}(t)
  2. H(t1t2)=H(H(t1),H(t2))H(t_1 \square t_2) = H_\square(H(t_1), H(t_2))
  3. H(¬ϕ)=H¬(H(ϕ))H(\neg \phi) = H_{\neg}(H(\phi))
  4. H(xiϕ)=H(H(ϕ))H(\forall x_i \phi) = H_{\forall}(H(\phi))
  5. H(xiϕ)=H(H(ϕ))H(\exists x_i \phi) = H_{\exists}(H(\phi))

定義 2.2.4 自由變元

TERMTERM:

  1. FV(ciˉ)=FV(\bar{c_i}) = \emptyset
  2. FV(xi)={xi}FV(x_i) = \{ x_i \}
  3. FV(fi(t1,...,tai))=FV(t1)...FV(tai)FV(f_i(t_1, ..., t_{a_i})) = FV(t_1) \cup ... \cup FV(t_{a_i})

FORMFORM:

  1. FV()=FV(\bot) = \emptyset
  2. PP 是命題符號,則 FV(P)=FV(P) = \emptyset
  3. FV(t1=t2)=FV(t1)FV(t2)FV(t_1 = t_2) = FV(t_1) \cup FV(t_2)
  4. FV(Pi(t1,...,tri))=FV(t1)...FV(tri)FV(P_i(t_1, ..., t_{r_i})) = FV(t_1) \cup ... \cup FV(t_{r_i})
  5. FV(ϕψ)=FV(ϕ)FV(ψ)FV(\phi \square \psi) = FV(\phi) \cup FV(\psi)
  6. FV(¬ϕ)=FV(ϕ)FV(\neg \phi) = FV(\phi)
  7. FV(xiϕ)=FV(ϕ){xi}FV(\forall x_i \phi) = FV(\phi) \setminus \{ x_i \}
  8. FV(xiϕ)=FV(ϕ){xi}FV(\exists x_i \phi) = FV(\phi) \setminus \{ x_i \}

定義 2.2.5 封閉詞項和封閉構句

  1. FV(t)=FV(t) = \emptyset,則 tt 稱為封閉詞項。封閉詞項集合寫作 TERMcTERM_c
  2. FV(ϕ)=FV(\phi) = \emptyset,則 ϕ\phi 稱為封閉構句或語句。語句集合寫作 SENTSENT
  3. 無量詞的構句稱為開放構句。

定義 2.2.6 拘束變元

TERMTERM:

  1. BV(ciˉ)=BV(\bar{c_i}) = \emptyset
  2. BV(xi)=BV(x_i) = \emptyset
  3. BV(fi(t1,...,tai))=BV(t1)...BV(tai)BV(f_i(t_1, ..., t_{a_i})) = BV(t_1) \cup ... \cup BV(t_{a_i})

FORMFORM:

  1. BV()=BV(\bot) = \emptyset
  2. PP 是命題符號,則 BV(P)=BV(P) = \emptyset
  3. BV(t1=t2)=BV(t1)BV(t2)BV(t_1 = t_2) = BV(t_1) \cup BV(t_2)
  4. BV(Pi(t1,...,tri))=BV(t1)...BV(tri)BV(P_i(t_1, ..., t_{r_i})) = BV(t_1) \cup ... \cup BV(t_{r_i})
  5. BV(ϕψ)=BV(ϕ)BV(ψ)BV(\phi \square \psi) = BV(\phi) \cup BV(\psi)
  6. BV(¬ϕ)=BV(ϕ)BV(\neg \phi) = BV(\phi)
  7. BV(xiϕ)=BV(ϕ){xi}BV(\forall x_i \phi) = BV(\phi) \cup \{ x_i \}
  8. BV(xiϕ)=BV(ϕ){xi}BV(\exists x_i \phi) = BV(\phi) \cup \{ x_i \}

定義 2.2.7 替代

TERMTERM

sstt 是兩個詞項,則 s[t/x]s[t/x] 定義如下:

  1. c[t/x]=cc[t/x] = c
  2. yy 不是 xx,則 y[t/x]=yy[t/x] = y
  3. yy 即是 xx,則 y[t/x]=ty[t/x] = t
  4. (f(t1,...,tai))[t/x]=f(t1[t/x],...,tai[t/x])(f(t_1, ..., t_{a_i}))[t/x] = f(t_1[t/x], ..., t_{a_i}[t/x])

FORMFORM 的詞項替代:

ϕ\phi 是一個構句,tt 是一個詞項,則 ϕ[t/x]\phi[t/x] 定義如下:

  1. [t/x]=\bot[t/x] = \bot
  2. PP 是命題符號,則 P[t/x]=PP[t/x] = P
  3. (t1=t2)[t/x]=t1[t/x]=t2[t/x](t_1 = t_2)[t/x] = t_1[t/x] = t_2[t/x]
  4. (Pi(t1,...,tri))[t/x]=Pi(t1[t/x],...,tri[t/x])(P_i(t_1, ..., t_{r_i}))[t/x] = P_i(t_1[t/x], ..., t_{r_i}[t/x])
  5. (ϕψ)[t/x]=ϕ[t/x]ψ[t/x](\phi \square \psi)[t/x] = \phi[t/x] \square \psi[t/x]
  6. (¬ϕ)[t/x]=¬ϕ[t/x](\neg \phi)[t/x] = \neg \phi[t/x]
  7. yy 不是 xx,則 (yϕ)[t/x]=yϕ[t/x](\forall y \phi)[t/x] = \forall y \phi[t/x]
  8. yy 即是 xx,則 (yϕ)[t/x]=yϕ(\forall y \phi)[t/x] = \forall y \phi
  9. yy 不是 xx,則 (yϕ)[t/x]=yϕ[t/x](\exists y \phi)[t/x] = \exists y \phi[t/x]
  10. yy 即是 xx,則 (yϕ)[t/x]=yϕ(\exists y \phi)[t/x] = \exists y \phi

FORMFORM 的構句替代:

ϕ\phiψ\psi 是兩個構句,則 ϕ[ψ/P]\phi[\psi/ P] 定義如下:

  1. ϕ\phi 即是 PP,則 ϕ[ψ/P]=ψ\phi[\psi/ P] = \psi
  2. ϕ\phi 不是 PP,但 ϕ\phi 是原子語句,則 ϕ[ψ/P]=ϕ\phi[\psi/ P] = \phi
  3. ϕ=ϕ1ϕ2\phi = \phi_1 \square \phi_2,則 ϕ[ψ/P]=ϕ1[ψ/P]ϕ2[ψ/P]\phi[\psi/ P] = \phi_1[\psi/ P] \square \phi_2[\psi/ P]
  4. ϕ=¬ϕ1\phi = \neg \phi_1,則 ϕ[ψ/P]=¬ϕ1[ψ/P]\phi[\psi/ P] = \neg \phi_1[\psi/ P]
  5. ϕ=xiϕ1\phi = \forall x_i \phi_1,則 ϕ[ψ/P]=xiϕ1[ψ/P]\phi[\psi/ P] = \forall x_i \phi_1[\psi/ P]
  6. ϕ=xiϕ1\phi = \exists x_i \phi_1,則 ϕ[ψ/P]=xiϕ1[ψ/P]\phi[\psi/ P] = \exists x_i \phi_1[\psi/ P]

定義 2.2.8 自由詞項

ϕ\phi 中,ttxx 是自由的,代表下述性質之一被滿足:

  1. ϕ\phi 是原子的,
  2. ϕ=ϕ1ϕ2\phi = \phi_1 \square \phi_2,且 ttxxϕ1\phi_1ϕ2\phi_2 中是自由的,
  3. ϕ=¬ϕ1\phi = \neg \phi_1,且 ttxxϕ1\phi_1 中是自由的,
  4. ϕ=yψ\phi = \exists y \psi,且若 xFV(ϕ)x\in FV(\phi),則 y∉FV(t)y \not\in FV(t)ttxxψ\psi 中是自由的。
  5. ϕ=yψ\phi = \forall y \psi,且若 xFV(ϕ)x\in FV(\phi),則 y∉FV(t)y \not\in FV(t)ttxxψ\psi 中是自由的。

定義 4 和 5 比較抽象,但直覺卻很單純:ttxx 是自由的,意味著將 xxtt 替代是安全的,表示,當 tt 取代 xx 出現在 ϕ\phi 中時,yy 不該提供新的量限,自由的必須保持自由的、拘束的必須保持拘束的。理解了這點以後,引理 2.2.9 和 2.2.11 都是非常容易理解的。

引理 2.2.9

ϕ\phi 中,ttxx 是自由的,當且僅當 ϕ[t/x]\phi[t/x] 的變數 tt 未被量詞拘束。

定義 2.2.10 自由構句

σ\sigma 中,ϕ\phiPP 是自由的,代表下述性質之一被滿足:

  1. σ\sigma 是原子的,
  2. σ=σ1σ2\sigma = \sigma_1 \square \sigma_2,且 ϕ\phiPPσ1\sigma_1σ2\sigma_2 中是自由的,
  3. σ=¬σ1\sigma = \neg \sigma_1,且 ϕ\phiPPσ1\sigma_1 中是自由的,
  4. σ=yψ\sigma = \exists y \psi,且若 PPσ\sigma 中出現,則 y∉FV(ϕ)y \not\in FV(\phi)ϕ\phiPPψ\psi 中是自由的。
  5. σ=yψ\sigma = \forall y \psi,且若 PPσ\sigma 中出現,則 y∉FV(ϕ)y \not\in FV(\phi)ϕ\phiPPψ\psi 中是自由的。

引理 2.2.11

σ\sigma 中,ϕ\phiPP 是自由的,當且僅當 ϕ\phi 的自由變元並未在 σ[ϕ/P]\sigma[\phi/P] 中被量詞拘束。

定義 2.2.12 擴充語言

A\mathfrak{A} 的擴充語言 L(A)L(\mathfrak{A}) 由語言 LLA\mathfrak{A} 的類型加上 A|\mathfrak{A}| 中的常元所構成。我們將 A|\mathfrak{A}| 中的 aa 標註為 aˉ\bar{a},作為語言中的常元符號。

此處的 A|\mathfrak{A}| 表示為 A\mathfrak{A} 中的所有元素命名。

語義學

考慮 A=A,R1,...,Rn,F1,...,Fm,{ciiI}\mathfrak{A} =\langle A, R_1, ..., R_n, F_1, ...,F_m, \{ c_i|i\in I \} \rangle,以及給定的相似類型 r1,...,rn;a1,...,am;κ\langle r_1, ..., r_n; a_1, ..., a_m; \kappa \rangle

相應的擴充語言的述詞符號是 R1ˉ,...,Rnˉ,F1ˉ,...,Fmˉ,ciˉ\bar{R_1}, ..., \bar{R_n}, \bar{F_1}, ..., \bar{F_m}, \bar{c_i}。並且,對於所有的 aAa\in \mathfrak{A},我們有 aˉ\bar{a} 的常元符號。

定義 2.3.13 封閉詞項與構句的詮釋

TERMcTERM_c

L(A)L(\mathfrak{A})A\mathfrak{A} 的封閉詞項的詮釋是一個函數 (.)A:TERMcA(.)^{\mathfrak{A}}: TERM_c \rightarrow |\mathfrak{A}| 滿足(使用 Scott brackets 標記):

  1. ciˉA=ci\llbracket \bar{c_i} \rrbracket_{\mathfrak{A}} = c_i
  2. aˉA=a\llbracket \bar{a} \rrbracket_{\mathfrak{A}} = a
  3. Fi(t1,...,tai)A=Fiˉ(t1A,...,taiA)\llbracket F_i(t_1, ..., t_{a_i}) \rrbracket_{\mathfrak{A}} = \bar{F_i}(\llbracket t_1 \rrbracket_{\mathfrak{A}}, ..., \llbracket t_{a_i} \rrbracket_{\mathfrak{A}})

SENTSENT

L(A)L(\mathfrak{A})A\mathfrak{A} 的語句的詮釋是一個函數 (.)A:SENT{0,1}(.)^{\mathfrak{A}}: SENT \rightarrow \{ 0, 1 \} 滿足:

  1. A=0\llbracket \bot \rrbracket_{\mathfrak{A}} = 0
  2. RˉA=R\llbracket \bar{R} \rrbracket_{\mathfrak{A}} = R0011);
  3. Rˉi(t1,...,tri)A=1\llbracket \bar{R}_i(t_1, ..., t_{r_i}) \rrbracket_{\mathfrak{A}} = 1 當且僅當 t1A,...,triARi\llbracket t_1 \rrbracket_{\mathfrak{A}}, ..., \llbracket t_{r_i} \rrbracket_{\mathfrak{A}} \in R_i
  4. t1=t2A=1\llbracket t_1 = t_2 \rrbracket_{\mathfrak{A}} = 1 當且僅當 t1A=t2A\llbracket t_1 \rrbracket_{\mathfrak{A}} = \llbracket t_2 \rrbracket_{\mathfrak{A}}
  5. ϕψA=min(ϕA,ψA)\llbracket \phi \land \psi \rrbracket_{\mathfrak{A}} = \min(\llbracket \phi \rrbracket_{\mathfrak{A}}, \llbracket \psi \rrbracket_{\mathfrak{A}})
  6. ϕψA=max(ϕA,ψA)\llbracket \phi \lor \psi \rrbracket_{\mathfrak{A}} = \max(\llbracket \phi \rrbracket_{\mathfrak{A}}, \llbracket \psi \rrbracket_{\mathfrak{A}})
  7. ϕψA=max(1,1ϕA+ψA)\llbracket \phi \rightarrow \psi \rrbracket_{\mathfrak{A}} = \max(1, 1 - \llbracket \phi \rrbracket_{\mathfrak{A}} + \llbracket \psi \rrbracket_{\mathfrak{A}})
  8. ϕψA=1ϕAψA\llbracket \phi \leftrightarrow \psi \rrbracket_{\mathfrak{A}} = 1 - |\llbracket \phi \rrbracket_{\mathfrak{A}} - \llbracket \psi \rrbracket_{\mathfrak{A}}|
  9. ¬ϕA=1ϕA\llbracket \neg \phi \rrbracket_{\mathfrak{A}} = 1 - \llbracket \phi \rrbracket_{\mathfrak{A}}
  10. xiϕA=minaAϕ[a/xi]A\llbracket \forall x_i \phi \rrbracket_{\mathfrak{A}} = \min_{a \in |\mathfrak{A}|} \llbracket \phi[a/x_i] \rrbracket_{\mathfrak{A}}
  11. xiϕA=maxaAϕ[a/xi]A\llbracket \exists x_i \phi \rrbracket_{\mathfrak{A}} = \max_{a \in |\mathfrak{A}|} \llbracket \phi[a/x_i] \rrbracket_{\mathfrak{A}}

定義 2.3.14 \models

Aϕ\mathfrak{A}\models \phi 當且僅當 ϕA=1\llbracket \phi \rrbracket_{\mathfrak{A}} = 1

定義 2.3.15 宇封閉句 universal closure

FV(ϕ)=z1,...,znFV(\phi)={z_1, ..., z_n},則 Cl(ϕ):=z1...zkϕCl(\phi):= \forall z_1...z_k \phiϕ\phi 的宇封閉句。


透過宇封閉句,我們可以將詮釋從封閉構句擴展到所有構句,由於對於所有的封閉構句 ψ\psiCl(ψ)=ψCl(\psi) = \psi,因此這個定義是合法的:

定義 2.3.16

Aϕ\mathfrak{A}\models \phi 當且僅當 ACl(ϕ)\mathfrak{A}\models Cl(\phi)

定義 2.3.17

  1. ϕ\models \phi 當且僅當 Aϕ\mathfrak{A}\models \phi 對所有的 A\mathfrak{A} 成立。
  2. AΣ\mathfrak{A}\models \Sigma 當且僅當 Aϕ\mathfrak{A}\models \phi 對所有的 ϕΣ\phi \in \Sigma 成立。
  3. Γϕ\Gamma \models \phi 當且僅當若 AΓ\mathfrak{A}\models \Gamma,則 Aϕ\mathfrak{A}\models \phi

引理 2.3.18 構句的邏輯意涵

對於語句 ϕ\phiψ\psi,下列等價性成立:

  1. Aϕψ\mathfrak{A}\models \phi \land \psi 當且僅當 Aϕ\mathfrak{A}\models \phiAψ\mathfrak{A}\models \psi
  2. Aϕψ\mathfrak{A}\models \phi \lor \psi 當且僅當 Aϕ\mathfrak{A}\models \phiAψ\mathfrak{A}\models \psi
  3. A¬ϕ\mathfrak{A}\models \neg \phi 當且僅當 A⊭ϕ\mathfrak{A}\not\models \phi
  4. Aϕψ\mathfrak{A}\models \phi \rightarrow \psi 當且僅當 Aϕ\mathfrak{A}\models \phi 蘊含 Aψ\mathfrak{A}\models \psi
  5. Aϕψ\mathfrak{A}\models \phi \leftrightarrow \psi 當且僅當 Aϕ\mathfrak{A}\models \phi 等價於 Aψ\mathfrak{A}\models \psi
  6. Axiϕ\mathfrak{A}\models \forall x_i \phi 當且僅當 Aϕ[aˉ/xi]\mathfrak{A}\models \phi[\bar{a}/x_i] 對所有的 aAa \in |\mathfrak{A}|
  7. Axiϕ\mathfrak{A}\models \exists x_i \phi 當且僅當 Aϕ[aˉ/xi]\mathfrak{A}\models \phi[\bar{a}/x_i] 對某個 aAa \in |\mathfrak{A}|

述詞邏輯的簡單性質

定理 2.4.19 量詞拘束構句的等價性

  1. ¬x¬ϕxϕ\models \neg \forall x \neg \phi \leftrightarrow \exists x \phi
  2. ¬x¬ϕxϕ\models \neg \exists x \neg \phi \leftrightarrow \forall x \phi

定理 2.4.20 量詞的結構規則

  1. xyϕyxϕ\models \forall x \forall y \phi \leftrightarrow \forall y \forall x \phi
  2. xyϕyxϕ\models \exists x \exists y \phi \leftrightarrow \exists y \exists x \phi
  3. xϕϕ\models \forall x \phi \leftrightarrow \phi,當 x∉FV(ϕ)x \not\in FV(\phi)
  4. xϕϕ\models \exists x \phi \leftrightarrow \phi,當 x∉FV(ϕ)x \not\in FV(\phi)

定理 2.4.21 量詞的分配規則

  1. x(ϕψ)(xϕxψ)\models \forall x (\phi \land \psi) \leftrightarrow (\forall x \phi \land \forall x \psi)
  2. x(ϕψ)(xϕxψ)\models \exists x (\phi \lor \psi) \leftrightarrow (\exists x \phi \lor \exists x \psi)
  3. x(ϕψ)(xϕψ)\models \forall x (\phi \lor \psi) \leftrightarrow (\forall x \phi \lor \psi),當 x∉FV(ψ)x \not\in FV(\psi)
  4. x(ϕψ)(xϕψ)\models \exists x (\phi \land \psi) \leftrightarrow (\exists x \phi \land \psi),當 x∉FV(ψ)x \not\in FV(\psi)

引理 2.4.22 替代的交換律

  1. x∉FV(r)x\not\in FV(r)yy 是相異變數,則 (t[s/x])[r/y]=(t[r/y])[s[r/y]/x](t[s/x])[r/y]=(t[r/y])[s[r/y]/x]
  2. x∉FV(s)x\not\in FV(s)yy 是相異變數,且 ttss 對於 xxyyϕ\phi 是自由的,則 (ϕ[t/x])[s/y]=(ϕ[s/y])[t[s/y]/x](\phi[t/x])[s/y]=(\phi[s/y])[t[s/y]/x]
  3. ψ\psi 對於 PPϕ\phi 是自由的,並且 tt 對於 xxϕ\phiψ\psi 中是自由的,則 (ϕ[ψ/P])[t/x]=(ϕ[t/x])[ψ[t/x]/P](\phi[\psi/P])[t/x]=(\phi[t/x])[\psi[t/x]/P]
  4. ϕ\phiψ\psi 對於 P1P_1P2P_2σ\sigma 是自由的,ψ\psi 對於 P2P_2ϕ\phi 中是自由的,並且 P1P_1ψ\psi 中沒有出現,則 (σ[ϕ/P1])[ψ/P2]=(σ[ψ/P2])[ϕ[ψ/P2]/P1](\sigma[\phi/P_1])[\psi/P_2]=(\sigma[\psi/P_2])[\phi[\psi/P_2]/P_1]

推論 2.4.23

  1. z∉FV(t)z\not\in FV(t),則 t[aˉ/x]=(t[z/x])[aˉ/z]t[\bar{a}/x] = (t[z/x])[\bar{a}/z]
  2. z∉FV(ϕ)z\not\in FV(\phi)zz 對於 xxϕ\phi 中是自由的,則 ϕ[aˉ/x]=(ϕ[z/x])[aˉ/z]\phi[\bar{a}/x] = (\phi[z/x])[\bar{a}/z]

定理 2.4.24 拘束變數的變換

xxyy 對於 zzϕ\phi 中是自由的,且 x,y∉FV(ϕ)x, y \not\in FV(\phi),則 xϕ[x/z]yϕ[y/z]\models\exists x \phi [x/z] \leftrightarrow \exists y \phi [y/z]xϕ[x/z]yϕ[y/z]\models\forall x \phi [x/z] \leftrightarrow \forall y \phi [y/z]

推論 2.4.25

所有構句都等價一個沒有變元同時是自由又拘束的構句。

定理 2.4.26 替代定理

  1. t1=t2s[t1/x]=s[t2/x]\models t_1 = t_2 \rightarrow s[t_1/x] = s[t_2/x]
  2. t1=t2(ϕ[t1/x]ϕ[t2/x])\models t_1 = t_2 \rightarrow (\phi[t_1/x] \leftrightarrow \phi[t_2/x])
  3. (ϕψ)(σ[ϕ/P]σ[ψ/P])\models(\phi \leftrightarrow \psi) \rightarrow (\sigma[\phi/P] \leftrightarrow \sigma[\psi/P])

推論 2.4.27

  1. s[t/x]=s[tˉ/x]\llbracket s[t/x] \rrbracket = \llbracket s [\bar{ \llbracket t \rrbracket } / x] \rrbracket
  2. ϕ[t/x]=ϕ[tˉ/x]\llbracket \phi[t/x] \rrbracket = \llbracket \phi [\bar{ \llbracket t \rrbracket } / x] \rrbracket

定義 2.4.28 前束標準句 prenex normal form

一個構句 ϕ\phi 是前束標準式,當且僅當 ϕ=Q1x1...Qnxnψ\phi = Q_1 x_1 ... Q_n x_n \psi,其中 QiQ_i 是量詞,{Qi}\{ Q_i \} 可以是 \emptysetψ\psi 是開放構句,且 x1,...,xnx_1, ..., x_n 是互異的變數。

定理 2.4.29 前束標準句的存在

對於每一個構句 ϕ\phi,存在一個等價的前束標準句。

定義 2.4.30 一元述詞與量詞作用域 unary predicate and scope of quantifier

PP 是一個一元述詞符號,則 (xP)ϕ=dfx(P(x)ϕ)(\forall x \in P)\phi =_\text{df} \forall x (P(x) \rightarrow \phi)(xP)ϕ=dfx(P(x)ϕ)(\exists x \in P)\phi =_\text{df} \exists x (P(x) \land \phi)

定義 2.4.31 子構句

Sub+Sub^+SubSub^- 定義如下:

  1. Sub+(ϕ)={ϕ}Sub^+(\phi) = \{ \phi \}
  2. Sub(ϕ)=Sub^-(\phi) = \emptyset,對於 ϕ\phi 是原子句。
  3. Sub+(ϕ1ϕ2)=Sub+(ϕ1)Sub+(ϕ2){ϕ1ϕ2}Sub^+(\phi_1 \square \phi_2) = Sub^+(\phi_1) \cup Sub^+(\phi_2) \cup \{ \phi_1 \square \phi_2 \}
  4. Sub(ϕ1ϕ2)=Sub(ϕ1)Sub(ϕ2)Sub^-(\phi_1 \square \phi_2) = Sub^-(\phi_1) \cup Sub^-(\phi_2),對於 {,}\square \in \{ \land, \lor \}
  5. Sub+(ϕ1ϕ2)=Sub+(ϕ1)Sub(ϕ2){ϕ1ϕ2}Sub^+(\phi_1 \rightarrow \phi_2) = Sub^+(\phi_1) \cup Sub^-(\phi_2) \cup \{ \phi_1 \rightarrow \phi_2 \}
  6. Sub(ϕ1ϕ2)=Sub+(ϕ1)Sub(ϕ2)Sub^-(\phi_1 \rightarrow \phi_2) = Sub^+(\phi_1) \cup Sub^-(\phi_2)
  7. Sub+(Qx.ϕ)=Sub+(ϕ){Qx.ϕ}Sub^+(Qx.\phi) = Sub^+(\phi) \cup \{ Qx.\phi \}
  8. Sub(Qx.ϕ)=Sub(ϕ)Sub^-(Qx.\phi) = Sub^-(\phi),對於 Q{,}Q \in \{ \forall, \exists \}

ϕSub+(ψ)\phi \in Sub^+(\psi),我們說 ϕ\phiψ\psi 中正面出現(occurs positively),若 ψSub+(ϕ)\psi \in Sub^+(\phi),我們說 ϕ\phiψ\psi 中負面出現(occurs negatively)。

Van Dalen 在這裡的定義缺了 ¬ϕ\neg \phi,我覺得這是滿奇怪的。按照正面出現和負面出現的意義,應該如此定義:

  1. Sub+(¬ϕ)=Sub(ϕ)¬ϕSub^+(¬\phi) = Sub^-(\phi) \cup {¬\phi}
  2. Sub(¬ϕ)=Sub+(ϕ)Sub^-(¬\phi) = Sub^+(\phi)

定理 2.4.32 出現與語義值

ϕ\phiψ\psi 中未負面出現、在 σ\sigma 中未正面出現,則:

  1. ϕ1ϕ2σ[ϕ1/ϕ]σ[ϕ2/ϕ]\llbracket \phi_1 \rrbracket \leq \llbracket \phi_2 \rrbracket \Rightarrow \llbracket \sigma[\phi_1 / \phi ] \rrbracket \leq \llbracket \sigma[\phi_2 / \phi ] \rrbracket
  2. ψ1ψ2σ[ψ1/ψ]σ[ψ2/ψ]\llbracket \psi_1 \rrbracket \leq \llbracket \psi_2 \rrbracket \Rightarrow \llbracket \sigma[\psi_1 / \psi ] \rrbracket \geq \llbracket \sigma[\psi_2 / \psi ] \rrbracket
  3. A(ϕ1ϕ2)(σ[ϕ1/ϕ]σ[ϕ2/ϕ])\mathfrak{A}\models (\phi_1 \rightarrow \phi_2) \rightarrow (\sigma[\phi_1 / \phi] \rightarrow \sigma[\phi_2 / \phi])
  4. A(ψ1ψ2)(σ[ψ2/ϕ]σ[ψ1/ϕ])\mathfrak{A}\models (\psi_1 \rightarrow \psi_2) \rightarrow (\sigma[\psi_2 / \phi] \rightarrow \sigma[\psi_1 / \phi])

同一性

定義 2.5.1 同一性公理

== 是同一性的符號,它並非一般的二元述詞,因為它需要滿足以下公理與公理格式:

定義 2.5.2 同一性的推導規則

引理 2.5.3 公理的可推導性

\vdash I1_1, I2_2, I3_3, I4_4

引理 2.5.4 RI4_4 的可推導性

LL 的型是 r1,...,rn;a1,...,am;κ\langle r_1, ..., r_n; a_1, ..., a_m; \kappa \rangle。若給定以下規則:

  1. D/x1=y1,...,xri=yri,Pi(x1,...,xri)XD / x_1 = y_1, ..., x_{r_i} = y_{r_i}, P_i(x_1, ..., x_{r_i}) \in X,則 D/x1=y1,...,xri=yri,P1(x1,...,xri)Pi(y1,...,yri)D / x_1 = y_1, ..., x_{r_i} = y_{r_i}, P_1(x_1, ..., x_{r_i}) \over P_i(y_1, ..., y_{r_i}) X\in X,對於所有 ini \leq n
  2. D/x1=y1,...,xaj=yajXD / x_1 = y_1, ..., x_{a_j} = y_{a_j} \in X,則 D/x1=y1,...,xaj=yajfj(x1,...,xaj)=fj(y1,...,yaj)D / x_1 = y_1, ..., x_{a_j} = y_{a_j} \over f_j(x_1, ..., x_{a_j}) = f_j(y_1, ..., y_{a_j}) X\in X,對於所有 jmj \leq m

那麼 RI4_4 是可推導的。

自然演繹法

定義 2.6.1 擴充的演繹集合

1.4.1 的自然演繹法開始擴充,加入兩個推導規則:

定義 2.6.2 形式二

定義 2.6.3 對 \models 的擴充

Γ\Gamma 為一個構句集合,且令 {xi1,xi2,}={FV(ψ)ψΓ{σ}}\{x_{i_1}, x_{i_2}, \ldots\} = \{FV(\psi) | \psi \in \Gamma \cup \{\sigma\}\}

a\mathbf{a}A|\mathfrak{A}| 中元素的序列 (a1,a2,)(a_1, a_2, \ldots)(允許重複),則 Γ(a)\Gamma(\mathbf{a}) 是透過將 Γ\Gamma 的所有構句同時把 xijx_{i_j} 替換為 ajˉ\bar{a_j} (j1j \geq 1) 所得到的集合(對於 Γ={ψ}\Gamma = \{\psi\},我們寫作 ψ(a)\psi(\mathbf{a}))。

我們定義:

定理 2.6.4 健全性

ΓσΓσ\Gamma \vdash \sigma \Rightarrow \Gamma \vDash \sigma

定理 2.6.5 形式三

xx 是並未出現在 Γ\Gammaσ\sigma 中的變數,則:

  1. ΓϕΓ[x/c]ϕ[x/c]\Gamma \vdash \phi \Rightarrow \Gamma[x/c] \vdash \phi[x/c]
  2. cc 並未出現在 Γ\Gamma 中,則 Γϕ(c)Γxϕ(x)\Gamma \vdash \phi(c) \Rightarrow \Gamma \vdash \forall x \phi(x)

引理 2.6.6 存在量詞的引入

xϕ=df¬x¬ϕ\exists x \phi =_\text{df} \neg\forall x \neg\phi,則:

  1. ϕ(t)xϕ(x)\phi(t)\vdash \exists x \phi(x)tt 對於 xxϕ\phi 中是自由的,
  2. Γ,ϕ(x)ψΓ,xϕ(x)ψ\Gamma, \phi(x) \vdash \psi \Rightarrow \Gamma, \exists x \phi(x) \vdash \psi,如果 xxϕ\phi 或某個 Γ\Gamma 的構句中不是自由的。

相反地,從另一個進路來看,給定這些推導規則,我們也可以證明 xϕ(x)¬x¬ϕ(x)\vdash \exists x \phi(x) \leftrightarrow \neg\forall x \neg\phi(x)