非正規(guī)模態(tài)邏輯C2 的時(shí)態(tài)擴(kuò)張

涂保勛

1 引言

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

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

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

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

2 句法和語(yǔ)義

定義2.1.令Prop是命題變?cè)臒o(wú)窮集合，公式集L遞歸定義如下：

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

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

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

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

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

M,w?⊥，

M,w?φ ∧ψ當(dāng)且僅當(dāng)M,w?φ并且M,w?ψ，

M,w?φ ∨ψ當(dāng)且僅當(dāng)M,w?φ或者M(jìn),w?ψ，

M,w?φ→ψ當(dāng)且僅當(dāng)M,w?φ或者M(jìn),w?ψ，

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

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

特別地，M,w?□?當(dāng)且僅當(dāng)w ∈N。M,w?■?當(dāng)且僅當(dāng)w ∈N。

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

稱(chēng)一個(gè)公式φ相對(duì)于一個(gè)正則框架類(lèi)C 有效，記為C ?φ，如果對(duì)所有F∈C，?φ。給定任意公式集Γ 和任意公式φ，稱(chēng)φ是Γ 的邏輯后承，記為Γ ?φ，如果對(duì)任意正則模型M 和任意w ∈W，M,w?Γ 蘊(yùn)含M,w?φ。

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

(1)公理：

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

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

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

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

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

定理2.1(完全性). HC2t 相對(duì)于所有正則框架類(lèi)是強(qiáng)完全的。

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

3 HC2t 的矢列演算

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

其中Γi?Δi(1 ≤i≤n)稱(chēng)為(R)的前提，Γ0?Δ0稱(chēng)為(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 中，一個(gè)推導(dǎo)D是由矢列組成的有窮樹(shù)結(jié)構(gòu)，其中每個(gè)節(jié)點(diǎn)要么是公理，要么是從子節(jié)點(diǎn)矢列使用某個(gè)規(guī)則得到的。稱(chēng)矢列Γ ?Δ 在GC2t 中可推導(dǎo)（記為：GC2t?Γ ?Δ），如果在GC2t 中存在推導(dǎo)D使得D的根節(jié)點(diǎn)為Γ ?Δ。稱(chēng)推理規(guī)則(R)可允許，如果(R)的結(jié)論(Γ0?Δ0)不可推導(dǎo)，那么(R)的前提(Γi?Δi)不可推導(dǎo)。

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

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

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

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

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

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

定理3.2.GC2t?Γ ?Δ 當(dāng)且僅當(dāng)HC2t?∧?！纽?。

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

由歸納假設(shè)得HC2t?□?∧∧?Θ∧∧Σ→φ。由Mon□得HC2t?□(□?∧∧?Θ∧∧Σ)→□φ。因?yàn)镠C2t?□?∧∧□?Θ∧∧□Σ→□(□?∧∧?Θ∧∧Σ)。因此HC2t?□?∧∧□?Θ∧∧□Σ→□φ。因?yàn)镠C2t?□?∧∧Θ∧∧□Σ→□?∧∧□?Θ∧∧□Σ。因此HC2t?□?∧∧Θ∧∧□Σ→□φ。

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

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

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

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

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

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

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

稱(chēng)公式集a ?Ξ 是Ξ-飽和的，如果二元組(a,Ξa(chǎn))在GC2t 中是Ξ-飽和的。在這一節(jié)的后面部分，我們會(huì)一直使用Ξ 表示子公式封閉的有窮公式集。另外，給定任意公式集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對(duì)某個(gè)i(1≤i ≤n)。設(shè)GC2t ?φ,an+1?bn+1。顯然GC2t?ak ?bk,φ，否則φ ∈bk+1?bn+1使得GC2t?φ,an+1?bn+1。因?yàn)閍k ?an+1并且bk ?bn+1，由假設(shè)得GC2t ?φ,ak ?bk。所以φ ∈ak+1?an+1。同理可得φ ∈bn+1。

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

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

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

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

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

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

證明.對(duì)公式φ的復(fù)雜度歸納證明。原子公式的情況顯然成立。由歸納假設(shè)可得布爾公式的情況。令φ=□ψ。從左到右，設(shè)□ψ ∈a并且RFab。由□-飽和的定義得φ ∈b。由歸納假設(shè)得MΞ,b?ψ。因?yàn)閎 ∈RF(a)。因此MΞ,a?□ψ。從右到左，設(shè)MΞ,a?□ψ并且RFab。由語(yǔ)義定義得MΞ,b?φ。由歸納假設(shè)得φ ∈b。因?yàn)镽Fab。因此□φ ∈a。當(dāng)φ=■ψ，證明類(lèi)似。

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

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

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

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

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

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

引理4.4.給定GC2t 中的矢列Γ ?Δ 使得Ξ:=Sf(Γ,Δ)。如果Γ ?Δ 在GC2t 中Ξ-不可證，那么對(duì)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ì)). 對(duì)任意矢列Γ ?Δ，如果Γ ?Δ 在GC2t 中可證，那么Γ ?Δ 在GC2t 中Ξ-可證，其中Ξ:=Sf(Γ,Δ)。

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

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

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

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

5 GC2t 的插值定理

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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