刘虎：分支时空结构上时态逻辑的公理化问题

6月23日下午2:30-4:30，中山大学哲学系副教授刘虎受我中心邀请做了题为“分支时空结构上时态逻辑的公理化问题”的学术报告。与会师生积极参与，讨论热烈。

刘从我们熟悉的线性时间结构（LT）和分支时间结构（BT）讲起，引入分支时空结构（BST）。与BT相比，BST少了历史线性条件（linear order condition of a history），而多了弱优先选择原则（WPCP）、不相容原则(IP)和弱历史连接(WHC)。刘接着介绍了线性时间的语言、线性时间的语义和分支时间的语义。基于两种不同的分支时间的语义，可以得到两种不同的分支时间逻辑（BTL）：Peircean分支时间逻辑和Ockhamist分支时间逻辑。

我们采用的语言是基本时态语言加四个模态算子：G, H, ?, S。要公理化BST上的时态逻辑，面临两个困难：一是禁自返性是不可表达的；二是路径算子?的语义条件是二阶条件。对于二阶问题的解决有Ockhamist Frame 、Kamp Frame 和Bundled Tree 三种方法。

一方面，我们可以从分支时空结构（BST）出发，定义基本结构（BS）。然后对BS加以限制，从而得到Ockhamist BST。Ockhamist BST 满足 Dis+DH+PI+MH+IP+WHC+WPCP。另一方面，我们可以从分支时空结构出发，定义捆绑世界（Bundled World）。可以证明，定义在BW上的语义和Ockhamist BST上的语义等价。

我们能够公理化右连续的Dis+DH+WHC+MH+IP+WPCP-结构上的逻辑，但还不能公理化Ockhamist BST上的逻辑。因为我们得到的逻辑所刻画的结构和分支时空结构有如下三点不同：右连续的（Right serial）、捆绑的（Bundled）、非过去同构（No PI）。

（徐召清)