1、逻辑学研究2023 年第 5 期，6980文章编号：1674-3202(2023)-05-0069-12非正规模态逻辑 C2 的时态扩张涂保勋摘要：本文构建了非正规时态逻辑 C2t 的矢列演算 GC2t。运用高野道夫（M.Takana）的语义方法证明了 GC2t 的子公式性质，进而证明了 GC2t 的有穷模型性和可判定性。另外，本文还证明了 GC2t 的插值性质。关键词：非正规模态逻辑；子公式性质；有穷模型性；插值性质中图分类号：B81文献标识码：A1引言正规模态逻辑 S5 的根岑式矢列演算通常不具有子公式性质。运用语义的方法，高野道夫（M.Takana）在 5 中证明了，如果一个矢列可证，那
2、么存在一个推导使得推导中的所有公式都是该矢列中公式的子公式，即证明了 S5 的子公式性质。高野道夫在 4 中评论说，运用同样的方法可以证明基本时态逻辑 Kt 的子公式性质。模态逻辑 K4 的时态扩张的子公式性质证明参见 2,3。非正规模态逻辑系统 C2 由雷蒙（E.J.Lemmon）在 1 中给出，该系统由命题逻辑的重言式，公理 2()(2 2)和以下两个规则组成：R1:R2:2 2在关系语义和代数语义下，该系统的完全性和有穷模型性被证明，雷蒙评论 C2 的结论可以扩张到其他逻辑。在 6 中，C2 被时态化为 C2t，C2t 的可靠性和完全性得到证明。另外，C2t 的加标矢列演算被给出，该演算
3、的可靠性和完全性得到证明。然而在此文章中，C2t 的有穷模型性和可判定性问题没有得到证明。本文将构建 C2t 的根岑式矢列演算，运用高野道夫的语义方法证明 C2t 的子公式性质，进而证明 C2t 的有穷模型性和可判定性。另外，本文还将证明 C2t 的插值性质。本文的结构如下。第二部分介绍非正规逻辑 C2t 的语型和语义。第三部分给出 C2t 的矢列演算 GC2t。第四部分证明 GC2t 的子公式性质，有穷模型性和可判定性。第 5 部分证明 GC2t 的插值性质。收稿日期：2021-03-26作者信息：涂保勋中山大学逻辑与认知研究所中山大学哲学系70逻辑学研究第 16 卷 第 5 期 2023
4、年2句法和语义定义 2.1.令 Prop 是命题变元的无穷集合，公式集 L 递归定义如下：:=p|(1 2)|(1 2)|(1 2)|2|其中 p Prop。定义 :=，:=，:=()()。3 的对偶定义为 3:=2。的对偶定义为 :=。定义 2.2.一个正则框架是一个四元组 F=(W,N,RF,RP)，其中 W 是非空集，N W 是正规时间点（世界）的集合，RF和 RP是 W 上满足以下条件的二元关系：对所有 w,u N，RFwu 当且仅当 RPuw。一个正则模型是一个二元组 M=(F,V)，其中 F 是正则框架，V:Prop (W)是一个赋值函数。定义 2.3.给定一个公式 L，一个正则模
5、型 M=(F,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 2 当且仅当 w N 并且 u W(RFwu M,u )，M,w 当且仅当 w N 并且 u W(RPwu M,u )。特别地，M,w 2 当且仅当 w N。M,w 当且仅当 w N。称一个公式 在 M 上可满足，如果存在 w W 使得 M,w 。称 在M 上真，记为 M ，如果对任意 w W 都有 M,w 。
6、称公式 在一个正则框架 F 上有效，记为 F ，如果对任意 F 上的赋值 V 并且对所有 w W，(F,V),w 。称一个公式相对于一个正则框架类C有效，记为C ，如果对所有F C，F 。给定任意公式集 和任意公式，称 是 的逻辑后承，记为 ，如果对任意正则模型 M 和任意 w W，M,w 蕴含 M,w 。称一个公式集 定义正则框架类 C，如果对任意正则框架 F，在 F 上有效当且仅当 F C。如果 是单元集，称 定义 C。涂保勋非正规模态逻辑 C2 的时态扩张71定义 2.4.希尔伯特式公理系统 HC2t 在 6 中给出，该系统由如下公理模式和推理规则组成：(1)公理：(Taut)所有命题逻
7、辑重言式特例，(K)2()(2 2)，(ad1)2 (2)，(N)2 ，(2)推理规则：(MP)(Mon2)2 2给定公式 和公式集，相对于系统 HC2t，称 是 的演绎后承，记为 HC2t，如果存在一个有穷集合 使得 HC2t，其中是 中所有公式的合取。当 =，记为 HC2t。命题 2.1.对任意公式 和，以下三条成立：(1)HC2t()()，(2)HC2t (3)，(3)若 HC2t ，则 HC2t 。命题 2.2(可靠性).对任意公式 L，如果 HC2t ，那么 。证明.需验证 HC2t 的公理有效并且推理规则保持有效性。给定任意正则框架 F，令 V 是 F 上的任意赋值并且 w 是 F
8、 上的任意点。以下验证公理(ad1)的有效性和规则(Mon2)保持有效性。(ad1)：设(F,V),w 2 并且(F,V),w 。那么 w N。令 w=v。那么对任意 u RF(w)存在 v 使得 RPvu 并且(F,V),v 。因此(F,V),w 2。(Mon2)：设(F,V),w 并且(F,V),w 2。那么 w N 并且对任意 u RF(w)，(F,V),u 。因为 w N。由假设得(F,V),u 。因此(F,V),u 。因为 u RF(w)。因此(F,V),w 2。定理 2.1(完全性).HC2t 相对于所有正则框架类是强完全的。证明.运用典范模型方法，在 6 中已被证明。3HC2t
9、的矢列演算令,等（有或者无下标）表示有穷可重公式集。一个矢列是形如 的表达式，其中 和 都是有穷的非空的可重公式集。一个矢列规则是以下形式72逻辑学研究第 16 卷 第 5 期 2023 年的表达式：1 1.n n(R)0 0其中 i i(1 i n)称为(R)的前提，0 0称为(R)的结论。定义 3.1.HC2t 的矢列演算 GC2t 由以下公理模式和矢列规则组成：(1)公理模式：(A1),(A2),(A3)2,(A4),2(2)联结词规则：1,2,()1 2,(),(),1,2(),1 2 ,(),(),(3)结构规则：(w),(w),(c),(c),(4)切割规则：,(Cut),(5)模
10、态规则：2,(adF)2,2 2,3,(adP),(KF)2 2 (KP)在 GC2t 中，一个推导 D 是由矢列组成的有穷树结构，其中每个节点要么是公理，要么是从子节点矢列使用某个规则得到的。称矢列 在 GC2t 中可推导（记为：GC2t ），如果在 GC2t 中存在推导 D 使得 D 的根节点为 。称推理规则(R)可允许，如果(R)的结论(0 0)不可推导，那么(R)的前提(i i)不可推导。涂保勋非正规模态逻辑 C2 的时态扩张73定义 3.2.给定任意正规模型 M=(F,V)，w M，称矢列 在 w 上真（记为：M,w ），如果 M,w 。称一个矢列规则在模型上保真，如果在模型上前提真
11、蕴含结论真。称矢列 是有效的（记为：），如果 是有效式。命题 3.1(可靠性).对任意矢列 ，如果 GC2t ，那么 。证明.容易验证 GC2t 的公理都是有效的并且推导规则保持有效性。引理 3.1.如果 HC2t ，那么 GC2t 。证明.假设 HC2t ，则在 HC2t 中存在一个推导 D。对 D 的长度归纳证明 。设|D|=0，则 在 HC2t 中是公理。公理(K)和(N)容易验证，这里只验证公理(ad1)。(ad1)的推导如下：2,(adF)2,2设|D|0，则 从 和 由(MP)得到。由归纳假设得 GC2t 并且GC2t 。的推导如下：,(),(Cut)(Cut)定理 3.2.GC2
12、t 当且仅当 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)。在这种情况下，推导的最后一步是：2,(adF)2,2 2由归纳假设得 HC2t 2 。由 Mon2得 HC2t 2(2)2。因为 HC2t 2 2 2 2(2 )。因此 HC2t
13、 2 2 2 2。因为 HC2t 2 2 2 2 2。因此 HC2t 2 2 2。74逻辑学研究第 16 卷 第 5 期 2023 年定理 3.3(完全性).令 CF 表示所有正则框架类，如果 CF ，那么 GC2t 。证明.设 CF 。则 CF 。由 HC2t 的完全性得 HC2t 。由定理 3.2 得 GC2t 。4子公式性质和可判定性令 为有穷可重公式集。Sf()表示 的所有子公式的集合。称一个可推导的矢列 有子公式性质，如果存在一个推导 D 使得 D 中出现的公式都属于Sf(,)。称一个矢列演算具有子公式性质，如果对该演算中任意可推导的矢列 ，存在一个推导 D 使得 D 中出现的公式都
14、属于 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 不是-可证的，那么
15、 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是形如 2()的公式，m+1,.,n不是形如 2()的公式。令a0 b0=a b。如果GC2t ak bk,k，那么令ak+1 bk+1=ak bk,k。
16、如果 GC2t ak bk,k并且 GC2t ak,k bk，那么令 ak+1 bk+1=ak,kbk。否则，令 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。涂保勋非正规模态逻辑 C2 的时态扩张75定义 4.2.令 为子公式封闭的有穷公式集，定义 G
17、C2t 的-模型 M如下：W=a|a 在 GC2t 中是-饱和的。N=a W|2 a。令 RF、RP是 W上的二元关系。对任意 a,b W并且 ，称 RF是2-饱和的，如果满足如下条件：2 a a N并且 b W(RFab b)。称 RF是-饱和的，如果满足以下条件：a a/N或者 b W(RFba并且 b)。RP的(3)饱和条件类似。V(p)=a W|p a。如果 RF是 2-饱和的并且是-饱和的，RP是-饱和的并且是 3-饱和的，那么 M=(W,N,RF,RP,V)是 GC2t 的-模型。引理 4.2.令 a,b W并且,，以下条件成立：(1)如果 a，那么 a 并且 a。(2)如果 ac
18、，那么 ac或者 ac。(3)如果 a，那么 a 或者 a。(4)如果 ac，那么 ac并且 ac。(5)如果 a，那么 ac或者 a。(6)如果 ac，那么 a 并且 ac。证明.由-饱和的定义和 GC2t 相应的联结词规则，条件(1)到(6)容易证明。引理 4.3.令 M是 GC2t 的正则-模型。对所有公式 并且 a ，a当且仅当 M,a 。证明.对公式 的复杂度归纳证明。原子公式的情况显然成立。由归纳假设可得布尔公式的情况。令 =2。从左到右，设 2 a 并且 RFab。由 2-饱和的定义得 b。由归纳假设得 M,b 。因为 b RF(a)。因此 M,a 2。从右到左，设 M,a 2
19、并且 RFab。由语义定义得 M,b 。由归纳假设得 b。因为 RFab。因此 2 a。当 =，证明类似。定义 4.3.给定 a,b W。令 2 a 并且 2 b。W上的二元关系 RadF、RadP定义如下：RadFab 当且仅当 2 ac蕴含 bc，并且 b 蕴含 a。RadFab 当且仅当 ac蕴含 bc，并且 3 b 蕴含 a。命题 4.1.对任意公式集,和公式，以下条件成立：(1)令 ，规则(adF)在 GC2t 中可允许当且仅当 RadF成立。(2)令 3 ，规则(adP)在 GC2t 可允许当且仅当 RadP成立。76逻辑学研究第 16 卷 第 5 期 2023 年证明.这里只证明
20、(1)。从右至左，设 GC2t 2,2 2。由引理 4.1 得2 a，a，2 a 并且 2 ac。由假设得 bc。如果 ，那么 ，并且如果 ，那么2 2。因为2 b。因此GC2t 2,。从左至右，设 2 ac。令 =a|并且 =|2 a。因为2 a，a 并且 2 a。由假设得 GC2t 2,2 2。那么 GC2t 2,。由引理 4.1 得 a、a 并且 ac。因此 RadF成立。定义 4.4.矢列演算 GC2t 在 W上的二元关系 RKF，RKP定义如下：(1)RKFab 当且仅当 2 a 蕴含 2 a 并且 b。(2)RKPab 当且仅当 a 蕴含 a 并且 b。命题 4.2.令切割规则(C
21、ut)的切割公式 ，对任意公式，以下命题成立：(1)规则(KF)在 GC2t 中可允许当且仅当对任意 a W，2 ac蕴含存在b W使得 RKFab 并且 bc。(2)规则(KF)在 GC2t 中可允许当且仅当对任意 a W，ac蕴含存在b W使得 RKPab 并且 bc。证明.这里只证明(2)。从右至左，设 GC2t 。由引理 4.1 得 a 并且 ac。由假设得存在 b W使得 RKPab 并且 bc。如果 ，那么 a。因为 RKPab。则 b。因此 b。因此 GC2t 。从左至右，设 ac。令 =|a。因为 a 并且 ac。则 GC2t 。由假设得 GC2t 。由引理 4.1 得存在 b
22、 W使得 b 并且 bc。因此 RKPab。引理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 的某个有穷正则框架上为假。
23、由 GC2t 的可靠性得 在 GC2t 中不可证。称 HC2t 具有有穷模型性质，如果存在正则框架类 C 使得对所有 HC2t 的定理，C 并且所有不是 HC2t 的定理，在 C 中的某个有穷框架上为假。涂保勋非正规模态逻辑 C2 的时态扩张77推论 1.HC2t 具有有穷模型性质并且 HC2t 可判定。证明.令 CF 为所有正则框架类。由 HC2t 得可靠性得所有 HC2t 中的定理 都有效。由 HC2t 的完全性和引理 4.4 得，所有不是 HC2t 的定理，在 CF 中的某个有穷框架上为假。因此 HC2t 具有有穷模型性质并且 HC2t 可判定。5GC2t 的插值定理定义5.1.GC2t
24、是将GC2t中的规则(Cut)，(adF)，(adP)分别替换成(Cut)，(adF)，(adP)，公理模式和其他规则保持不变得到的矢列演算。其中规则(Cut)，(adF)，(adP)分别定义如下：,(Cut),其中 Sf()。2,(adF)2,2 2,3,(adP),其中 Sf()，3 Sf()。我们在上一节证明了 GC2t 的子公式性质。由 GC2t 的子公式性质得 GC2t 和GC2t等价。在这一节，我们将要证明 GC2t的插值定理。从而得到 GC2t 的插值性质。定义 5.2.我们用 表示 和 的并。对任意矢列 ，称(1:1);(2:2)是 的划分，如果 1 2=and 1 2=。令
25、GC2t 。对任意 的划分(1:1);(2:2)，称公式 是(1:1);(2:2)的插值，如果以下条件满足：(1)GC2t 1 1,，(2)GC2t,2 2，(3)var()var(1,1)var(2,2)，其中 var()在 中所有变元的集合。定理 5.1.如果 GC2t 并且(1:1);(2:2)是 的划分，那么存在公式 使得 是(1:1);(2:2)的插值。证明.设 GC2t 并且(1:1);(2:2)是 的划分。令 D 是矢列 在GC2t的推导。对|D|归纳证明存在公式使得是(1:1);(2:2)的插值。78逻辑学研究第 16 卷 第 5 期 2023 年(1)设|D|=0。那么 是公
26、理。以下有四种情况，在这四种情况下，变元条件显然满足。(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)。因为 ,11,并且 ,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)。因为 11,并且 ,2 2。因此 是插值。(1.2)是(A2：,)的特例，分以下情况。(1.2.1)
27、(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：2,)的特例，分以下情况。(1.3.1)(1:1);(2:2)=(2,1:1);(2:2,)。因为 2,11,并且 ,2 2,。因此 是插值。(1.3.2)(1:1);(2:2)=(2,1:1,);(2:2)。因为 2,11,并且 ,2 2。因此 是插值。(1.3.3)(1:1);(2:2)=(1:1);(2,2:2,)。因为 11,并且 ,2,2 2,。因此 是插值。(1.
28、3.4)(1:1);(2:2)=(1:1,);(2,2:2)。因为 11,并且 ,2,2 2。因此 是插值。(1.4)是(A4,2)的特例。证明类似。(2)设|D|0。那么 由推理规则(R)得到。这里只验证规则(adF)和(KF)。(2.1)(R)是(adF)，则推导的最后一步是：2,(adF)2,2 2令(2,1,21:2,2,22)是 2,2 2 的划分。往证存在插值 使得 GC2t 2,1,21 并且 GC2t,2,2,22 2，var()var(1,21)var(2,22,2)。由归纳假设得，存在公式 使得(1a)2,1,1 涂保勋非正规模态逻辑 C2 的时态扩张79(1b),2,2,
29、2(1c)var()var(1,1)(2,2,)由(1a)运用规则(adF)得 2,1,21 2。由(KF)和(1b)得 2,2,22,22 2。显然 2,2,22,2 2,22,2,22。因此 2,2,2,22 2。因为 var()var(1,1)var(2,2)。显然var(2)var(1,21)var(2,22)。因此 2 是插值。(2.2)(R)是(KF)，则推导的最后一步是：(KF)2 2令(21:22)是 2 2 的划分。往证存在插值 使得 GC2t 21 并且 GC2t,22 2，var()var(21)var(22,2)。由归纳假设得存在公式 使得(1a)1(1b),2(1c)
30、var()var(1)var(2,)由(1a)运用规则(KF)得 21 2。由(1b)运用规则(KF)得 2(,2)2。显然 2,22 2(,2)。因此 2,22 2。因为 var()var(1)var(2,)。显然var(2)var(21)var(22,2)。因此2是插值。参考文献1E.J.Lemmon,1996,“Algebraic semantics for modal logic I”,The Journal of Symbolic Logic,31(1):4665.2A.Maruyama,2003,Towards Combined System of Modal LogicsA Sy
31、ntactic and SemanticStudy,phdthesis,School of Information Science,Japan Advanced Institute of Science and Tech-nology.3A.Maruyama,S.Tojo and H.Ono,2001,“Decidability of temporal epistemic logics for multi-agent models”,Proceedings of the ICLP0 Workshop on Computational Logic in Multi-Agent Sys-tems(
32、CLIMA-01),pp.3140.4M.Takano,1992,“Subformula property as a substitute for cut-elimination in modal propositionallogics”,Mathmatica Japonica,37(6):11291145.5M.Takano,2001,“A modified subformula property for the modal logics K5 and K5D”,Bulletinof the Section of Logic,30(2):115122.6马明辉，王善侠，邓辉文，“极小非正规时
33、序逻辑的矢列式演算系统”，中国科学：信息科学，2017 年第 1 期，第 3146 页。（责任编辑：袁之）80逻辑学研究第 16 卷 第 5 期 2023 年Temporal Extension of Non-Normal Modal Logic C2Baoxun TuAbstractWe build another sequent calculi GC2t for non-normal temporal logic C2t.Apply-ingTakanossemanticmethod,weshowthesubformulapropertyof GC2t.Consequentlywe show the finite model property and decidability of GC2t.Furthermore,we show theinterpolation property of GC2t.Baoxun TuInstitute of Logic and Cognition,Sun Yat-sen UniversityDepartment of Philosophy,Sun Yat-sen U
