拟传递模态逻辑的有限模型性质

确立了拟传递模态逻辑 $\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box p$ 的有限模型性质。该模态逻辑被保守地扩展为时态逻辑 $\mathsf{Kt}_2^3$。我们给出 $\mathsf{Kt}_2^3$ 的 Gentzen 相继式演算 $\mathsf{G}$。相继式演算 $\mathsf{G}$ 通过有限语法构造具有有限代数性质。由此可知 $\mathsf{Kt}_2^3$ 与 $\mathsf{K}_2^3$ 具有有限模型性质。