时态逻辑

指研究包含时态变化的命题的逻辑分支。时态逻辑的研究首先从现在、过去和将来这几个时态开始，用F代表将来时态算子，P代表过去时态算子，T代表现在时态算子，把含有这些算子的命题称为时态命题，如“今天下雪”，“拿破仑曾统治过欧洲”，“下届奥运会将在欧洲举行”等等。用这些时态算子，就可以把时态命题形式化。例如，用p代表命题“巴黎下雨”，则

?Pp表示命题“过去巴黎从不下雨”，

Pp∧T?p表示命题“巴黎曾经下雨，现在巴黎不下雨”，

F?p表示命题“将来巴黎不会总下雨”，

?F

p

表示命题“将来巴黎再也不会下雨”。

在时态逻辑研究中，还引进全时间性算子G和H。G读作“将来总有”，G

p

定义为?F?p。H读作“过去总有”，H

p

定义为?P?p。为了把所有真的时态命题全部推演出来，逻辑学家在命题演算的基础上，构造了若干个时态逻辑系统。以时态逻辑的极小系统K

t

为例，它除了把命题演算的重言式作为自己的公理外，增加了下面六条公理：GA→B→(GA→GB)

H (A→B)→(HA→HB)

A→HFA

A→GPA

GA，如果A是公理;

HA如果A是公理;

又增加了若干条推理规则。由此出发，就可把其余的真的时态命题推演出来。