證明論學習筆記5：賦值系統

05-18

證明論學習筆記5：賦值系統

來自專欄類型論驛站

目錄：類型論驛站寫作計劃

上一篇：證明論學習筆記4：直覺主義邏輯和相繼式演算

賦值系統為邏輯語句提供語義詮釋。我們以命題語言 $L$ 為例，其句法規則如下：

命題語言的句法規則：

如果 $A$ 為原子句，那麼 $A$ 為 $L$ 中的句子。
$ot$ 是 $L$ 中的句子。
如果 $A$ 為 $L$ 中的句子，那麼 $eg A$ 也是 $L$ 中的句子。
如果 $A$ 和 $B$ 為 $L$ 中的句子，那麼 $Awedge B, Avee B$ 以及 $A o B$ 也都是 $L$ 中的句子。

對於特定的釋義（或模型） $m$ ，句子 $p$ 的語義記作 $[[p]]_m$ 。若 $[[p]]_m$ 為真，我們也可以寫作 $mVdash p$ 。Dummett 採用二值或多值真值表為原子句以及複合句提供語義解釋。例如， $mVdash Awedge B$ 當且僅當 $mVdash A$ 且 $mVdash B$ 。

形式地，我們可以將命題語言 $L$ 視為一個二元組 $langle P,O angle$ ，其中 $P$ 為原子句的可數集合， $O$ 為運算元（或曰邏輯連接詞）集合。 $ot$ 可以視為零元運算元。命題語言 $L$ 的所有語句是在 $O$ 中所有的運算下面閉合的包含 $P$ 的最小集合。由此，我們可以定義命題語言的賦值系統。

賦值系統（valuation system）的定義：

命題語言 $L$ 的賦值系統是一個三元組 $langle M,D,F angle$ ，其中

$M$ 是一個含有至少兩個元素的邏輯值集合。
$D$ 是 $M$ 的非空真子集，指定的真值集合。
$F={f_{o_1},f_{o_2},dots,f_{o_n}}$ 是和 $O={o_1,o_2,dots, o_n}$ 相對應的函數集合，使得 $f_o:M^{n_o} o M$ ，其中 $n_o$ 為運算元 $o$ 的論元（argument，數學中常譯為「參數」）個數。

經典命題邏輯的賦值系統可以用下列運算給出：

$M={0,1}$
$D={1}$
$f_{wedge}(x,y)=x imes y$
$f_vee(x,y) = x+y$
$f_ eg(x)=1-x$
$f_ o(x,y)=(1-x)+y$
$f_ot =0$

注意，在這裡我們定義 1+1=1。

賦值系統負責組合語義，而原子句的語義則由配值/指派函數（assignment）負責。對於賦值系統 $mathcal{M}=langle M,D,F angle$ ，指派函數 $a:P o M$ 為語言 $L=langle P,O angle$ 中的原子句指派邏輯值。

語義詮釋/釋義（interpretation） $v_a$ 是賦值系統和指派函數組成的二元組 $langle M,a angle$ 。我們有：

$v_a(p)=a(p), pin P$
$v_a(o(A_1,dots,A_n))=f_o(v_a(A_1),dots,v_a(A_n))$ ，其中 $n$ 為 $o$ 的元數

後承關係（consequence relation, 參見證明論學習筆記2：希爾伯特系統）

一般認為，語言 $L$ 上的後承關係 $vdash:mathcal{P}(L) o L$ 滿足下面三個特徵：

包含（inclusion）：如果 $AinGamma,$ 那麼 $Gammavdash A$
單調性（monotonicity）： $frac{Gammavdash A}{Gamma, Delta vdash A}$ ，又稱弱化（weakening, thinning）
切（cut）： $frac{Gammavdash Cphantom{two} Delta,Cvdash A}{Delta,Gammavdash A}$

蘊含關係（entailment relation）

蘊含關係是一種特殊的後承關係。它是基於賦值系統定義的。在賦值系統 $mathcal{M}=langle M,D,F angle$ 中，我們稱 $GammavDash_mathcal{M} A$ ，當對於任意一個指派函數 $a$ 來說，我們有，如果對於每個 $BinGamma$ ， $v_a(B)=D$ ，那麼 $v_a(A)=D.$

健全性/可靠性和完備性（soundness and completeness）

如果 $Gammavdash ARightarrow GammavDash A$ ，那麼我們稱 $vdash$ 對於 $vDash$ 來說是健全的。
如果 $GammavDash ARightarrow Gamma vdash A$ ，那麼我們稱 $vDash$ 對於 $vdash$ 來說是完備的。

我們還需要注意區分完備（complete）和完全（complete），雖然兩者的英文是一樣的。「完全」出現在「一致性」的定義中。

一致性（consistency）的定義：

對於一個後承關係 $vdash$ 來收，我們說句子集合 $Gamma$ 是

否定一致（negation consistent）的，如果不存在可以讓 $Gammavdash A$ 和 $Gammavdash eg A$ 同時成立的 $A$
絕對一致（absolutely consistent）的，如果存在 $A$ ，使得 $Gamma otvdash A$
最大否定一致（maximally negation consistent）的，如果1） $Gamma$ 是否定一致的，2）如果 $Gamma otvdash A$ ，那麼 $Gammacup{A}$ 不是否定一致的
完全（complete）的，如果對於所有 $A$ ，抑或 $Gammavdash A$ ，抑或 $Gammavdash eg A$

在經典邏輯、直覺主義邏輯和模態邏輯 $S4$ 中，否定一致性等同於絕對一致性，最大否定一致性則等同於否定一致性加上完全性。

目錄：類型論驛站寫作計劃

上一篇：證明論學習筆記4：直覺主義邏輯和相繼式演算

參考文獻：

Handbook of Logic in Computer Science