非正规模态逻辑C2的时态扩张

Temporal Extension of Non-Normal Modal Logic C2

本文构建了非正规时态逻辑C2t的矢列演算GC2t。运用高野道夫(M.Takana)的语义方法证明了GC2t的子公式性质,进而证明了GC2t的有穷模型性和可判定性。另外,本文还证明了GC2t的插值性质。

We build another sequent calculi GC2t for non-normal temporal logic C2t.Applying Takano’s semantic method,we show the subformula property of GC2t.Consequently we show the finite model property and decidability of GC2t.Furthermore,we show the interpolation property of GC2t.