时态逻辑

指研究包含时态变化的命题的逻辑分支。时态逻辑的研究首先从现在、过去和将来这几个时态开始，用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是公理；
又增加了若干条推理规则。由此出发，就可把其余的真的时态命题推演出来。