如果一个知识系统包含命题A及其否定┐A，那么这个知识系统就是不协调的。我们的经验常识大都是不协调的，一些包含海量信息的巨型知识系统也是不协调的知识系统。对于一个存在不协调信息的知识系统，我们如何限制不协调信息的作用范围，合理地使用已有的知识系统进行推理、预测，首先必须解决的问题是如何描述包含不协调信息的知识系统的推理机制。
对此问题，目前主要存在两种基本的研究路径。一种就是弗协调逻辑(Paraconsistent Logic)[1]方案。其基本策略是改变人们对于经典否定的理解，即把命题A和其否定┐A之间的关系不再理解为经典的矛盾关系，而是解释为通常的下反对关系。[2]这样A和其否定┐A就可以同真，从而经典的逻辑有效式A∧┐A→B在此解释下就不是一个逻辑有效式了，因之任意一个信息B就不能总可以从不协调信息A和┐A推出，不协调信息A和┐A的作用范围就被限制。[3]这种策略又有两种实现方式。一种就是基于对A和┐A之间的下反对关系的理解来构建逻辑系统，以此来描述不协调知识系统的推理机制。这主要有巴西逻辑学家科斯塔(N.C.A.da Costa)建立起来的一系列弗协调逻辑系统C[,n]（1≤n＜ω）。[4]另一种实现方式是在经典逻辑内部来描述通常的下反对关系，从而实现对不协调信息的描述。这种实现方式是在经典命题逻辑的系统内，增加一个初始一元算子*，定义引入另两个一元算子和△，建立一个经典命题逻辑的扩充系统。在该扩充系统内，有遵守矛盾律和排中律的经典否定算子，有遵守矛盾律而不遵守排中律的构造性否定算子，有不遵守矛盾律而遵守排中律的弗协调否定算子，还有既不遵守矛盾律又不遵守排中律的差等否定算子。[5-6]
另一种基本的研究路径是不改变人们对于经典否定的理解，即把命题A和其否定┐A之间的关系仍然理解为经典的矛盾关系，而在推理关系的描述上进行修正，从而弱化系统的推理功能，特别是弱化矛盾信息的推理功能，以此来限制不协调信息的作用范围。这也主要有两种实现方式，一种就是直接限制经典的推出关系；[4]另一种是修正经典的蕴涵关系，然后根据蕴涵关系和推理关系的联系来实现对于矛盾信息的限制。笔者提出的“知识蕴涵”概念就是修正经典的蕴涵关系，从而实现对包含不协调信息知识系统的推理机制的描述。[7-8]在《知识蕴涵逻辑系统》一文中，作者完成了知识蕴涵命题逻辑系统的构建；在《知识蕴涵模态逻辑系统》一文中，作者完成了知识蕴涵模态命题逻辑系统的构建，并且证明了严格蕴涵悖论在该系统中不会出现。[8]本文拟在上述工作的基础上，将知识蕴涵逻辑系统扩充到时态上，构建知识蕴涵时态命题逻辑系统，以此来描述包含时态信息的不协调知识系统的推理机制。
一、知识蕴涵时态逻辑公理系统的构建
知识蕴涵时态命题逻辑的形式语言由知识蕴涵命题逻辑语言附加时态符号而得。包括下列四类初始符号：
其中，第三类符号G，直观上想要表达的是“将来永远……”(be going to)，H直观上想要表达的是“过去一直……”(had being)。可分别读作“永远”、“一直”。
那么所有公式都具有性质P。
知识蕴涵时态命题逻辑公理系统是在知识蕴涵命题逻辑系统D[7]的基础上扩充而成的，包括下列公理模式：
(Ax1)全体知识蕴涵命题逻辑的定理；
(Ax2)G(A→(A→B)→(GA→(GA→GB))；
(Ax3)H(A→(A→B))→(HA→(HA→HB))；
(Ax4)PGA→A；
(Ax5)FHA→A；
(Ax6)如果A是公理，GA也是公理；
(Ax7)如果A是公理，HA也是公理。
知识蕴涵时态逻辑极小系统的推理规则只有一条，即分离规则(modus ponens)：由A和A→B可以推出B，简记为MP。
定义4 一个有穷的公式序列
在知识蕴涵时态逻辑中有下列导出规则。
定理2
(1)G规则：如果├ A，则├ GA；
(2)H规则：如果├ A，则├ HA；
(3)G→规则：如果├ A→(A→B)，则├ GA→(GA→GB)；
(4)H→规则：如果├ A→(A→B)，则├ HA→(HA→HB)；
(5)F规则：如果├ A→(A→B)，则├ FA→(FA→FB)；
(6)P规则：如果├ A→(A→B)，则├ PA→(PA→PB)。
在知识蕴涵时态逻辑中可以证明下列定理（限于篇幅，我们略去其中的证明）：
二、知识蕴涵时态逻辑公理系统的形式语义
定义5 设是任一二元组，是知识蕴涵时态逻辑框架（简称框架），当且仅当，T是任一非空集，R是T上的二元关系。
(1)V（┐A，t)=1，当且仅当V(A，t)=0；
(2)v(A∧B，t)=1，当且仅当，v(A，t)=v(B，t)=1；
(3)如果v(A，t)=v(B，t)，那么v(A→B，t)=1；
(4)如果v(A，t)=1，v(B，t)=0，那么v(A→B，t)=0；
(5)如果v(A，t)=0，v(B，t)=1，并且A、B相关，那么v(A→B，t)=1；
(6)V(GA，t)=1，当且仅当，对于任何t'∈T，如果tRt'，则V(A，t')=1；
(7)V(HA，t)=1，当且仅当，对于任何t'∈T，如果t'Rt，则V(A，t')=1。
由此定义不难得出：
(8)V(A∨B，t)=1，当且仅当V(A，t)=1或者V(B，t)=1；
(9)，当且仅当（V(A，t)=1并且V(B，t)=1）或者（V(A，t)=0并且V(B，t)=0）；
(10)，当且仅当V(A，t)=0或者V(B，t)=1；
(11)V(FA，t)=1，当且仅当，存在t'∈T，tRt'并且V(A，t')=1；
(12)V(PA，t)=1，当且仅当，存在t'∈T，t'Rt并且V(A，t')=1。
定义9 设A是任一公式，若A在任一知识蕴涵时态逻辑模型上都是有效的，则称公式A为有效式，记作。
定理3 设A、B为任意的知识蕴涵逻辑公式，则
(1)若A是知识蕴涵命题逻辑系统的定理，则；
证明：
我们给出(2)的证明，其他略。
假设不成立，则一定存在一时态逻辑模型，使得：
不成立，所以，存在t∈T，
(1)V(PGA→A，t)=0
由(1)可得：
(2)V(PGA，t)=1
(3)V(A，t)=0
由(2)可得：
(4)存在t'∈T，t'Rt并且V(Ga，t')=1
由(4)可得：
(5)V(A，t)=1
(3)和(5)矛盾，所以假设不成立。
定理4 如果，并且，那么。
定理5
三、知识蕴涵时态逻辑公理系统的元性质
可以证明知识蕴涵时态逻辑极小系统具有可靠性和完全性。
证明：
(1)只需证明系统的公理都是有效的，并且分离规则保持有效性即可。而这由定理3、定理4和定理5保证。
(2)由(1)可证。
下面我们将直接使用知识蕴涵命题逻辑中给出的协调集、极大协调集概念和定理。我们讨论的系统S指的是知识蕴涵时态逻辑极小系统的扩充。
定义10 设∑和∑′是两个S极大协调集，并且满足：
如果A∈∑，则PA∈∑′。
则称∑′是∑的将来伴随集，称∑是∑′的过去伴随集。记为。
定理7 设∑和∑′是两个S极大协调集，则如下的叙述是等价的。
(1)
(2)如果GB∈∑，则B∈∑′；
(3)如果C∈∑，则FC∈∑；
(4)如果HD∈∑′，则D∈∑。
证明：
定理8 设∑是S极大协调集，。
(1)如果FA∈∑，则存在S极大协调集∑′，使得并且A∈∑′；
(2)如果PA∈∑，则存在S极大协调集∑′，使得并且A∈∑′。
证明：
(1)该证明可分作三步来完成。
这与∑是S极大协调集相矛盾，所以假设不成立。
证明：
施归纳于公式A的结构。
(1)A为原子公式，根据定义，显然成立；
(2)A=┐B或者A=B∨C或者A=B→C与知识蕴涵命题逻辑中的证明相同；
(3)A=GB。
杜国平(1965～），男，江苏盱眙人，南京大学哲学系教授，逻辑学博士。南京大学哲学系，
（原载《安徽大学学报》2009年5期。录入编辑：乾乾）