時(shí)態(tài)德摩根邏輯的語義與證明論*

梁飛

中山大學(xué)邏輯與認(rèn)知研究所

中山大學(xué)哲學(xué)系

liangf25@mail2.sysu.edu.cn

1 引言

德摩根代數(shù)又稱擬布爾代數(shù)（quasi-Boolean algebras）、分配i-格（distributive i-lattice），它是帶德摩根否定的分配格，是布爾代數(shù)的弱化。德摩根代數(shù)最早由莫斯?fàn)枺℅.Moisil）在1935年提出（[19]），之后它在邏輯與代數(shù)領(lǐng)域中得到廣泛研究（[1,2,6,20]）。類似于二值代數(shù)與布爾代數(shù)的關(guān)系，德摩根代數(shù)與四值代數(shù)4（見下圖）關(guān)系密切，卡爾曼（J.A.Kalman）（[17]）證明了4（[17]中為D）是德摩根代數(shù)的一個(gè)子直不可歸約代數(shù)（subdirectly irreducible algebras），每一個(gè)德摩根代數(shù)均能嵌入4的直積（direct product）中。

貝爾納普（N.Belnap）在研究相干性與推衍（entailment）時(shí)（[21]）認(rèn)識(shí)到德摩根代數(shù)是一度蘊(yùn)涵（first-degree implication）系統(tǒng)Rfde的代數(shù)語義模型。鄧恩（M.Dunn）在[8]中證明了Rfde相對于4是可靠且完全的。隨后，在[3,4]中，貝爾納普創(chuàng)造性地給出了四值代數(shù)的直觀解釋。他將n解釋為“缺乏信息”，將b解釋為“矛盾信息”。鄧恩在此基礎(chǔ)上，進(jìn)一步給出了四值邏輯的關(guān)系語義模型。（[7,9,10]）貝爾納普和鄧恩的這一系列工作使四值邏輯在邏輯學(xué)、計(jì)算機(jī)科學(xué)、人工智能等領(lǐng)域均受到大量關(guān)注，四值邏輯也被稱作“貝爾納普-鄧恩”（Belnap-Dunn）邏輯。

如果在布爾代數(shù)上加入一元時(shí)態(tài)算子G（將來總是…）、H（過去總是…）及其對偶算子F（過去可能…）、P（將來可能…），那么所得到的結(jié)構(gòu)就是時(shí)態(tài)代數(shù)（Tense algebras）。時(shí)態(tài)代數(shù)所對應(yīng)的邏輯是極小時(shí)態(tài)邏輯Kt。相應(yīng)地，費(fèi)加羅（A.V.Figallo）與佩萊特（G.Pelaitay）研究了帶有一元時(shí)態(tài)算子的德摩根代數(shù)（[11]），稱之為時(shí)態(tài)德摩根代數(shù)（Tense De Morgan algebras）。他們從代數(shù)的角度證明了時(shí)態(tài)德摩根代數(shù)的表示定理、拓?fù)鋵ε迹╠uality）定理，并在此基礎(chǔ)上刻畫了該結(jié)構(gòu)的同余（congruence）關(guān)系。本文將從邏輯的角度研究時(shí)態(tài)德摩根代數(shù)。首先給出時(shí)態(tài)德摩根代數(shù)所對應(yīng)的邏輯：時(shí)態(tài)德摩根邏輯（DMt）。其次給出該邏輯的關(guān)系語義，證明DMt在該語義下的可靠性與完全性。最后，本文還從證明論的角度研究時(shí)態(tài)德摩根邏輯的顯示演算（display calculus），并證明該演算切割消除定理及子結(jié)構(gòu)性質(zhì)。

2 時(shí)態(tài)德摩根邏輯的代數(shù)語義

定義1([11])一個(gè)德摩根代數(shù)（簡稱DM-代數(shù)）是A=(A,∧,∨,～,1,0)，其中(A,∧,∨,1,0)是有界分配格，且滿足以下4個(gè)條件：對任意a,b∈A，

定義2([11])一個(gè)時(shí)態(tài)德摩根代數(shù)（簡稱DMt-代數(shù)）是A=(A,∧,∨,～,G,H,1,0)，其中(A,∧,∨,～,1,0)是德摩根代數(shù)，G,H是定義在A上的一元算子且滿足以下條件:對任意a,b∈A，

(T1)G(1)=1，H(1)=1；

(T2)G(a∧b)=G(a)∧G(b)，H(a∧b)=H(a)∧H(b)；

(T3)a≤GP(a),a≤HF(a)，其中F(a):=～G～(a),P(a):=～H～(a)；

(T4)G(a∨b)≤G(a)∨F(b)，H(a∨b)≤H(a)∨P(b)。

DMt-代數(shù)構(gòu)成了時(shí)態(tài)德摩根代數(shù)簇，下文中我們用DMT代表該代數(shù)簇。

推論1([11])以下命題在DMt-代數(shù)中成立：對任意a,b∈A，

(T5)如果a≤b，那么G(a)≤G(b)且H(a)≤H(b)；

(T6)如果a≤b，那么P(a)≤P(b)且F(a)≤F(b)；

(T7)F(0)=0，P(0)=0；

(T8)F(a∨b)=F(a)∨F(b)，P(a∨b)=P(a)∨P(b)；

(T9)PG(a)≤a，F(xiàn)H(a)≤a；

(T10)G(a)∧F(b)≤F(a∧b),H(a)∧P(b)≤P(a∧b)。

易知，若DMt-代數(shù)滿足a∧～a≤0或1≤a∨～a，則其為時(shí)態(tài)代數(shù)。

定義3(時(shí)態(tài)德摩根邏輯語言)給定可數(shù)無窮原子命題集Prop，時(shí)態(tài)德摩根邏輯（記作DMt）語言遞歸定義如下：

其中p∈Prop。下文中我們用Fm代表DMt公式集。

令F::=～G～，P::=～H～。

定義4(公理系統(tǒng))DMt公理系統(tǒng)定義如下：

1.公理

2.規(guī)則

推論2以下矢列在DMt中可證：

定義5稱矢列A?B在系統(tǒng)S中可證（記作A?SB），如果存在一個(gè)由公理開始的證明序列，序列中的每一個(gè)元素要么是公理，要么由規(guī)則得到。

定義6(賦值及有效)任給時(shí)態(tài)德摩根代數(shù)A=(A,∧,∨,～,G,H,1,0)，稱σ:Prop→A是A中的賦值函數(shù)。對任意A∈Fm，Aσ遞歸定義如下：

稱A?B在代數(shù)A中有效（記作A|=A?B），如果對任意A中賦值σ，Aσ≤Bσ，其中≤是A中的格序。任給代數(shù)類K，稱A?B在代數(shù)類K中有效(記作:K|=A?B)，如果對任意A∈K，A|=A?B。

定理1任給矢列A?B，A?DMtB當(dāng)且僅當(dāng)DMT|=A?B。

證明：根據(jù)林登鮑姆-塔斯基（Lindenbaum-Tarski）證明易得。 □

下面我們證明DMt的系統(tǒng)性質(zhì)。

定義7(推演)任給Γ∪{A}?Fm，稱Γ?A是DMt的推演，如果存在有窮集合Δ?Γ，使得∧Δ?A可證。

推論3以下命題成立：

(1)如果Γ?A且Γ?B，那么Γ?A∧B；

(2)如果?！葅A}?C且Γ∪{B}?C，那么Γ∪{A∨B}?C；

(3)如果Γ?A且Δ∪{A}?C，那么Γ∪Δ?C。

證明：(1)設(shè)Γ?A，據(jù)推演定義可知，存在有窮集Γ1?Γ，使得∧Γ1?A(i)。同理可得，存在有窮集Γ2?Γ，使得∧Γ2?B。據(jù)(A6)、(R1)和(i)得∧Γ1∧∧Γ2?A，同理有∧Γ1∧∧Γ2?B。據(jù)(R2)，∧Γ1∧∧Γ2?A∧B，因?yàn)棣?∪Γ2?Γ且有窮，得證。(2)與(3)證明與之類似，從略。 □

下面給出理論與對偶理論的定義及性質(zhì)。

定義8任給Σ?Fm，稱Σ是DMt的理論，如果Σ滿足以下條件:

(1)Σ/=?；

(2)如果A∈Σ且A?B，那么B∈Σ；

(3)如果A∈Σ且B∈Σ，那么A∧B∈Σ。

定義9任給Σ??Fm，稱Σ?是DMt的對偶理論，如果Σ?滿足以下條件:

(1)Σ?/=?；

(2)B∈Σ?且A?B，那么A∈Σ?；

(3)如果A∈Σ?且B∈Σ?，那么A∨B∈Σ?。

定義10設(shè)Σ是DMt的理論，稱Σ是DMt的一致素理論，如果Σ滿足以下條件:

(1)⊥/∈Σ；

(2)如果A∨B∈Σ，那么A∈Σ或B∈Σ。

推論4如果Γ是一致素理論，那么是對偶理論，其中Γ是Γ的補(bǔ)集。

證明：設(shè)B∈且A?B，欲證A∈。假設(shè)A∈/，那么A∈Γ。故B∈Γ，且B∈/Γ，與題設(shè)條件矛盾，故A∈。如果A∈且B∈，假設(shè)A∨B∈/，那么A∨B∈Γ，因?yàn)棣Ｊ撬乩碚?，故A∈?；駼∈Γ，矛盾。 □

引理1如果Γ?B且⊥/∈Γ，那么存在一致素理論Σ，使得Γ?Σ且B/∈Σ。

證明：枚舉所有的DMt公式：A0,A1,...,Σ的構(gòu)造如下：

根據(jù)構(gòu)造，易知Σ?B，且⊥/∈Σ?，F(xiàn)證Σ是一個(gè)理論。

如果Ai∈Σ且Ai?Aj，假設(shè)Aj/∈Σ，那么Σj∪{Aj}?B。因?yàn)锳i?Aj，據(jù)推論3(3)，得Σj∪{Ai}?B，故Σ?B，矛盾。假設(shè)Ai,Aj∈Σ且Ai∧Aj/∈Σ，易知Σij∪{Ai∧Aj}?B。不失一般性，設(shè)i≤j，根據(jù)構(gòu)造可知Ai,Aj∈Σj，所以Σj?Ai且Σj?Aj，據(jù)推論3(1)，Σj?Ai∧Aj。據(jù)推論3(3)，得Σij∪Σj?B，故Σ?B，矛盾。綜上，Σ是一個(gè)理論。

現(xiàn)證Σ是素理論。假設(shè)Ai∨Aj∈Σ，Ai/∈Σ且Aj/∈Σ。不失一般性，設(shè)i≤j，那么Σj∪{Ai}?B且Σj∪{Aj}?B。據(jù)推論3(2)有Σj∪{Ai∨Aj}?B，又因?yàn)棣瞛∪{Ai∨Aj}?Σ，所以Σ?B，矛盾。 □

類似地，可證明引理2。

引理2如果Γ是一個(gè)一致理論，Δ是對偶理論，?！搔??，那么存在一致素理論Σ，使得Γ?Σ且Σ∩Δ=?。

引理3對任意Γ?Fm，如果Γ/=?且對∨封閉，那么存在對偶理論Σ?，使得Γ?Σ?。

證明：令Σ?={A∈Fm|A?B，其中B∈Γ}。顯然，Γ?Σ?，Σ?/=?。下證Σ?是對偶理論。設(shè)A1∈Σ?且A2?A1，據(jù)構(gòu)造存在B∈Γ，A1?B。據(jù)(R1)得，A2?B，故A1∈Σ?。設(shè)A1∈Σ?且A2∈Σ?，據(jù)構(gòu)造存在B1,B2∈Γ，A1?B1且A2?B2，據(jù)(A9)(R1)得，A1?B1∨B2且A2?B1∨B2，據(jù)(R3)，A1∨A2?B1∨B2。又因Γ對∨封閉，故B1∨B2∈Γ，故A1∨A2∈Σ?。 □

3 時(shí)態(tài)德摩根邏輯的關(guān)系語義

本節(jié)我們將給出DMt的關(guān)系語義，定義其框架、模型及滿足關(guān)系，進(jìn)而證明DMt的可靠性與完全性。

定義11(框架及模型)稱F=(W,≤,g,R,R-1)是時(shí)態(tài)德摩根框架，如果F滿足以下條件:對任意w1,w2∈W,

(F1)(W,≤)是一個(gè)偏序結(jié)構(gòu)；

(F2)g:W→W，使得:如果w1≤w2，那么g(w2)≤g(w1)；

(F3)對任意w∈W，gg(w)=w；

(F4)(≤?R)?(R?≤)；

(F5)(≤?R-1)?(R-1?≤)；

(F6)如果(w1,w2)∈R，那么(g(w1),g(w2))∈R。

定義賦值V:Prop→?(W)↑，其中?(W)↑意為：如果w1∈?(W)且w1≤w2，那么w2∈?(W)，并稱M=(F,V)是時(shí)態(tài)德摩根模型。

框架中g(shù)函數(shù)為對合函數(shù)（involutive），最早由拉西娃（H.Rasiowa）在[6]中研究德摩根代數(shù)的表示定理時(shí)提出，用以解釋德摩根否定。需要注意的是，因?yàn)榈履Ω壿嬛忻苈膳c排中律的失效，各可能世界之間并不是反鏈（anti-chain）關(guān)系，而是偏序關(guān)系，因此模型中的賦值需要對該偏序關(guān)系保持。(F4)與(F5)保證了該框架所定義的賦值是上升集，(F6)保證了G與F，H與P之間能夠相互定義。

定義12(滿足及有效)對任意公式A∈Fm，滿足關(guān)系定義如下：

(1)M,w??；

(2)M,w?⊥；

(3)M,w?p當(dāng)且僅當(dāng)w∈V(p)；

(4)M,w?～A當(dāng)且僅當(dāng)g(w)?A；

(5)M,w?GA當(dāng)且僅當(dāng)對任意w′∈W，如果w′∈R(w)，那么w′?A；

(6)M,w?HA當(dāng)且僅當(dāng)對任意w′∈W，如果w′∈R-1(w)，那么w′?A；

(7)M,w?A∧B當(dāng)且僅當(dāng)w?A且w?B；

(8)M,w?A∨B當(dāng)且僅當(dāng)w?A或w?B。

根據(jù)F,P定義，易知：

(9)M,w?FA當(dāng)且僅當(dāng)存在v∈W，使得v∈R(w)且v?A；

(10)M,w?PA當(dāng)且僅當(dāng)存在v∈W，使得v∈R-1(w)且v?A。

賦值V:Prop→?(W)↑可唯一地?cái)U(kuò)展至V′:Fm→?(W)，故M,w?A當(dāng)且僅當(dāng)w∈V′(A)。若V′(A)?V′(B)，則稱模型M滿足A?B。若對F上的任意模型M，M滿足A?B，則稱A?B在框架類F上有效，記作A?B。

命題1對任意w∈W，如果w∈V′(A)且w≤w′∈W，那么w′∈V′(A)。

證明：施歸納于公式A的復(fù)雜度。當(dāng)A=p,⊥,?時(shí)，據(jù)滿足關(guān)系定義可得。當(dāng)A=A1∧A2或A=A1∨A2時(shí)，據(jù)歸納假設(shè)易得。

當(dāng)A=～B時(shí)，w∈V′(～B)。據(jù)滿足關(guān)系定義g(w)/∈V′(B)。又因?yàn)閣≤w′，據(jù)(F2)，得g(w′)≤g(w)。據(jù)歸納假設(shè)，g(w′)/∈V′(B)，即w′∈V′(～B)。

當(dāng)A=GB時(shí)，w∈V′(GB)。據(jù)滿足關(guān)系定義R(w)?V′(B)。對任意x∈W，如果x∈R(w′)，因?yàn)閣≤w′，那么(w,x)∈(≤?R)。據(jù)(F4)，存在z∈W使得z∈R(w)且z≤x。易見z∈V′(B)，據(jù)歸納假設(shè)得x∈V′(B)，故R(w′)?V′(B)，即w′∈V′(GB)。A=HB時(shí)證明與之類似。 □

定義13(典范框架與典范模型)稱Fc=(Wc,?,g,RG,RH)為一個(gè)時(shí)態(tài)德摩根典范框架，如果Fc滿足以下條件:對任意X,Y∈Wc,

(C1)Wc={X:X是一致素理論}；

(C2)g(X)={A∈Fm|～A/∈X}；

(C3)(X,Y)∈RG當(dāng)且僅當(dāng)G-(X)?Y?F-(X)；

(C4)(X,Y)∈RH當(dāng)且僅當(dāng)H-(X)?Y?P-(X)。

定義賦值Vc:Prop→?(Wc),Vc(p)={X∈Wc|p∈X}，并稱Mc=(Fc,Vc)為一個(gè)時(shí)態(tài)德摩根典范模型。

上述定義中，G-(X)={A|GA∈X}，F(xiàn)-(X),H-(X),P-(X)定義類似。由推論 2的 (7)、(9)、(11)、(13)及 (R6)、(R7)可得：

推論5G-(X)，H-(X)是理論，是對偶理論。

為了證明系統(tǒng)的完全性，我們首先來證明上述定義下的框架是一個(gè)時(shí)態(tài)德摩根框架。顯然，(Wc,?)是一個(gè)偏序結(jié)構(gòu)，(F1)成立。下證(F2)-(F6)成立。

引理4對任意X,Y∈Wc，以下命題成立：

(1)g(X)∈Wc，且gg(X)=X；

(2)如果X?Y，那么g(Y)?g(X)。

證明：(1)欲證g(X)∈Wc，即證明g(X)是一致素理論。設(shè)⊥∈g(X)，據(jù)定義～⊥/∈X。又據(jù)推論2(2)，得?/∈X。因?yàn)閄/=?及(A2)，?∈X，矛盾。故g(X)是一致的。

現(xiàn)證g(X)是一個(gè)理論。設(shè)A∈g(X)且A?B(i)，那么～A/∈X，根據(jù)推論2(4)、(R1)、(R4)和(i)得：～B?～A，故～B/∈X，所以B∈g(X)。設(shè)A∈g(X)那么～A/∈X，同理可得，B∈g(X)那么～B/∈X。因?yàn)閄是素理論，所以～A∨～B/∈X。根據(jù)推論2(6)得～(A∧B)/∈X，即(A∧B)∈g(X)。

現(xiàn)證g(X)是素理論。設(shè)A∨B∈g(X)，那么～(A∨B)/∈g(X)。據(jù)推論2(5)得：～A∧～B/∈g(X)。因?yàn)閄是理論，所以～A/∈g(X)或～B/∈g(X)，即A∈g(X)或B∈g(X)。故g(X)是素理論。

下證gg(X)=X。

(?)：設(shè)A∈gg(X)，那么～A/∈g(X)，那么～～A∈X，根據(jù)推論2(1)得：A∈X。

(?)：設(shè)A∈X，根據(jù)推論2(4)及X可得：～～A∈X。據(jù)定義有～A/∈g(X)，那么A∈gg(X)。

(2)設(shè)X?Y且A∈g(Y)，據(jù)定義有～A/∈Y，那么～A/∈X，即A∈g(X)?！?/p>

引理5任取X,Y∈Wc，(X,Y)∈RG當(dāng)且僅當(dāng)(Y,X)∈RH。

證明：(?)如果(X,Y)∈RG，即G-X?Y?F-X，假設(shè)HA∈Y，欲證A∈X。由HA∈Y可得：HA∈F-X。據(jù)定義有：FHA∈X，據(jù)(A13)得A∈X，即H-Y?X?，F(xiàn)證明X?P-Y，即設(shè)A∈X，欲證PA∈Y。據(jù)(A10)，得GPA∈X。據(jù)定義，有PA∈G-X，故PA∈Y。(?)證明類似，從略。 □

引理6任取X,Y∈Wc，以下命題成立：

(3)如果(X,Y)∈RG，那么(g(X),g(Y))∈RG。

證明：(1)令X,Z,Y∈Wc，X?Z且(Z,Y)∈RG，那么G-(Z)?Y?F-(Z)，據(jù)定義得，G-(X)?G-(Z)?Y。令Δ′={A0∨...∨An∨B0∨...∨Bm|顯然且Δ′對∨封閉。據(jù)引理3得，存在對偶理論Δ，使得Δ′?Δ。下證:G-(X)∩Δ=?。

假設(shè)G-(X)∩Δ/=?，那么存在A∈G-(X)(i)且A∈Δ。據(jù)Δ構(gòu)造可得，存在D=A0∨...∨An∨B0∨...∨Bm∈Δ′，使得A?D，其中A0...An∈B0...Bm∈又據(jù)引理4和推論5，A0∨...∨An∈Y(ii)且B0∨...∨Bm∈F-(X)(iii)。據(jù)(R6)，GA?GD，即GA?G(A0∨...∨An∨B0∨...∨Bm)。由 (i)可得，GA∈X，故 G(A0∨...∨An∨B0∨...∨Bm)∈X。據(jù) (A14)，G(A0∨...∨An)∨F(B0∨...∨Bm)∈X。因?yàn)閄是素理論，故G(A0∨...∨An)∈X或F(B0∨...∨Bm)∈X。

如果G(A0∨...∨An)∈X，那么A0∨...∨An∈G-(X)，據(jù)題設(shè)條件，A0∨...∨An∈Y，即矛盾于(ii)。如果F(B0∨...∨Bm)∈X，那么B0∨...∨Bm∈F-(X)，即矛盾于 (iii)。故G-(X)∩Δ = ?，據(jù)引理2可得：存在一致素理論Σ，使得G-(X)?Σ且Σ∩Δ=?，故且因此G-(X)?Σ?F-(X)且Σ?Y。故(??RG)?(RG??)。(2)與(1)證明類似，從略。

(3)設(shè)(X,Y)∈RG，那么G-(X)?Y?F-(X)。欲證G-(g(X))?g(Y)?F-(g(X))。假設(shè)G-(g(X))?g(Y)，那么存在A∈G-(g(X))且A/∈g(Y)，根據(jù)定義有：～GA/∈X且～A∈Y。據(jù)題設(shè)條件可知F～A∈X。因?yàn)镕～A?～GA，所以～GA∈X，矛盾。同理可證，g(Y)?F-(g(X))。 □

由引理2與引理5立得：

命題2時(shí)態(tài)德摩根典范框架是時(shí)態(tài)德摩根框架。

引理7任給X∈Wc，Mc,X?A當(dāng)且僅當(dāng)A∈X。

證明：施歸納于公式A的復(fù)雜度。A=p,?,⊥時(shí)，據(jù)典范模型定義可得。A=A1∨A2或A1∧A2時(shí)，據(jù)歸納假設(shè)易得，證明從略。

當(dāng)A=～B時(shí)，Mc,X?～B，據(jù)滿足關(guān)系定義，Mc,g(X)?B。據(jù)歸納假設(shè)，B∈g(X)，又據(jù)g定義，～B/∈X。

當(dāng)A=GB時(shí)，先證從右向左。設(shè)Mc,X?GB，據(jù)滿足關(guān)系定義，存在Y∈Wc，Y∈RG(X)且Mc,Y?B。據(jù)RG定義，G-(X)?Y?F-(X)且Mc,Y?B。據(jù)歸納假設(shè)，B/∈Y，故B/∈G-(X)，據(jù)定義，得GB/∈X。

再證從左向右。設(shè)GB/∈X，那么B/∈G-X。令與引理6(1)證明類似，存在對偶理論Δ，使得Δ′?Δ且G-(X)∩Δ =?。據(jù)推論2，可知存在一致素理論Y，使得G-(X)?Y且Y∩Δ=?，故Y∩F-(X)=?。因此G-(X)?Y?F-(X)且B/∈Y。據(jù)歸納假設(shè)及RG定義，Mc,X?GB。

當(dāng)A=HB時(shí)，證明與之類似，從略。 □

定理2A?B當(dāng)且僅當(dāng)A?B。

證明：(?)即可靠性證明，證明方法如常。這里僅舉例說明：

如果A?GPA，任給模型M，欲證V′(A)?V′(GPA)。即證明：任取w∈W，如果w∈V′(A)，那么w∈V′(GPA)。假設(shè)w/∈V′(GPA)，據(jù)滿足關(guān)系得R(w)?V′(PA)，即存在z∈R(w)且z/∈V′(PA)。那么R-1(z)∩V′(A)=?，故w/∈R-1(z)，這與z∈R(w)矛盾。

如果(R4)成立，任給模型M，欲證：如果V′(A)?V′(～B)，那么V′(B)?V′(～A)。假設(shè)V′(B)?V′(～A)，即存在w∈V′(B)且w/∈V′(～A)。據(jù)滿足關(guān)系得g(w)∈V′(A)，那么據(jù)題設(shè)條件得g(w)∈V′(～B)。故gg(w)/∈V′(B)，據(jù)(F3)，w/∈V′(B)，與假設(shè)條件矛盾。

(?)假設(shè)A?B，根據(jù)引理1，存在一致素理論U，使得A∈X且B/∈X。據(jù)引理7，存在典范模型Mc，Mc,X?A且Mc,X?B，即A?B。 □

4 時(shí)態(tài)德摩根邏輯的顯示演算

顯示演算是貝爾納普在[5]提出的，它是對甘岑系統(tǒng)的一般化研究。其基本思想是，區(qū)分公式與結(jié)構(gòu)以及命題聯(lián)結(jié)詞與結(jié)構(gòu)算子。根據(jù)結(jié)構(gòu)算子出現(xiàn)的位置（矢列左邊或右邊）的不同，每一個(gè)結(jié)構(gòu)算子被解釋為不同的聯(lián)結(jié)詞。因?yàn)轱@示規(guī)則的存在，每一個(gè)結(jié)構(gòu)都能夠通過顯示規(guī)則單獨(dú)地出現(xiàn)在矢列的左邊或右邊，即顯示性質(zhì)。這樣使系統(tǒng)地研究切割消除的證明成為可能。貝爾納普提出了滿足顯示演算特點(diǎn)的8個(gè)條件(C1)-(C8)，分別為：

(C1)出現(xiàn)在規(guī)則(R)前提中的每一個(gè)公式都是(R)結(jié)論中某個(gè)公式的子公式。

(C2)同余（congruent）參數(shù)是相同結(jié)構(gòu)的出現(xiàn)。

(C3)每一個(gè)參數(shù)最多與結(jié)論中一個(gè)組成部分為同余關(guān)系，等價(jià)地，結(jié)論中任意兩個(gè)組成部分均不為同余關(guān)系。

(C4)同余參數(shù)要么是矢列的整個(gè)前件，要么是矢列的整個(gè)后件。

(C5)如果出現(xiàn)在規(guī)則(R)結(jié)論中的公式不是參數(shù)的，那么這個(gè)公式要么是矢列的整個(gè)前件，要么是矢列的整個(gè)后件。這樣的公式稱為規(guī)則(R)的主要（principal）公式。

(C6/7)用任意結(jié)構(gòu)對規(guī)則(R)中同余參數(shù)同時(shí)進(jìn)行替換，所得結(jié)果仍是規(guī)則(R)。

(C8)如果規(guī)則(R)與規(guī)則(R′)的結(jié)論分別為:X?A，A?Y，其中A是兩個(gè)規(guī)則的主要公式，且對這兩個(gè)結(jié)論使用切割（Cut）規(guī)則得X?Y。那么X?Y要么與X?A或A?Y相同，要么可以對規(guī)則(R)與規(guī)則(R′)的前提使用切割規(guī)則，其中切割公式是A的真子公式。

除(C8)外，每條性質(zhì)均可根據(jù)系統(tǒng)規(guī)則的形式來判斷。相較于甘岑系統(tǒng)，這樣的形式極大的簡化了切割可消除的證明。在貝爾納普之后，克拉赫特（M.Kracht）系統(tǒng)地研究了顯示演算的表達(dá)力及限度。（[18]）萬辛（H.Wansing）（[22,23]），戈萊（R.Goré）（[12,13]），帕米迦娜（A.Palmigiano）和格里克（G.Greco）（[14-16]）進(jìn)一步拓寬了顯示演算的領(lǐng)域，分別研究了模態(tài)邏輯，子結(jié)構(gòu)邏輯以及多類型顯示演算。

定義14(語言)給定可數(shù)無窮的原子命題集Prop，顯示演算（記作D.DMt）公式遞歸定義如下：

其中，?::=～□～,?::=～■～。D.DMt結(jié)構(gòu)遞歸定義如下：

下文中我們用Stru指代D.DMt系統(tǒng)中結(jié)構(gòu)的集合。D.DMt結(jié)構(gòu)算子的解釋如下：

為了使系統(tǒng)具有顯示性質(zhì)，D.DMt系統(tǒng)引入了A→A和A.-A，相應(yīng)地，在結(jié)構(gòu)中引入了X＞X。在下文中我們將證明該系統(tǒng)是DMt的保守?cái)U(kuò)張。

定義15(規(guī)則)D.DMt的規(guī)則如下：

下面首先證明D.DMt是DMt的保守?cái)U(kuò)張，即對任意A,B∈Fm,A?DMtB，當(dāng)且僅當(dāng)，A?D.DMtB。從左至右易得，只需證明DMt系統(tǒng)的公理及規(guī)則在D.DMt中可證。為了證明反方向成立，我們證明其逆否命題。證明思路如下:首先證明，D.DMt相對于DMt框架是可靠的。根據(jù)結(jié)構(gòu)在矢列左邊與右邊的不同解釋，我們證明X?D.DMtY，那么Xτ?Yτ，其中(·)τ,(·)τ:Stru→Fm。在第3節(jié)中我們已經(jīng)證明，DMt相對于DMt框架是完全的，即A?DMtB，當(dāng)且僅當(dāng)，A?B。因此，如果A?DMtB，根據(jù)完全性有A?B，根據(jù)可靠性得A?D.DMtB，故從右向左方向成立，即D.DMt是DMt的保守?cái)U(kuò)張。

引理8A?A在D.DMt中可證。

證明：施歸納于公式A的復(fù)雜度。

(1)當(dāng)A=p時(shí)，A?A是D.DMt的公理。

(2)當(dāng)A=□B時(shí)，據(jù)歸納假設(shè)可得B?B，

(3)當(dāng)A=■B時(shí)，證明方法與(2)類似；

(4)當(dāng)A=A1∧A2時(shí)，據(jù)歸納假設(shè)可得A1?A1且A2?A2，

(5)當(dāng)A=A1∨A2時(shí)，據(jù)歸納假設(shè)可得A1?A1且A2?A2，

命題3(A1)-(A16)，(R1)-(R7)在D.DMt中可證。

證明：僅舉例說明：(A10)

由引理7和命題3可得：

定理3任給A,B∈LDMt,如果A?DMtB，那么A?D.DMtB。

下面來證明從右向左方向。為了證明D.DMt的可靠性，我們首先給出D.DMt語言中新算子的滿足關(guān)系。令M是一個(gè)時(shí)態(tài)德摩根模型，

·M,w?A.-B當(dāng)且僅當(dāng)存在w′∈W且w′≤w，w′?A且w′?B；

·M,w?A→B當(dāng)且僅當(dāng)對任意w≤w′∈W，w′?A或w′?B。

我們將X?Y解釋為Xτ?Yτ，其遞歸定義如下：

下證D.DMt的可靠性：

定理4如果X?Y在D.DMt中可證，那么Xτ?Yτ有效。

證明：只需證明D.DMt的公理和規(guī)則在時(shí)態(tài)德摩根框架上有效，這里僅舉例說明。

任給模型M，欲證：V′(Xτ∧Yτ)?V′(Zτ)，當(dāng)且僅當(dāng)，V′(Yτ)?V′(Xτ→Zτ)。

(?)假設(shè)V′(Yτ)?V′(Xτ→Zτ)，即存在w∈V′(Yτ)(i)且w/∈V′(Xτ→Zτ)。據(jù)滿足關(guān)系得：存在w≤w′使得：w′∈V′(Xτ)(ii)且w′/∈V′(Zτ)。據(jù)題設(shè)條件，w′/∈V′(Xτ∧Yτ)，那么w′/∈V′(Xτ)或w′/∈V′(Yτ)(iii)。前者與(ii)矛盾。因?yàn)閂′(Yτ)是上升集，據(jù)w≤w′與(i)，得w′∈V′(Yτ)，與(iii)矛盾。

(?)證明類似，從略。

任給模型M，欲證：V′(Xτ)?V′(Yτ∨Zτ)，當(dāng)且僅當(dāng)，V′(Yτ.-Xτ)?V′(Zτ)。

(?)假設(shè)V′(Yτ.-Xτ)?V′(Zτ)，即存在w∈V′(Yτ.-Xτ)且w/∈V′(Zτ)(i)。據(jù)滿足關(guān)系得：存在w′≤w使得：w′/∈V′(Yτ)(ii)且w′∈V′(Xτ)。據(jù)題設(shè)條件，w′∈V′(Yτ∨Zτ)，那么w′∈V′(Yτ)或w′∈V′(Zτ)(iii)。前者與 (ii)矛盾。因?yàn)閂′(Zτ)是上升集，據(jù)w′≤w與(i)，得w′/∈V′(Zτ)，與(iii)矛盾。(?)證明類似，從略。 □

故由定理2,4可得：

定理5任給A,B∈LDMt，如果A?D.DMtB，那么A?DMtB。

接下來我們證明D.DMt具有子公式性質(zhì)，并且切割消除定理在D.DMt成立。如前所述，據(jù)[5]，如果系統(tǒng)滿足(C1)，那么該系統(tǒng)滿足子公式性質(zhì)。如果系統(tǒng)滿足(C1)-(C8)，該系統(tǒng)可證明切割消除。除(C8)外，其他性質(zhì)均可根據(jù)系統(tǒng)規(guī)則形式確定。

下證D.DMt滿足(C8)。

引理9D.DMt滿足(C8)。

證明：施歸納于切割公式復(fù)雜度。

原子命題：

常項(xiàng):

常項(xiàng)⊥的證明類似。

一元聯(lián)結(jié)詞:

■A,?A,?A的證明類似。

二元聯(lián)結(jié)詞:

A∨B、A→B、A.-B證明類似。因此，如果規(guī)則(R)與規(guī)則(R’)的結(jié)論分別為:X?A，A?Y，其中A是兩個(gè)規(guī)則的主要公式，且對這兩個(gè)結(jié)論使用切割(Cut)規(guī)則得X?Y。那么X?Y要么與X?A或A?Y相同，要么可以對規(guī)則(R)與規(guī)則(R’)的前提使用切割規(guī)則，其中切割公式是A的真子公式，即(C8)成立。 □

定理6(切割消除，[5])如果X?Y在D.DMt中可證，那么X?Y的證明中不需要使用(Cut)。

證明：D.DMt滿足(C2)-(C8)。 □

定理7(子公式性質(zhì)，[5])如果X?Y在D.DMt中可證，那么其證明序列中出現(xiàn)的公式均為X,Y中的子公式。

證明：D.DMt滿足(C1)?！?/p>

5 結(jié)論

本文從語義學(xué)及證明論的角度研究了時(shí)態(tài)德摩根邏輯，給出了時(shí)態(tài)德摩根邏輯的關(guān)系語義，證明了該邏輯的可靠性及完全性。本文還構(gòu)建了時(shí)態(tài)德摩根邏輯的顯示演算，同時(shí)證明了該演算具有切割消除定理和子公式性質(zhì)。在此基礎(chǔ)上，我們可以進(jìn)一步推廣[18]中的結(jié)論，在該文中克拉赫特用初始（primitive）公式的概念給出了時(shí)態(tài)邏輯Kt擴(kuò)張顯示化（displaying）的刻畫條件，即:時(shí)態(tài)邏輯的擴(kuò)張可被顯示化，當(dāng)且僅當(dāng)，擴(kuò)張的公理集為初始公式集（參見[18]，定理16）。我們可以用帕米迦娜與格里克等在[15]的定義55中提出的分析遞歸（analytic inductive）公式的概念得到時(shí)態(tài)德摩根邏輯的擴(kuò)張顯示化（displaying）的刻畫條件，即擴(kuò)張的公理集為分析遞歸（analytic inductive）公式集。除此之外，我們可以進(jìn)一步研究不同的時(shí)態(tài)德摩根邏輯擴(kuò)張，如：DM4t、DMS4t等，這有助于我們進(jìn)一步地拓展非經(jīng)典模態(tài)邏輯的視野及其應(yīng)用。

[1]A.Anderson and N.Belnap,1975,Entailment:The Logic of Relevance and Necessity,Vol.1,Princeton and Oxford:Princeton University Press.

[2]O.Arieli and A.Avron,1996,“Reasoning with logical bilattices”,Journal of Logic,Language and Information,5:25-63.

[3]N.Belnap,1976,“How a computer should think”,in G.Ryle(ed.),Contemporary Aspects of Philosophy,pp.30-56,Boston:Oriel Press.

[4]N.Belnap,1977,“A useful four-valued logic”,Modern Uses of Multiple-valued Logic,pp.5-37,Netherlands:Springer.

[5]N.Belnap,1982,“Display logic”,Journal of Philosophical Logic,11(4):375-417.

[6]A.Bialynicki-Birula and H.Rasiowa,1957,“On the representation of quasi-Boolean algebras”,Bulletin of the Polish Academy of Science,5(3):259-261.

[7]K.BimboandM.Dunn,2001,“Four-valuedlogic”,NotreDameJournalofFormalLogic,42(3):171-192.

[8]M.Dunn,1966,The Algebra of Intensional Logics,PhD thesis,University of Pittsburgh.

[9]M.Dunn,1976,“Intuitive semantics for first-degree entailments and coupled trees”,Philosophical Studies,29:149-168.

[10]M.Dunn,1999,“A comparative study of various model-theoretic teartments of negation:A history of formal negation”,in D.Gabbay and H.Wansing(eds.),What is Negation?,pp.23-51,Dordrecht;Boston,Mass.:Kluwer Academic Publishers.

[11]A.V.Figallo and G.Pelaitay,2014,“Tense operators on De Morgan algebras”,Logic Journal of IGPL,22(2):255-267.

[12]R.Goré,1998,“Gaggles,GentzenandGalois:Howtodisplayyourfavouritesubstructurallogic”,Logic Journal of IGPL,6(5):669-694.

[13]R.Goré,1998,“Substructural logics on display”,Logic Journal of IGPL,6(3):451-504.

[14]G.Greco and A.Palmigiano,2016,“Linear logic properly displayed”,https://arxiv.org/abs/1611.04181.

[15]G.Greco,M.Ma,A.Palmigiano,A.Tzimoulis and Z.Zhao,2016,“Unified correspondence as a proof-theoretic tool”,Journal of Logic and Computation,exw022,http://dx.doi.org/10.1093/logcom/exw022.

[16]G.Greco and A.Palmigiano,2017,“Lattice logic properly displayed”,International Workshop on Logic,Language,Information,and Computation,pp.153-169.

[17]J.A.Kalman,1958,“Lattices with involution”,Transactions of the American Mathematical Society,87(2):485-491.

[18]M.Kracht,1996,“Power and weakness of the modal display calculus”,Proof Theory of Modal Logic,pp.93-121,Springer.

[19]G.Moisil,1935,“Recherches sur l’algebre de la logique”,Annales Scientifiques de l’Université de Jassy,22(3):1-117.

[20]H.Rasiowa,1974,An Algebraic Approach to Non-Classical Logics,Amsterdam:North-Holland Co.

[21]J.Spencer and N.Belnap,1966,“Intentionally complemented distributive lattices”,Portugalie Mathematics,25:99-104.

[22]H.Wansing,2013,Displaying Modal Logic,Springer Science Business Media.

[23]H.Wansing,2013,Proof theory of Modal Logic,Springer Science Business Media.