3. 完備性與其他應用

January 15, 2022

Dirk van Dalen, Logic and Structure, 4th.

3.1 完備性定理

兩個重要工具:

〔引理 3.1.1(模型存在引理)〕Γ\Gamma 是一個一致語句集,則 Γ\Gamma 有一個模型。

〔引理 3.1.2〕LL 的基數為 κ\kappa。若 Γ\Gamma 是一個一致語句集,則 Γ\Gamma 有一個基數 κ\leq\kappa 的模型。

需要證明的:

〔定理 3.1.3(完備性定理)〕 ΓϕΓϕ\Gamma\vdash\phi\Leftrightarrow\Gamma\vDash\phi


〔定義 3.1.4〕

  1. 一個定理 TT 是一個具 TϕϕTT\vdash\phi\Rightarrow\phi\in T 性質的語句集合(即定理是演繹封閉的),
  2. 一個使得 T={ϕΓϕ}T = \{ \phi|\Gamma\vdash\phi \}Γ\Gamma 是定理 TT 的公理集合,裡面的元素稱之為公理,
  3. TT 是一個 Henkin 定理,若每個 xϕ(x)\exist x\phi(x),都存在常數 cc 使得 xϕ(x)ϕ(c)T\exist x\phi(x)\rightarrow\phi(c)\in T,這樣的 cc 稱作 xϕ(x)\exist x\phi(x) 的目擊(witness)。

〔定義 3.1.5〕TTTT' 分別是語言 LLLL' 的定理:

  1. TT'TT 的擴展(extension),若 TTT\sube T'
  2. TT'TT 的保守擴展(conservative extension),若 TL=TT'\cap L=T

〔定義 3.1.6〕TTLL 的定理。語言 LL^* 來自 LL 為每個語句 xϕ(x)\exist x\phi(x) 加上目擊的常數 cϕc_\phiTT^* 是一個有公理集合 T{xϕ(x)ϕ(cϕ)xϕ(x) 是封閉的,且有目擊 cϕ}T\cup\{\exist x\phi(x)\rightarrow\phi(c_\phi)|\exist x\phi(x) \text{ 是封閉的,且有目擊 }c_\phi\} 的定理。


〔引理 3.1.7〕 TT^*TT 的保守擴展。

證明:令 xϕ(x)ϕ(c)\exist x\phi(x)\rightarrow\phi(c) 是一個新公理,Γ\GammaTT 的公理集合,假設 Γ,xϕ(x)ϕ(c)ψ\Gamma,\exist x\phi(x)\rightarrow\phi(c)\vdash\psicc 不在 ψ\psi 中出現,以推論規則證明 Γψ\Gamma\vdash\psi。再透過歸納法證明,若 ψT\psi\in T^*ψL\psi\in L,則 ψT\psi\in T


〔引理 3.1.8〕 定義 T0T;Tn+1=(Tn)T_0\coloneqq T ; T_{n+1}=(T_n)^*,定義 Tω{Tnn0}T_\omega\coloneqq\cup\{T_n|n\geq 0\}。則 TωT_\omega 是一個 Henkin 定理,並且是 TT 上的保守擴展。

〔系理 3.1.8.1〕TT 是一致的,則 TωT_\omega 是一致的。

證明:若 TωT_\omega\vdash\bot,則因保守性 TT\vdash\bot


〔引理 3.1.9(Lindenbaum)〕 每個一致定理都包含在最大一致定理中。

證明:考慮 TT 是一致定理,令定理 AATT 所有的一致擴展 TiT_i 的集合,有偏序的包含關係。令 {TiiI}\{T_i|i\in I\} 是任意一個鏈,由於 T=TiT'=\bigcup T_i(可簡單看出 TT' 是一致的)是任何 TiT_i 的上界,因此根據 Zorn 引理,AA 有最大元素 TmT_m。這個 TmT_m 即包含 TT 的最大一致集合。


〔引理 3.1.10〕 Henkin 定理在同一個語言中的擴展依然是 Henkin 定理。


〔引理 3.1.11(模型存在引理)〕Γ\Gamma 是一致的,則 Γ\Gamma 有模型。

證明

T={σΓσ}T = \{\sigma|\Gamma\vdash\sigma\} 是一個定理,TT 的模型就會是 Γ\Gamma 的模型。令 TmT_mTT 的最大一致 Henkin 擴展,語言 LmL_m

建立模型 A\mathfrak{A} 如下:

  1. A={tLmt 是封閉的}A=\{t\in L_m| t\text{ 是封閉的}\}
  2. 為每個 f\overline{f} 函數符號,定義 f^:AkA\hat{f}: A^k\rightarrow Af^(t1,...,tk)f(t1,...,tk)\hat{f}(t_1,...,t_k)\coloneqq \overline{f}(t_1,...,t_k)
  3. 為每個述詞符號 P\overline{P},定義 P^Ap\hat{P}\sube A^pt1,...,tpP^TmP(t1,...,tp)\lang t_1,...,t_p\rang\in\hat P\Leftrightarrow T_m\vdash \overline P(t_1,...,t_p)
  4. 為每個常數 c\overline c 定義 c^c\hat c\coloneqq\overline c

接著證明 \backsimtsTmt=s\coloneqq t\backsim s \Leftrightarrow T_m\vdash t=s)符合公理 I1I4I_1-I_4

最後,證明 A\mathfrak{A}TT 的一個模型:

  1. 證明對於 tAt\in AAϕ(t)Aϕ([t])\mathfrak{A}\vDash\phi(t)\Leftrightarrow\mathfrak{A}\vDash\phi(\overline{[t]})

Profile picture

Wei Hung 的筆記 / 部落格。