Rt时态逻辑

引入Rt算子，将时态词换成事件发生的具体时刻，从而将句子的时态去掉后进行处理的时态逻辑，其中Rt(p)表示“P在时间t成立”。这种类型的时态逻辑源于J．洛斯于1947年研究归纳推理的密尔方法时提出的一个系统，1957年A．N．普赖尔在《时间和模态》中也提出过类似的系统。N．雷谢尔是此类时态逻辑的重要代表人物。

洛斯1947年提出的系统是在命题演算基础上加入下述公理和规则而构成的：

　　(L1)Rt(p)Rt(p)

　　(L2)Rt(p→q)→［Rt(p)→Rt(q)］

　　(L3)(t)Rt(p)→p

　　(R)若┝T，则┝Rt(T)

这里，(L3)是说，若一命题在所有时间内普遍地真，则它不受限定地真。规则(R)是说，定理在任意或每一时间内真。洛斯的系统还有另外一些公理，但若假定t在实数域内取值，则它们都可归约为上述公理。

A．N．普赖尔提出了两个系统，分别命名为P和P，它们都是在命题演算的基础上加入一些公理和规则得到的。其中P的构造如下：

公理：(A1)～(A3)=(L1)～(L3)

　　　(A4) Rt'［Rt(p)］→Rt(p)

　　　(R)若┝T，则┝Rt(T)

系统P除有规则(R)外，还有下述公理

　　　(A1)～(A2)=(L1)～(L2)

　　　(A3、2) Rn(p)→p(这里n表示现在)

　　　(A4，2) Rt'［R(p)］→R(t'+t)(p)

　　　(A5) Rt'［(t)Rt(p)］→(t)Rt'［Rt(p)］

N．雷谢尔1966年在《关于时间函词逻辑》一文中，提出了两个Rt型时间逻辑系统R1和R2，两个系统都有规则(R)，此外分别有下述公理：

这里，(R)和(R，2)分别是用来处理叠置的Rt算子的。(R4)是说：最里面的算子是首先完全确定的。这等于假设了一个定点座标系，它具有一个始终确定的原点：假定p在确定的时间t真，则“p在时间t真”在任意时间t'也真。(R，2)则先确定最外面的算子，然后根据较外面的算子所确定的状况来逐次确定较里面的算子，这等于假设了一个动点座标系。(R5)则表明，Rt算子可以移过一个不相干的量词。

Rt型时态逻辑与拓扑逻辑有密切关系。除了参数(即Rt中的t)的取值范围不同而外，时态逻辑系统Rl和R2与拓扑逻辑系统Pl和PI实际上是相同的。这说明，时间和空间的逻辑在结构方面有着相同的基本性质。