涂保勛

1 引言

正規(guī)模態(tài)邏輯S5 的根岑式矢列演算通常不具有子公式性質(zhì)。運用語義的方法，高野道夫（M.Takana）在[5]中證明了，如果一個矢列可證，那么存在一個推導使得推導中的所有公式都是該矢列中公式的子公式，即證明了S5 的子公式性質(zhì)。高野道夫在[4]中評論說，運用同樣的方法可以證明基本時態(tài)邏輯Kt 的子公式性質(zhì)。模態(tài)邏輯K4 的時態(tài)擴張的子公式性質(zhì)證明參見[2,3]。

非正規(guī)模態(tài)邏輯系統(tǒng)C2 由雷蒙（E.J.Lemmon）在[1]中給出，該系統(tǒng)由命題邏輯的重言式，公理□(φ→ψ)→(□φ→□ψ)和以下兩個規(guī)則組成：

在關(guān)系語義和代數(shù)語義下，該系統(tǒng)的完全性和有窮模型性被證明，雷蒙評論C2 的結(jié)論可以擴張到其他邏輯。在[6]中，C2 被時態(tài)化為C2t，C2t 的可靠性和完全性得到證明。另外，C2t 的加標矢列演算被給出，該演算的可靠性和完全性得到證明。然而在此文章中，C2t 的有窮模型性和可判定性問題沒有得到證明。本文將構(gòu)建C2t 的根岑式矢列演算，運用高野道夫的語義方法證明C2t 的子公式性質(zhì)，進而證明C2t 的有窮模型性和可判定性。另外，本文還將證明C2t 的插值性質(zhì)。

本文的結(jié)構(gòu)如下。第二部分介紹非正規(guī)邏輯C2t 的語型和語義。第三部分給出C2t 的矢列演算GC2t。第四部分證明GC2t 的子公式性質(zhì)，有窮模型性和可判定性。第5 部分證明GC2t 的插值性質(zhì)。

2 句法和語義

定義2.1.令Prop是命題變元的無窮集合，公式集L遞歸定義如下：

其中p ∈Prop。定義?φ:=φ→⊥，?:=⊥→⊥，φ ?ψ:=(φ→ψ)∧(ψ→φ)?！螃盏膶ε级x為◇φ:=?□?φ。?φ的對偶定義為?φ:=?■?φ。

定義2.2.一個正則框架是一個四元組=(W,N,RF,RP)，其中W是非空集，N ?W是正規(guī)時間點（世界）的集合，RF和RP是W上滿足以下條件的二元關(guān)系：

一個正則模型是一個二元組M=(F,V)，其中F 是正則框架，V:Prop→?(W)是一個賦值函數(shù)。

定義2.3.給定一個公式φ ∈L，一個正則模型M=(,V)，和一個點w ∈W，公式φ在w上真（記為M,w?φ）遞歸定義如下：

M,w?p當且僅當w ∈V(p)，其中p ∈Prop，

M,w?⊥，

M,w?φ ∧ψ當且僅當M,w?φ并且M,w?ψ，

M,w?φ ∨ψ當且僅當M,w?φ或者M,w?ψ，

M,w?φ→ψ當且僅當M,w?φ或者M,w?ψ，

M,w?□φ當且僅當w ∈N并且?u ∈W(RFwu ?M,u?φ)，

M,w?■φ當且僅當w ∈N并且?u ∈W(RPwu ?M,u?φ)。

特別地，M,w?□?當且僅當w ∈N。M,w?■?當且僅當w ∈N。

稱一個公式φ在M 上可滿足，如果存在w ∈W使得M,w?φ。稱φ在M 上真，記為M ?φ，如果對任意w ∈W都有M,w?φ。稱公式φ在一個正則框架上有效，記為?φ，如果對任意上的賦值V并且對所有w ∈W，(,V),w?φ。

稱一個公式φ相對于一個正則框架類C 有效，記為C ?φ，如果對所有F∈C，?φ。給定任意公式集Γ 和任意公式φ，稱φ是Γ 的邏輯后承，記為Γ ?φ，如果對任意正則模型M 和任意w ∈W，M,w?Γ 蘊含M,w?φ。

定義2.4.希爾伯特式公理系統(tǒng)HC2t 在[6]中給出，該系統(tǒng)由如下公理模式和推理規(guī)則組成：

(1)公理：

(2)推理規(guī)則：

給定公式φ和公式集Γ，相對于系統(tǒng)HC2t，稱φ是Γ 的演繹后承，記為Γ?HC2tφ，如果存在一個有窮集合Γ′ ?Γ 使得∧?！洹?∈HC2t，其中∧?！涫铅！渲兴泄降暮先?。當Γ=?，記為?HC2tφ。

命題2.1.對任意公式φ和ψ，以下三條成立：

命題2.2(可靠性). 對任意公式φ ∈L，如果HC2t?φ，那么?φ。

證明.需驗證HC2t 的公理有效并且推理規(guī)則保持有效性。給定任意正則框架F，令V是上的任意賦值并且w是上的任意點。以下驗證公理(ad1)的有效性和規(guī)則(Mon□)保持有效性。

定理2.1(完全性). HC2t 相對于所有正則框架類是強完全的。

證明.運用典范模型方法，在[6]中已被證明。

3 HC2t 的矢列演算

令Γ,Δ 等（有或者無下標）表示有窮可重公式集。一個矢列是形如Γ ?Δ的表達式，其中Γ 和Δ 都是有窮的非空的可重公式集。一個矢列規(guī)則是以下形式的表達式：

其中Γi?Δi(1 ≤i≤n)稱為(R)的前提，Γ0?Δ0稱為(R)的結(jié)論。

定義3.1.HC2t 的矢列演算GC2t 由以下公理模式和矢列規(guī)則組成：

(1)公理模式：

(2)聯(lián)結(jié)詞規(guī)則：

(3)結(jié)構(gòu)規(guī)則：

(4)切割規(guī)則：

(5)模態(tài)規(guī)則：

在GC2t 中，一個推導D是由矢列組成的有窮樹結(jié)構(gòu)，其中每個節(jié)點要么是公理，要么是從子節(jié)點矢列使用某個規(guī)則得到的。稱矢列Γ ?Δ 在GC2t 中可推導（記為：GC2t?Γ ?Δ），如果在GC2t 中存在推導D使得D的根節(jié)點為Γ ?Δ。稱推理規(guī)則(R)可允許，如果(R)的結(jié)論(Γ0?Δ0)不可推導，那么(R)的前提(Γi?Δi)不可推導。

定義3.2.給定任意正規(guī)模型M=(,V)，w ∈M，稱矢列Γ ?Δ 在w上真（記為：M,w?Γ ?Δ），如果M,w?∧?！纽ぁ７Q一個矢列規(guī)則在模型上保真，如果在模型上前提真蘊含結(jié)論真。稱矢列Γ ?Δ 是有效的（記為：?Γ ?Δ），如果∧Γ→∨Δ 是有效式。

命題3.1(可靠性). 對任意矢列Γ ?Δ，如果GC2t?Γ ?Δ，那么?Γ ?Δ。

證明.容易驗證GC2t 的公理都是有效的并且推導規(guī)則保持有效性。

引理3.1.如果HC2t?α，那么GC2t??α。

證明.假設(shè)HC2t?α，則在HC2t 中存在一個推導D。對D的長度歸納證明??α。設(shè)|D|=0，則α在HC2t 中是公理。公理(K)和(N)容易驗證，這里只驗證公理(ad1)。(ad1)的推導如下：

設(shè)|D| ＞0，則α從ψ→α和α由(MP)得到。由歸納假設(shè)得GC2t??ψ并且GC2t??ψ→α。?α的推導如下：

定理3.2.GC2t?Γ ?Δ 當且僅當HC2t?∧Γ→∨Δ。

證明.從右到左，設(shè)HC2t?∧?！纽?。由引理3.1 得GC2t??∧?！纽?。顯然GC2t?Γ ?∧Γ 并且GC2t?∧Γ,∧Γ ?∨Δ。由(Cut)得GC2t?Γ ?∨Δ。顯然，GC2t?∨Δ ?Δ。由(Cut)得GC2t?Γ ?Δ。另一個方向，設(shè)GC2t?Γ ?Δ。那么在GC2t 中存在Γ ?Δ 的推導D。對|D|歸納證明HC2t?∧?！纽?。設(shè)|D|=0。則矢列Γ ?Δ 是公理。對每條GC2t 的公理，容易驗證HC2t?∧?！纽?。設(shè)|D| ＞0。則矢列Γ ?Δ 由規(guī)則(R)得到。其他情況容易驗證，這里只驗證規(guī)則(adF)。在這種情況下，推導的最后一步是：

由歸納假設(shè)得HC2t?□?∧∧?Θ∧∧Σ→φ。由Mon□得HC2t?□(□?∧∧?Θ∧∧Σ)→□φ。因為HC2t?□?∧∧□?Θ∧∧□Σ→□(□?∧∧?Θ∧∧Σ)。因此HC2t?□?∧∧□?Θ∧∧□Σ→□φ。因為HC2t?□?∧∧Θ∧∧□Σ→□?∧∧□?Θ∧∧□Σ。因此HC2t?□?∧∧Θ∧∧□Σ→□φ。

定理3.3(完全性). 令CF 表示所有正則框架類，如果CF ?Γ ?Δ，那么GC2t?Γ ?Δ。

證明.設(shè)CF ?Γ ?Δ。則CF ?∧Γ→∨Δ。由HC2t 的完全性得HC2t?∧Γ→∨Δ。由定理3.2 得GC2t?Γ ?Δ。

4 子公式性質(zhì)和可判定性

令Γ 為有窮可重公式集。Sf(Γ)表示Γ 的所有子公式的集合。稱一個可推導的矢列Γ ?Δ 有子公式性質(zhì)，如果存在一個推導D使得D中出現(xiàn)的公式都屬于Sf(Γ,Δ)。稱一個矢列演算具有子公式性質(zhì)，如果對該演算中任意可推導的矢列Γ ?Δ，存在一個推導D使得D中出現(xiàn)的公式都屬于Sf(Γ,Δ)。在GC2t 中，顯然規(guī)則(Cut)、(adF)和(adP)不具有子公式性質(zhì)。本節(jié)的目標是證明GC2t 的子公式性質(zhì)。為此，我們將要證明，如果一個矢列Γ ?Δ 在GC2t 中可推導，那么存在一個該矢列的推導D使得D中出現(xiàn)的公式都屬于Sf(Γ,Δ)。

定義4.1.令Ξ 是子公式封閉的有窮公式集。稱一個矢列Γ ?Δ 在GC2t 中Ξ-可證，如果存在一個該矢列的推導D使得D中出現(xiàn)的公式都屬于Ξ。令a,b為Ξ的兩個子集，稱二元組(a,b)Ξ-不相交，如果a ?b不是Ξ-可證的。稱一個矢列a ?b是Ξ-飽和的，如果(a,b)Ξ-不相交并且滿足如下條件：

(1)如果φ,a ?b不是Ξ-可證的，那么φ ∈a。

(2)如果a ?b,φ不是Ξ-可證的，那么φ ∈b。

稱公式集a ?Ξ 是Ξ-飽和的，如果二元組(a,Ξa(chǎn))在GC2t 中是Ξ-飽和的。在這一節(jié)的后面部分，我們會一直使用Ξ 表示子公式封閉的有窮公式集。另外，給定任意公式集a ?Ξ，用ac表示Ξa(chǎn)。

引理4.1.如果(a,b)在GC2t 中Ξ-不相交，那么存在Ξ-飽和的二元組(a+,b+)使得a ?a+并且b ?b+。

證明.令φ1,φ2,...,φm,φm+1,...,φn(1≤m ≤n) 是Ξ 中所有公式的列舉使得φ1,φ2,...,φm是形如□(■)α的公式，φm+1,...,φn不是形如□(■)α的公式。令a0?b0=a ?b。如果GC2t ?ak ?bk,φk，那么令ak+1?bk+1=ak ?bk,φk。如果GC2t?ak ?bk,φk并且GC2t ?ak,φk ?bk，那么令ak+1?bk+1=ak,φk ?bk。否則，令ak+1?bk+1=ak ?bk。

下證an+1?bn+1是Ξ-飽和的。顯然GC2t ?an+1?bk,φn+1。令φ=φi對某個i(1≤i ≤n)。設(shè)GC2t ?φ,an+1?bn+1。顯然GC2t?ak ?bk,φ，否則φ ∈bk+1?bn+1使得GC2t?φ,an+1?bn+1。因為ak ?an+1并且bk ?bn+1，由假設(shè)得GC2t ?φ,ak ?bk。所以φ ∈ak+1?an+1。同理可得φ ∈bn+1。

定義4.2.令Ξ 為子公式封閉的有窮公式集，定義GC2t 的Ξ-模型MΞ如下：

令RF、RP是WΞ上的二元關(guān)系。對任意a,b ∈WΞ并且φ ∈Ξ，稱RF是□-飽和的，如果滿足如下條件：□φ ∈a ?a ∈NΞ并且?b ∈WΞ(RFab ?φ ∈b)。稱RF是?-飽和的，如果滿足以下條件：?φ ∈a ?a/∈NΞ或者?b ∈WΞ(RFba并且φ ∈b)。RP的■(◇)飽和條件類似。

如果RF是□-飽和的并且是?-飽和的，RP是■-飽和的并且是◇-飽和的，那么MΞ=(WΞ,NΞ,RF,RP,VΞ)是GC2t 的Ξ-模型。

引理4.2.令a,b ∈WΞ并且φ,ψ ∈Ξ，以下條件成立：

證明.由Ξ-飽和的定義和GC2t 相應的聯(lián)結(jié)詞規(guī)則，條件(1)到(6)容易證明。

引理4.3.令MΞ是GC2t 的正則Ξ-模型。對所有公式φ ∈Ξ 并且a ∈Ξ，φ ∈a當且僅當MΞ,a?φ。

證明.對公式φ的復雜度歸納證明。原子公式的情況顯然成立。由歸納假設(shè)可得布爾公式的情況。令φ=□ψ。從左到右，設(shè)□ψ ∈a并且RFab。由□-飽和的定義得φ ∈b。由歸納假設(shè)得MΞ,b?ψ。因為b ∈RF(a)。因此MΞ,a?□ψ。從右到左，設(shè)MΞ,a?□ψ并且RFab。由語義定義得MΞ,b?φ。由歸納假設(shè)得φ ∈b。因為RFab。因此□φ ∈a。當φ=■ψ，證明類似。

定義4.3.給定a,b ∈WΞ。令□?∈a并且□?∈b。WΞ上的二元關(guān)系定義如下：

命題4.1.對任意公式集Σ,Θ 和公式φ，以下條件成立：

證明.這里只證明(1)。從右至左，設(shè)GC2t ?□?,Θ,□Σ?□φ。由引理4.1 得□?∈a，Θ?a，□Σ?a并且□φ ∈ac。由假設(shè)得φ ∈bc。如果?θ ∈?Θ，那么θ ∈Θ，并且如果σ ∈Σ，那么□σ ∈□Σ。因為□?∈b。因此GC2t ?□?,?Θ,Σ?φ。從左至右，設(shè)□φ ∈ac。令Θ={θ ∈a |?θ ∈Ξ}并且Σ={σ | □σ ∈a}。因為□?∈a，Θ?a并且□Σ?a。由假設(shè)得GC2t ?□?,Θ,□Σ?□φ。那么GC2t?□?,?Θ,Σ?φ。由引理4.1 得?Θ?a、Σ?a并且φ ∈ac。因此成立。

定義4.4.矢列演算GC2t 在WΞ上的二元關(guān)系定義如下：

命題4.2.令切割規(guī)則(Cut)的切割公式φ ∈Ξ，對任意公式ψ，以下命題成立：

證明.這里只證明(2)。從右至左，設(shè)GC2t ?■Γ ?■φ。由引理4.1 得■Γ?a并且■φ ∈ac。由假設(shè)得存在b ∈WΞ使得并且ψ ∈bc。如果α ∈Γ，那么■α ∈■Γ?a。因為。則α ∈b。因此Γ?b。因此GC2t ?Γ?φ。從左至右，設(shè)■φ ∈ac。令Γ={α |■α ∈a}。因為■Γ?a并且■φ ∈ac。則GC2t?■Γ ?■φ。由假設(shè)得GC2t ?Γ?φ。由引理4.1 得存在b ∈WΞ使得Γ?b并且φ ∈bc。因此。

引理4.4.給定GC2t 中的矢列Γ ?Δ 使得Ξ:=Sf(Γ,Δ)。如果Γ ?Δ 在GC2t 中Ξ-不可證，那么對GC2t 框架上的有窮模型MΞ，存在a ∈MΞ使得MΞ,a?Γ ?Δ。證明.假設(shè)Γ ?Δ 在GC2t Ξ-不可證。由引理4.1 得存在a ∈WΞ使得Γ?a并且Δ?ac。由引理4.3 得MΞ,a?Γ ?Δ，其中MΞ是基于GC2t 的框架FΞ。由命題4.2 得FΞ是HC2t 的框架。

定理4.5(子公式性質(zhì)). 對任意矢列Γ ?Δ，如果Γ ?Δ 在GC2t 中可證，那么Γ ?Δ 在GC2t 中Ξ-可證，其中Ξ:=Sf(Γ,Δ)。

證明.設(shè)Γ ?Δ 在GC2t 中Ξ-不可證。由引理4.4 得Γ ?Δ 在GC2t 的某個有窮正則框架上為假。由GC2t 的可靠性得Γ ?Δ 在GC2t 中不可證。

稱HC2t 具有有窮模型性質(zhì)，如果存在正則框架類C 使得對所有HC2t 的定理φ，C ?φ并且所有不是HC2t 的定理ψ，ψ在C 中的某個有窮框架上為假。

推論1.HC2t 具有有窮模型性質(zhì)并且HC2t 可判定。

證明.令CF 為所有正則框架類。由HC2t 得可靠性得所有HC2t 中的定理φ都有效。由HC2t 的完全性和引理4.4 得，所有不是HC2t 的定理ψ，ψ在CF 中的某個有窮框架上為假。因此HC2t 具有有窮模型性質(zhì)并且HC2t 可判定。

5 GC2t 的插值定理

定義5.1.GC2t*是將GC2t 中的規(guī)則(Cut)，(adF)，(adP)分別替換成(Cut*)，()，()，公理模式和其他規(guī)則保持不變得到的矢列演算。其中規(guī)則(Cut*)，()，()分別定義如下：

我們在上一節(jié)證明了GC2t 的子公式性質(zhì)。由GC2t 的子公式性質(zhì)得GC2t 和GC2t*等價。在這一節(jié)，我們將要證明GC2t*的插值定理。從而得到GC2t 的插值性質(zhì)。

定義5.2.我們用Γ?Δ 表示Γ 和Δ 的并。對任意矢列Γ ?Δ，稱(Γ1:Δ1);(Γ2:Δ2)是Γ ?Δ 的劃分，如果Γ1?Γ2=Γ and Δ1?Δ2=Δ。令GC2t* ?Γ ?Δ。對任意Γ ?Δ 的劃分(Γ1:Δ1);(Γ2:Δ2)，稱公式χ是(Γ1:Δ1);(Γ2:Δ2)的插值，如果以下條件滿足：

定理5.1.如果GC2t* ?Γ ?Δ 并且(Γ1:Δ1);(Γ2:Δ2)是Γ ?Δ 的劃分，那么存在公式χ使得χ是(Γ1:Δ1);(Γ2:Δ2)的插值。

證明.設(shè)GC2t*?Γ ?Δ 并且(Γ1:Δ1);(Γ2:Δ2)是Γ ?Δ 的劃分。令D是矢列Γ ?Δ 在GC2t*的推導。對|D|歸納證明存在公式χ使得χ是(Γ1:Δ1);(Γ2:Δ2)的插值。

(1)設(shè)|D|=0。那么Γ ?Δ 是公理。以下有四種情況，在這四種情況下，變元條件顯然滿足。

(1.1)Γ ?Δ 是(A1：φ,Γ ?Δ,φ)的特例，分以下情況。

(1.1.1)(Γ1:Δ1);(Γ2:Δ2)=(φ,Γ1:Δ1);(Γ2:Δ2,φ)。因為?φ,Γ1?Δ1,φ并且?φ,Γ2?Δ2,φ。因此φ是插值。

(1.1.2) (Γ1: Δ1);(Γ2: Δ2)=(φ,Γ1: Δ1,φ);(Γ2: Δ2)。因為?φ,Γ1?Δ1,φ,⊥并且?⊥,Γ2?Δ2。因此⊥是插值。

(1.1.3)(Γ1: Δ1);(Γ2: Δ2)=(Γ1: Δ1);(φ,Γ2: Δ2,φ)。因為?Γ1?Δ1,?并且??,φ,Γ2?Δ2,φ。因此?是插值。

(1.1.4) (Γ1: Δ1);(Γ2: Δ2)=(Γ1: Δ1,φ);(φ,Γ2: Δ2)。因為?Γ1?Δ1,φ,?φ并且??φ,φ,Γ2?Δ2。因此?φ是插值。

(1.2)Γ ?Δ 是(A2：⊥,Γ ?Δ)的特例，分以下情況。

(1.2.1)(Γ1: Δ1);(Γ2: Δ2)=(⊥,Γ1: Δ1);(Γ2: Δ2)。因為?⊥,Γ1?Δ1,⊥并且?⊥,Γ2?Δ2。因此⊥是插值

(1.2.2)(Γ1: Δ1);(Γ2: Δ2)=(Γ1: Δ1);(⊥,Γ2: Δ2)。因為?Γ1?Δ1,?并且??,⊥,Γ2?Δ2。因此?是插值。

(1.3)Γ ?Δ 是(A3：□?,Γ ?Δ,■?)的特例，分以下情況。

(1.3.1)(Γ1:Δ1);(Γ2:Δ2)=(□?,Γ1:Δ1);(Γ2:Δ2,■?)。因為?□?,Γ1?Δ1,■?并且?■?,Γ2?Δ2,■?。因此■?是插值。

(1.3.2)(Γ1:Δ1);(Γ2:Δ2)=(□?,Γ1:Δ1,■?);(Γ2:Δ2)。因為?□?,Γ1?Δ1,■?,⊥并且?⊥,Γ2?Δ2。因此⊥是插值。

(1.3.3) (Γ1: Δ1);(Γ2: Δ2)=(Γ1: Δ1);(□?,Γ2: Δ2,■?)。因為?Γ1?Δ1,?并且??,□?,Γ2?Δ2,■?。因此?是插值。

(1.3.4) (Γ1: Δ1);(Γ2: Δ2)=(Γ1: Δ1,■?);(□?,Γ2: Δ2)。因為?Γ1?Δ1,■?,?■?并且??■?,□?,Γ2?Δ2。因此?■?是插值。

(1.4)Γ ?Δ 是(A4□■?,Γ ?Δ,□?)的特例。證明類似。

(2)設(shè)|D|＞0。那么Γ ?Δ 由推理規(guī)則(R)得到。這里只驗證規(guī)則(adF)和(KF)。

(2.1)(R)是(adF)，則推導的最后一步是：

令(□?,Θ1,□Σ1:□?,Θ2,□Σ2) 是□?,Θ,□Σ?□φ的劃分。往證存在插值χ使得GC2t* ?□?,Θ1,□Σ1?χ并且GC2t* ?χ,□?,Θ2,□Σ2?□φ，var(χ)?var(Θ1,□Σ1)∩var(Θ2,□Σ2,□φ)。由歸納假設(shè)得，存在公式χ使得

由(1a)運用規(guī)則(adF)得?□?,Θ1,□Σ1?□χ。由(KF)和(1b)得?□χ,□?,□?Θ2,□Σ2?□φ。顯然?□?,□χ,□Σ2,Θ2?□?,□?Θ2,□χ,□Σ2。因此?□χ,□?,Θ2,□Σ2?□φ。因為var(χ)?var(?Θ1,Σ1)∩var(?Θ2,Σ2)。顯然var(□χ)?var(Θ1,□Σ1)∩var(Θ2,□Σ2)。因此□χ是插值。(2.2)(R)是(KF)，則推導的最后一步是：

令(□Γ1:□Γ2)是□Γ?□φ的劃分。往證存在插值χ使得GC2t*?□Γ1?χ并且GC2t*?χ,□Γ2?□φ，var(χ)?var(□Γ1)∩var(□Γ2,□φ)。由歸納假設(shè)得存在公式χ使得

由(1a)運用規(guī)則(KF)得?□Γ1?□χ。由(1b)運用規(guī)則(KF)得?□(χ,Γ2)?□φ。顯然?□χ,□Γ2?□(χ,Γ2)。因此?□χ,□Γ2?□φ。因為var(φ)?var(Γ1)∩var(Γ2,φ)。顯然var(□φ)?var(□Γ1)∩var(□Γ2,□φ)。因此□χ是插值。