Skip to content

「van Dalen,邏輯與結構」筆記:述詞邏輯

Posted on:2024年2月21日 at 下午09:25
「van Dalen,邏輯與結構」筆記:述詞邏輯

目錄

Open 目錄

結構

定義 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 的(常數)元素。

定義 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 \rangleA,R1,...,Rn,F1,...,Fm,{ciiI}\langle A, R_1, ..., R_n, F_1, ...,F_m, \{ c_i|i\in I \} \rangle 的相似性類型。

定義 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 N)
  3. 函數封閉性:若 t1,...,taiXt_1, ..., t_{a_i} \in X,則 fi(t1,...,tai)Xf_i(t_1, ..., t_{a_i}) \in X

定義 2.2 構句集

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

  1. X\bot \in X
  2. ri=0r_i = 0πiX\pi_i\in X(即 π\pi 是命題符號);
  3. t1,...,triTERMt_1,...,t_{r_i} \in TERM,則 πi(t1,...,tri)X\pi_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 \land \psi), (\phi \lor \psi), (\phi \rightarrow \psi), (\phi \leftrightarrow \psi) \in X(寫作 (ϕψ)(\phi \square \psi));
  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.3 歸納法與遞迴性

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

一般歸納法原理過於繁瑣,這裡不再贅述。

語詞集的遞迴性

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. H(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:AtAH_{at}: At \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.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. π\pi 是命題符號,則 FV(π)=FV(\pi) = \emptyset
  3. FV(t1=t2)=FV(t1)FV(t2)FV(t_1 = t_2) = FV(t_1) \cup FV(t_2)
  4. FV(πi(t1,...,tri))=FV(t1)...FV(tri)FV(\pi_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.5 封閉語詞和封閉構句

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

定義 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. π\pi 是命題符號,則 BV(π)=BV(\pi) = \emptyset
  3. BV(t1=t2)=BV(t1)BV(t2)BV(t_1 = t_2) = BV(t_1) \cup BV(t_2)
  4. BV(πi(t1,...,tri))=BV(t1)...BV(tri)BV(\pi_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.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. π\pi 是命題符號,則 π[t/x]=π\pi[t/x] = \pi
  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. (πi(t1,...,tri))[t/x]=πi(t1[t/x],...,tri[t/x])(\pi_i(t_1, ..., t_{r_i}))[t/x] = \pi_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 是兩個構句,則 ϕ[ψ/π]\phi[\psi/ \pi] 定義如下:

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

定義 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 中是自由的。

引理 2.9

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

證明:對 ϕ\phi 做歸納法。

定義 2.10 自由構句

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

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

引理 2.11

σ\sigma 中,ϕ\phiπ\pi 是自由的,當且僅當 σ[ϕ/π]\sigma[\phi/\pi] 的變數 ϕ\phi 未被量詞拘束。

定義 2.12 擴充語言

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

語義學

定義 2.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. aA=a\llbracket a \rrbracket_{\mathfrak{A}} = a
  3. Fi(t1,...,tai)A=Fi(t1A,...,taiA)\llbracket F_i(t_1, ..., t_{a_i}) \rrbracket_{\mathfrak{A}} = 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}} = R
  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.14 \models

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

定義 2.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.16

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

定義 2.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.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.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.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.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.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 對於 π\piϕ\phi 是自由的,並且 tt 對於 xxϕ\phiψ\psi 中是自由的,則 (ϕ[ψ/π])[t/x]=(ϕ[t/x])[ψ[t/x]/π](\phi[\psi/\pi])[t/x]=(\phi[t/x])[\psi[t/x]/\pi]
  4. ϕ\phiψ\psi 對於 π1\pi_1π2\pi_2σ\sigma 是自由的,ψ\psi 對於 π2\pi_2ϕ\phi 中是自由的,並且 π1\pi_1ψ\psi 中沒有出現,則 (σ[ϕ/π1])[ψ/π2]=(σ[ψ/π2])[ϕ[ψ/π2]/π1](\sigma[\phi/\pi_1])[\psi/\pi_2]=(\sigma[\psi/\pi_2])[\phi[\psi/\pi_2]/\pi_1]

推論 2.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.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.25

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

定理 2.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. (ϕψ)(σ[ϕ/π]σ[ψ/π])\models(\phi \leftrightarrow \psi) \rightarrow (\sigma[\phi/\pi] \leftrightarrow \sigma[\psi/\pi])

推論 2.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.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.29 前束標準句的存在

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

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

PP 是一個一元述詞符號,則 (xP)ϕ:=x(P(x)ϕ)(\forall x \in P)\phi := \forall x (P(x) \rightarrow \phi)(xP)ϕ:=x(P(x)ϕ)(\exists x \in P)\phi := \exists x (P(x) \land \phi)