时态逻辑

研究包含时间因素的命题及推理的逻辑学科，哲学逻辑的一个分支。经典逻辑演算中所讨论的命题不受任何时间的限制，既不涉及时态的变化也不涉及特定的参照时间，它不考虑包含时间因素的推理。时态逻辑则试图把包含时间因素的命题之间的推理关系系统化，从而为涉及时间命题的精确讨论和严格推理提供工具。

时态逻辑的历史可以追溯到古希腊。麦加拉学派的第欧多鲁用时间来定义模态，并且在条件句的真值定义中引入了时间因素。第欧多鲁关于模态概念的定义如下：p是可能的当且仅当p(现在)是真的或在将来某时是真的；p是不可能的当且仅当p(现在)不是真的并且将来永远不是真的；p是必然的当且仅当p(现在)是真的并且将来永远是真的；p不是必然的当且仅当p(现在)不是真的或将来某时不是真的。他关于条件命题的真值定义如下：如果p则q是真的，当且仅当对一切时刻t而言，并非p在t是真的而q在t是假的。亚里士多德则这样定义可能与必然：p是可能的当且仅当p过去是真的或现在是真的或将来是真的；p是必然的当且仅当p过去一直是真的并且现在是真的并且将要永远是真的。中古阿拉伯学者阿维森那发展了第欧多鲁和亚里士多德模态概念，从更复杂的时间角度考虑，提出了4种基本模态关系，由它们构成了13种模态。阿拉伯学者还对直言命题从其主项所表时间的角度进行处理，形成16种直言命题，并将□、◇、、与以上命题结合，构成更复杂的推理。中世纪经院学者讨论了模态词能使主项的指代域扩大的问题，例如萨克森阐明了9条扩大规则，其中有：每一个具有指代作用的词项作为主项，相对于过去时，被扩大到现在存在或已存在的东西；而相对于将来时，则被扩大到现在存在或将存在的东西，等等。可以看出，这里含有明显的时态逻辑因素。此外，司各脱、沃尔他·巴勒、奥卡姆等人也在时态逻辑方面贡献了一些思想。在中世纪以后一段时间内，时间模态问题似乎已被人们遗忘，只是到近代，它才逐步被逻辑学家重新重视。

现代时态逻辑的思想是从20世纪40年代兴起的。来自哲学、解释学、语言学、计算机科学和逻辑科学自身5个方面的动力，促使了时态逻辑的形成。并且，数理逻辑的发展成熟、模态逻辑的形成发展，语言学的发展、古代、中世纪学者的著述，为时态逻辑提供了理论基础。30～40年代，J．麦克塔加特、J．N．芬德利、J．洛斯、H．赖兴巴赫、W．V．O．奎因等一批哲学家、逻辑学家都不同程度地为时态逻辑形式化作出了贡献。麦克塔加特认为，有两种方法区分时间关系：首先，一事件早于某事件，或晚于另外某事件；其次，时间序列上的每一点都是过去或现在或未来。他认为，前一类区别是恒久的，后一类区别却不然。如果M曾先于N，那么M总是先于N。但是，一事件此时是现在，曾经是将来，并且将成为过去。他引入“A序列”表示“遥远的过去——近期的过去——现在——近期的将来——遥远的未来”这一序列，用“B序列”表示“先后”序列。他认为，A序列和B序列是同一问题的两种解释方式。如果选择A序列，则B序列沿固定的A序列滑动；反之不然。并且B序列可转化成A序列，如“M先于N”可转化为“曾经M现在N或现在M将要N”。芬德利继承了麦克塔加特的上述思想，于1941年提出要建立时态的形式演算，这是最早的时态逻辑形式化的构想。他认为，该演算应包含以下命题：

　现在x=现在(现在x)

　将来x=现在(将来x)

　　　 =将来(现在x)

　(x)将来(过去x)

这最后一个公式是说，一切事件，无论是过去的、现在的和将来的，都将成为过去。但它的形式表达有问题，可将其修改为：

　　(现在x)或(过去x)或(将来x)→将来(过去x)

1947年，赖兴巴赫指出，在处理时态时不仅要考虑谈话时间、事件发生时间，还有一个相关时间。如“我将会见吴为”，这里不仅要考虑我会见吴为的时间、谈话的时间，还要考虑比谈话晚的时间，使该事件成为过去。

J．洛斯在1947年研究归纳推理的密尔方法时提出了一套演算系统，其中没有时态词，但有变元p，p等，表示在一定时间内被满足的谓词；还有变量t、t、n、n表示时刻。∪t(p)表示p在时刻t被满足，δtn表示n比t晚，ρtt表示t、t为同一点。洛斯的思想，对于A．N．普赖尔的∪t(p)时态逻辑和N．雷谢尔于1965年建立的系统有直接影响。

奎因在其《语词和对象》一书中认为，有时态的句子不是完整的句子，而是一种谓词。他提出了对自然语言进行语义整编的思想，即用带时态量词的无时态动词代替时态动词，从而把其真值随时间不同而变化的时态语句整编为其真值保持不变的无时态语句，然后用时间量词去扩充标准谓词逻辑，这样就可以用标准逻辑句法表达非形式的时态议论。奎因的这种思想成为范·边沁形式系统的先驱。

时态逻辑的真正开创性工作是由普赖尔作出的。他于1950年应邀在牛津大学就时态逻辑发表了一系列讲演，1957年结集为《时间和模态》一书出版。该书的主要目的在于发展一种能够对日常应用的时态区分进行解释的符号逻辑。在此书中，他在经典命题演算和谓词演算的基础上，通过加入P、F、P、F等几个时态算子和一些不同的时态公理，从而构造3个不同的时态逻辑系统P、P和Q。此书因此成为时态逻辑的奠基性著作，成为现代时态逻辑诞生的标志。

至70年代止，时态逻辑可分为3种类型：第一种类型是以P、F(或G、H)算子为基础的，它由普赖尔最初建构，M．J．莱蒙等许多逻辑学家都为此作出了重要贡献，它是时态逻辑中发展最成熟、也是最重要的一支，与模态逻辑有密切关系；第二种类型是以由洛斯提出的U算子为基础的，普赖尔也做了一些工作，但它的主要工作是由雷谢尔完成的，这一类型与后来发展起来的拓扑逻辑关系密切；第三种类型是由奎因设想，经由范·边沁发展起来的，它不应用特别的时态算子，仅用扩展经典谓词演算来建构。

70年代末至80年代，时态逻辑又有了新发展，突出表现在U－S系统、时态逻辑与模态逻辑、道义逻辑等结合、时间副词和时态谓词逻辑的研究等方面。80年代以来，D．麦克多莫特、J．F．艾伦、J．凯普、范．边沁、Z．曼纳和A．普纽里、J．哈尔帕恩等一批逻辑学家和人工智能专家把时态逻辑应用于人工智能领域，在这方面做了不少工作。