1. 回顧

上文我們從代數學角度重新認識了自然數，認識了自然數是如何被編碼為符號串的，

以及自然數在數學上是如何表示的。

我們的整體思路是，首先用公理化的方式建立一個形式系統，

然後為這個形式系統選擇一種數學解釋作為它的語義，

這樣就建立了符號和數學對象之間的對應關係。

一般的，這些數學對象需要具有不同的運算性質，有不同的結構，

因此構成了不同的代數。

在《你好，類型》系列文章中，我們介紹了命題邏輯和一階謂詞邏輯，

當時，我們只是從形式系統（符號演算）的角度來介紹它們。

例如，我們只要知道公理和推導規則，就可以做出形式證明，

forall x(alphaleftrightarroweta)vdashforall xalphaleftrightarrowforall xeta 。

但是，這些符號到底代表什麼含義呢？

我們當時故意沒有提及。

本文從模型論角度來做出一些解釋。

2. 一階語言

首先讓我們回顧以下一階謂詞邏輯有哪些符號構成，

（1）變元符號集合 V ，

它由可數個（包括0個）變元符號組成，用 x_1,x_1,cdots,x_n,cdots 表示。（2）邏輯連接詞符號集合 C ，它由邏輯連接詞符號 eg,wedge,vee, ightarrow,leftrightarrow 組成。（3）量詞符號集合 Q ，包括 forall,exists 。（4）等詞符號集合 E ，只包括一個符號 doteq 。（5）括弧集合，包括 ),( 。

以上這些符號稱為邏輯符號，每個一階邏輯都有這些符號。

而不同的一階邏輯，還有屬於自己的非邏輯符號。

（1）常元符號集合 mathscr{L}_c ，

它由可數個（包括0個）常元符號組成，用 c_1,c_2,cdots 表示。（2）函數符號集合 mathscr{L}_f ，它由可數個（包括0個）函數符號組成，用 f_1,f_2,cdots 表示。（3）謂詞符號集合 mathscr{L}_P ，它由可數個（包括0個）謂詞符號組成，用 P_1,P_2,cdots 表示。

等詞符號 doteq 實際上可以看做是一個謂詞符號。

因此，一階謂詞邏輯是一種一階邏輯。

一階邏輯中的邏輯符號和非邏輯符號，稱為一階語言，記為 mathscr{L} 。

3. 初等算術語言

初等算術語言是一個一階語言，記為 Pi 。

它的常元符號集合為 {0} ，函數符號集合為 {S,+,cdot} ，謂詞符號集合為 {<} 。

其中， S 可以表示算術中的後繼函數，

而二元函數符號 + 和 cdot 可以分別表示算術中的加法和乘法，謂詞符號 < 可以描述自然數之間的小於關係。

4. 語法項和邏輯公式

從形式語言的角度來看，除了知道語言包含哪些符號之外，還要指定語法，

習慣上，我們經常使用BNF來指定， t::=c|x|f~t_1cdots t_n

即一個合法的項，可以歸納定義為，

（1）每一個常元都是合法的項，（2）每一個變元都是合法的項，（3）如果 t_1,t_2,cdots,t_n 都是合法的項，而 f 是一個 n 元函數符號，那麼 f~t_1cdots t_n 也是一個合法的項。

初等算術語言 Pi 中的合法項，以下符號串都是合法的，

S0 ， Sx_1 ， +S0SSx ， cdot x_1+Sx_1x_2 ，而 SS< 是不合法的。

我們知道邏輯證明，並不是建立在形式語法之上的，

而是建立在公理系統上面，而每一個推導規則都表明了前提和結論之間的關係，

這些前提和結論，稱為邏輯公式。

一階語言 mathscr{L} 中的邏輯公式，用大寫字母 A,B,cdots 表示，定義為，

A ::= t_1doteq t_2 | Rt_1cdot cdot cdot t_n | eg A | Awedge B | Avee B | A ightarrow B | Aleftrightarrow B | forall xA | exists xA

即，邏輯公式可以歸納的定義為，

（1）如果 t_1 和 t_2 是合法的項，則 t_1doteq t_2 是公式，（2）如果 t_1, ..., t_n 是合法的項，而 R 是一個 n 元謂詞，則 Rt_1cdot cdot cdot t_n 是公式，（3）如果 A 是公式，則 eg A 是公式，（4）若 A, B 是公式，則 Awedge B, Avee B, A ightarrow B, Aleftrightarrow B 都是公式，（5）若 A 是公式並且 x 是一個變元，那麼 forall xA 和 exists xA 也是公式， x 稱為約束變元。

例，以下符號串可以看做一個初等算術公式，

forall x eg (Sxdoteq 0), forall xforall y(< xy ightarrow(exists (ydoteq +xz)))

5. 語義模型

有了一階語言之後，我們就可以為符號選擇語義了，

通常的，語言的語義有兩部分組成，其一稱為結構，用來解釋常元符號，函數符號和謂詞符號，其二稱為賦值，用來解釋變元符號。

5.1 語言結構

一階語言 mathscr{L} 的結構 M 是一個偶對，記為 M=(mathbb{M}, I) ，其中，

（1） mathbb{M} 是一個非空集合，稱為論域，（2） I 是從 mathscr{L} 到 mathbb{M} 的映射，稱為解釋，記為 I:mathscr{L} ightarrow mathbb{M} ，它滿足下面三個條件

對 mathscr{L} 中的每一個常元符號 c ， I(c) 是 mathbb{M} 中的元素

對 mathscr{L} 中的每一個 n 元函數符號 f ， I(f) 是 mathbb{M} 上的 n 元函數對 mathscr{L} 中的每一個 n 元謂詞符號 P ， I(P) 是 mathbb{M} 上的一個 n 元關係

例，我們可以指定初等算術語言 Pi 的結構為，偶對 N=(mathbb{N}, I) ，

其中論域 mathbb{N} 為自然數集， I(S) 為自然數集上的加 1 函數， I(+) 為自然數加法運算， I(cdot) 為自然數乘法運算。 I(<) 為自然數集上的小於關係。

5.2 變元賦值

賦值 sigma 是一個映射， sigma:V omathbb{M} ，

它將 mathscr{L} 中的每一個變元，賦以論域 mathbb{M} 中的一個元素 a ，

記為 sigma(x)=a ，其中 xin V,ainmathbb{M} 。

有了賦值運算之後，公式中的變元就固定下來了，

我們就可以談論在某一指定賦值運算下公式的語義了。

5.3 模型和語義

給定一階語言 mathscr{L} ，並指定結構 M 和賦值 sigma ，

我們稱 (M,sigma) 是，我們為語言 mathscr{L} 選擇的一個模型。

項的語義

選擇了模型 (M,sigma) 之後， mathscr{L} 中的合法項 t 的語義，

就可以歸納的定義為論域 mathbb{M} 中的元素了，記為 t_{M[sigma]} 。（1） x_{M[sigma ]}=sigma (x) ， x 為變元符號（2） c_{M[sigma ]}=c_M ， c 為常元符號（3） (ft_1cdot cdot cdot t_n)_{M[sigma ]}=f_M((t_1)_{M[sigma ]},cdot cdot cdot (t_n)_{M[sigma ]})

例，初等算術 Pi 中項的語義，

(+x_1Sx_7)_{N[sigma ]}=(x_1)_{N[sigma ]}+(Sx_7)_{N[sigma ]}=1+((x_7)_{N[sigma ]}+1)=1+(7+1)=9

邏輯公式的語義

公式 A 在模型 (M, sigma ) 下的語義是一個真假值，用 A_{M[sigma ]} 表示，歸納定義如下，

（1） (Pt_1cdot cdot cdot t_n)_{M[sigma ]}=P_M((t_1)_{M[sigma ]},cdot cdot cdot ,(t_n)_{M[sigma ]}) （2） (t_1doteq t_2)_{M[sigma ]}=egin{cases}T,& ext{if }(t_1)_{M[sigma ]}=(t_2)_{M[sigma ]}\F,& ext{otherwise}end{cases} （3） ( eg A)_{M[sigma ]}=B_ eg (A_{M[sigma ]}) （4） (Avee B)_{M[sigma ]}=B_vee (A_{M[sigma ]}, B_{M[sigma ]}) （5） (Awedge B)_{M[sigma ]}=B_wedge (A_{M[sigma ]}, B_{M[sigma ]}) （6） (A ightarrow B)_{M[sigma ]}=B_ ightarrow (A_{M[sigma ]}, B_{M[sigma ]}) （7） (Aleftrightarrow B)_{M[sigma ]}=B_leftrightarrow (A_{M[sigma ]}, B_{M[sigma ]}) （8） (forall x_iA)_{M[sigma ]}=egin{cases}T,&forall ain M, A_{M[sigma [x_i:=a]]}=T\F,& ext{otherwise}end{cases} （9） (exists x_iA)_{M[sigma ]}=egin{cases}T,&exists ain M, A_{M[sigma [x_i:=a]]}=T\F,& ext{otherwise}end{cases}

其中，二元真值函數 B_wedge, B_vee, B_ ightarrow, B_leftrightarrow ，分別邏輯連接詞符號 wedge, vee, ightarrow, leftrightarrow 的語義。

至此，我們通過為一階語言指定模型，

將語言中所有的符號串都進行了解釋。

6. 總結

本文以一階邏輯為例，從邏輯學角度給出了語義模型的定義，

由此，一階邏輯系統中的符號串，都有了一個數學對象與之對應，它們是論域，論域集合上的函數和運算。

可想而已，這些數學對象是有代數性質的，下文我們將繼續深入瞭解。

參考

你好，類型（五）：Predicate logic

數理邏輯 一階邏輯

下一篇：語言背後的代數學（四）：哥德爾定理


推薦閱讀：
相关文章