非正规模态逻辑C2 的时态扩张

涂保勋

1 引言

正规模态逻辑S5 的根岑式矢列演算通常不具有子公式性质。运用语义的方法，高野道夫（M.Takana）在[5]中证明了，如果一个矢列可证，那么存在一个推导使得推导中的所有公式都是该矢列中公式的子公式，即证明了S5 的子公式性质。高野道夫在[4]中评论说，运用同样的方法可以证明基本时态逻辑Kt 的子公式性质。模态逻辑K4 的时态扩张的子公式性质证明参见[2,3]。

非正规模态逻辑系统C2 由雷蒙（E.J.Lemmon）在[1]中给出，该系统由命题逻辑的重言式，公理□(φ→ψ)→(□φ→□ψ)和以下两个规则组成：

在关系语义和代数语义下，该系统的完全性和有穷模型性被证明，雷蒙评论C2 的结论可以扩张到其他逻辑。在[6]中，C2 被时态化为C2t，C2t 的可靠性和完全性得到证明。另外，C2t 的加标矢列演算被给出，该演算的可靠性和完全性得到证明。然而在此文章中，C2t 的有穷模型性和可判定性问题没有得到证明。本文将构建C2t 的根岑式矢列演算，运用高野道夫的语义方法证明C2t 的子公式性质，进而证明C2t 的有穷模型性和可判定性。另外，本文还将证明C2t 的插值性质。

本文的结构如下。第二部分介绍非正规逻辑C2t 的语型和语义。第三部分给出C2t 的矢列演算GC2t。第四部分证明GC2t 的子公式性质，有穷模型性和可判定性。第5 部分证明GC2t 的插值性质。

2 句法和语义

定义2.1.令Prop是命题变元的无穷集合，公式集L递归定义如下：

其中p ∈Prop。定义¬φ:=φ→⊥，⊤:=⊥→⊥，φ ↔ψ:=(φ→ψ)∧(ψ→φ)。◇φ的对偶定义为◇φ:=¬□¬φ。♦φ的对偶定义为♦φ:=¬■¬φ。

定义2.2.一个正则框架是一个四元组=(W,N,RF,RP)，其中W是非空集，N ⊆W是正规时间点（世界）的集合，RF和RP是W上满足以下条件的二元关系：

一个正则模型是一个二元组M=(F,V)，其中F 是正则框架，V:Prop→℘(W)是一个赋值函数。

定义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.希尔伯特式公理系统HC2t 在[6]中给出，该系统由如下公理模式和推理规则组成：

(1)公理：

(2)推理规则：

给定公式φ和公式集Γ，相对于系统HC2t，称φ是Γ 的演绎后承，记为Γ⊢HC2tφ，如果存在一个有穷集合Γ′ ⊆Γ 使得∧Γ′→φ ∈HC2t，其中∧Γ′是Γ′中所有公式的合取。当Γ=∅，记为⊢HC2tφ。

命题2.1.对任意公式φ和ψ，以下三条成立：

命题2.2(可靠性). 对任意公式φ ∈L，如果HC2t⊢φ，那么⊨φ。

证明.需验证HC2t 的公理有效并且推理规则保持有效性。给定任意正则框架F，令V是上的任意赋值并且w是上的任意点。以下验证公理(ad1)的有效性和规则(Mon□)保持有效性。

定理2.1(完全性). HC2t 相对于所有正则框架类是强完全的。

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

3 HC2t 的矢列演算

令Γ,Δ 等（有或者无下标）表示有穷可重公式集。一个矢列是形如Γ ⇒Δ的表达式，其中Γ 和Δ 都是有穷的非空的可重公式集。一个矢列规则是以下形式的表达式：

其中Γi⇒Δi(1 ≤i≤n)称为(R)的前提，Γ0⇒Δ0称为(R)的结论。

定义3.1.HC2t 的矢列演算GC2t 由以下公理模式和矢列规则组成：

(1)公理模式：

(2)联结词规则：

(3)结构规则：

(4)切割规则：

(5)模态规则：

在GC2t 中，一个推导D是由矢列组成的有穷树结构，其中每个节点要么是公理，要么是从子节点矢列使用某个规则得到的。称矢列Γ ⇒Δ 在GC2t 中可推导（记为：GC2t⊢Γ ⇒Δ），如果在GC2t 中存在推导D使得D的根节点为Γ ⇒Δ。称推理规则(R)可允许，如果(R)的结论(Γ0⇒Δ0)不可推导，那么(R)的前提(Γi⇒Δi)不可推导。

定义3.2.给定任意正规模型M=(,V)，w ∈M，称矢列Γ ⇒Δ 在w上真（记为：M,w⊨Γ ⇒Δ），如果M,w⊨∧Γ→∨Δ。称一个矢列规则在模型上保真，如果在模型上前提真蕴含结论真。称矢列Γ ⇒Δ 是有效的（记为：⊨Γ ⇒Δ），如果∧Γ→∨Δ 是有效式。

命题3.1(可靠性). 对任意矢列Γ ⇒Δ，如果GC2t⊢Γ ⇒Δ，那么⊨Γ ⇒Δ。

证明.容易验证GC2t 的公理都是有效的并且推导规则保持有效性。

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

证明.假设HC2t⊢α，则在HC2t 中存在一个推导D。对D的长度归纳证明⊢⇒α。设|D|=0，则α在HC2t 中是公理。公理(K)和(N)容易验证，这里只验证公理(ad1)。(ad1)的推导如下：

设|D| ＞0，则α从ψ→α和α由(MP)得到。由归纳假设得GC2t⊢⇒ψ并且GC2t⊢⇒ψ→α。⇒α的推导如下：

定理3.2.GC2t⊢Γ ⇒Δ 当且仅当HC2t⊢∧Γ→∨Δ。

证明.从右到左，设HC2t⊢∧Γ→∨Δ。由引理3.1 得GC2t⊢⇒∧Γ→∨Δ。显然GC2t⊢Γ ⇒∧Γ 并且GC2t⊢∧Γ,∧Γ ⇒∨Δ。由(Cut)得GC2t⊢Γ ⇒∨Δ。显然，GC2t⊢∨Δ ⇒Δ。由(Cut)得GC2t⊢Γ ⇒Δ。另一个方向，设GC2t⊢Γ ⇒Δ。那么在GC2t 中存在Γ ⇒Δ 的推导D。对|D|归纳证明HC2t⊢∧Γ→∨Δ。设|D|=0。则矢列Γ ⇒Δ 是公理。对每条GC2t 的公理，容易验证HC2t⊢∧Γ→∨Δ。设|D| ＞0。则矢列Γ ⇒Δ 由规则(R)得到。其他情况容易验证，这里只验证规则(adF)。在这种情况下，推导的最后一步是：

由归纳假设得HC2t⊢□⊤∧∧♦Θ∧∧Σ→φ。由Mon□得HC2t⊢□(□⊤∧∧♦Θ∧∧Σ)→□φ。因为HC2t⊢□⊤∧∧□♦Θ∧∧□Σ→□(□⊤∧∧♦Θ∧∧Σ)。因此HC2t⊢□⊤∧∧□♦Θ∧∧□Σ→□φ。因为HC2t⊢□⊤∧∧Θ∧∧□Σ→□⊤∧∧□♦Θ∧∧□Σ。因此HC2t⊢□⊤∧∧Θ∧∧□Σ→□φ。

定理3.3(完全性). 令CF 表示所有正则框架类，如果CF ⊨Γ ⇒Δ，那么GC2t⊢Γ ⇒Δ。

证明.设CF ⊨Γ ⇒Δ。则CF ⊨∧Γ→∨Δ。由HC2t 的完全性得HC2t⊢∧Γ→∨Δ。由定理3.2 得GC2t⊢Γ ⇒Δ。

4 子公式性质和可判定性

令Γ 为有穷可重公式集。Sf(Γ)表示Γ 的所有子公式的集合。称一个可推导的矢列Γ ⇒Δ 有子公式性质，如果存在一个推导D使得D中出现的公式都属于Sf(Γ,Δ)。称一个矢列演算具有子公式性质，如果对该演算中任意可推导的矢列Γ ⇒Δ，存在一个推导D使得D中出现的公式都属于Sf(Γ,Δ)。在GC2t 中，显然规则(Cut)、(adF)和(adP)不具有子公式性质。本节的目标是证明GC2t 的子公式性质。为此，我们将要证明，如果一个矢列Γ ⇒Δ 在GC2t 中可推导，那么存在一个该矢列的推导D使得D中出现的公式都属于Sf(Γ,Δ)。

定义4.1.令Ξ 是子公式封闭的有穷公式集。称一个矢列Γ ⇒Δ 在GC2t 中Ξ-可证，如果存在一个该矢列的推导D使得D中出现的公式都属于Ξ。令a,b为Ξ的两个子集，称二元组(a,b)Ξ-不相交，如果a ⇒b不是Ξ-可证的。称一个矢列a ⇒b是Ξ-饱和的，如果(a,b)Ξ-不相交并且满足如下条件：

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

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

称公式集a ⊆Ξ 是Ξ-饱和的，如果二元组(a,Ξa)在GC2t 中是Ξ-饱和的。在这一节的后面部分，我们会一直使用Ξ 表示子公式封闭的有穷公式集。另外，给定任意公式集a ⊆Ξ，用ac表示Ξa。

引理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)。设GC2t ⊬φ,an+1⇒bn+1。显然GC2t⊢ak ⇒bk,φ，否则φ ∈bk+1⊆bn+1使得GC2t⊢φ,an+1⇒bn+1。因为ak ⊆an+1并且bk ⊆bn+1，由假设得GC2t ⊬φ,ak ⇒bk。所以φ ∈ak+1⊆an+1。同理可得φ ∈bn+1。

定义4.2.令Ξ 为子公式封闭的有穷公式集，定义GC2t 的Ξ-模型MΞ如下：

令RF、RP是WΞ上的二元关系。对任意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 相应的联结词规则，条件(1)到(6)容易证明。

引理4.3.令MΞ是GC2t 的正则Ξ-模型。对所有公式φ ∈Ξ 并且a ∈Ξ，φ ∈a当且仅当MΞ,a⊨φ。

证明.对公式φ的复杂度归纳证明。原子公式的情况显然成立。由归纳假设可得布尔公式的情况。令φ=□ψ。从左到右，设□ψ ∈a并且RFab。由□-饱和的定义得φ ∈b。由归纳假设得MΞ,b⊨ψ。因为b ∈RF(a)。因此MΞ,a⊨□ψ。从右到左，设MΞ,a⊨□ψ并且RFab。由语义定义得MΞ,b⊨φ。由归纳假设得φ ∈b。因为RFab。因此□φ ∈a。当φ=■ψ，证明类似。

定义4.3.给定a,b ∈WΞ。令□⊤∈a并且□⊤∈b。WΞ上的二元关系定义如下：

命题4.1.对任意公式集Σ,Θ 和公式φ，以下条件成立：

证明.这里只证明(1)。从右至左，设GC2t ⊬□⊤,Θ,□Σ⇒□φ。由引理4.1 得□⊤∈a，Θ⊆a，□Σ⊆a并且□φ ∈ac。由假设得φ ∈bc。如果♦θ ∈♦Θ，那么θ ∈Θ，并且如果σ ∈Σ，那么□σ ∈□Σ。因为□⊤∈b。因此GC2t ⊬□⊤,♦Θ,Σ⇒φ。从左至右，设□φ ∈ac。令Θ={θ ∈a |♦θ ∈Ξ}并且Σ={σ | □σ ∈a}。因为□⊤∈a，Θ⊆a并且□Σ⊆a。由假设得GC2t ⊬□⊤,Θ,□Σ⇒□φ。那么GC2t⊬□⊤,♦Θ,Σ⇒φ。由引理4.1 得♦Θ⊆a、Σ⊆a并且φ ∈ac。因此成立。

定义4.4.矢列演算GC2t 在WΞ上的二元关系定义如下：

命题4.2.令切割规则(Cut)的切割公式φ ∈Ξ，对任意公式ψ，以下命题成立：

证明.这里只证明(2)。从右至左，设GC2t ⊬■Γ ⇒■φ。由引理4.1 得■Γ⊆a并且■φ ∈ac。由假设得存在b ∈WΞ使得并且ψ ∈bc。如果α ∈Γ，那么■α ∈■Γ⊆a。因为。则α ∈b。因此Γ⊆b。因此GC2t ⊬Γ⇒φ。从左至右，设■φ ∈ac。令Γ={α |■α ∈a}。因为■Γ⊆a并且■φ ∈ac。则GC2t⊬■Γ ⇒■φ。由假设得GC2t ⊬Γ⇒φ。由引理4.1 得存在b ∈WΞ使得Γ⊆b并且φ ∈bc。因此。

引理4.4.给定GC2t 中的矢列Γ ⇒Δ 使得Ξ:=Sf(Γ,Δ)。如果Γ ⇒Δ 在GC2t 中Ξ-不可证，那么对GC2t 框架上的有穷模型MΞ，存在a ∈MΞ使得MΞ,a⊭Γ ⇒Δ。证明.假设Γ ⇒Δ 在GC2t Ξ-不可证。由引理4.1 得存在a ∈WΞ使得Γ⊆a并且Δ⊆ac。由引理4.3 得MΞ,a⊭Γ ⇒Δ，其中MΞ是基于GC2t 的框架FΞ。由命题4.2 得FΞ是HC2t 的框架。

定理4.5(子公式性质). 对任意矢列Γ ⇒Δ，如果Γ ⇒Δ 在GC2t 中可证，那么Γ ⇒Δ 在GC2t 中Ξ-可证，其中Ξ:=Sf(Γ,Δ)。

证明.设Γ ⇒Δ 在GC2t 中Ξ-不可证。由引理4.4 得Γ ⇒Δ 在GC2t 的某个有穷正则框架上为假。由GC2t 的可靠性得Γ ⇒Δ 在GC2t 中不可证。

称HC2t 具有有穷模型性质，如果存在正则框架类C 使得对所有HC2t 的定理φ，C ⊨φ并且所有不是HC2t 的定理ψ，ψ在C 中的某个有穷框架上为假。

推论1.HC2t 具有有穷模型性质并且HC2t 可判定。

证明.令CF 为所有正则框架类。由HC2t 得可靠性得所有HC2t 中的定理φ都有效。由HC2t 的完全性和引理4.4 得，所有不是HC2t 的定理ψ，ψ在CF 中的某个有穷框架上为假。因此HC2t 具有有穷模型性质并且HC2t 可判定。

5 GC2t 的插值定理

定义5.1.GC2t*是将GC2t 中的规则(Cut)，(adF)，(adP)分别替换成(Cut*)，()，()，公理模式和其他规则保持不变得到的矢列演算。其中规则(Cut*)，()，()分别定义如下：

我们在上一节证明了GC2t 的子公式性质。由GC2t 的子公式性质得GC2t 和GC2t*等价。在这一节，我们将要证明GC2t*的插值定理。从而得到GC2t 的插值性质。

定义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)的插值。

证明.设GC2t*⊢Γ ⇒Δ 并且(Γ1:Δ1);(Γ2:Δ2)是Γ ⇒Δ 的划分。令D是矢列Γ ⇒Δ 在GC2t*的推导。对|D|归纳证明存在公式χ使得χ是(Γ1:Δ1);(Γ2:Δ2)的插值。

(1)设|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)设|D|＞0。那么Γ ⇒Δ 由推理规则(R)得到。这里只验证规则(adF)和(KF)。

(2.1)(R)是(adF)，则推导的最后一步是：

令(□⊤,Θ1,□Σ1:□⊤,Θ2,□Σ2) 是□⊤,Θ,□Σ⇒□φ的划分。往证存在插值χ使得GC2t* ⊢□⊤,Θ1,□Σ1⇒χ并且GC2t* ⊢χ,□⊤,Θ2,□Σ2⇒□φ，var(χ)⊆var(Θ1,□Σ1)∩var(Θ2,□Σ2,□φ)。由归纳假设得，存在公式χ使得

由(1a)运用规则(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,□φ)。由归纳假设得存在公式χ使得

由(1a)运用规则(KF)得⊢□Γ1⇒□χ。由(1b)运用规则(KF)得⊢□(χ,Γ2)⇒□φ。显然⊢□χ,□Γ2⇒□(χ,Γ2)。因此⊢□χ,□Γ2⇒□φ。因为var(φ)⊆var(Γ1)∩var(Γ2,φ)。显然var(□φ)⊆var(□Γ1)∩var(□Γ2,□φ)。因此□χ是插值。