Cut elimination in coalgebraic logics
Cut elimination in coalgebraic logics
复制标题
余代数逻辑中的割消除
DOI：
10.1016/j.ic.2009.11.008
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Lutz Schröder
中科院分区：
文献类型：
--
作者：
D. Pattinson;Lutz Schröder
我们给出了两个一般的证明，削减消除命题模态逻辑，解释了余代数。我们首先调查语义一致性条件之间的公理化的一个特定的逻辑和它的coalgebraic语义，保证切割规则是容许在随后的微积分。然后，我们独立地隔离一组模态规则，保证削减消除的纯语法属性。除了事实上，削减消除举行，我们的主要结果是，语法和语义假设是等价的情况下，逻辑是服从于共代数语义。作为应用，我们给出了一个新的证明（已经知道）的联合逻辑的插值性质和新建立的条件逻辑LCK和LCKID的插值性质。
We give two generic proofs for cut elimination in propositional modal logics, interpreted over coalgebras. We first investigate semantic coherence conditions between the axiomatisation of a particular logic and its coalgebraic semantics that guarantee that the cut-rule is admissible in the ensuing sequent calculus. We then independently isolate a purely syntactic property of the set of modal rules that guarantees cut elimination. Apart from the fact that cut elimination holds, our main result is that the syntactic and semantic assumptions are equivalent in case the logic is amenable to coalgebraic semantics. As applications we present a new proof of the (already known) interpolation property for coalition logic and newly establish the interpolation property for the conditional logics LCK and LCKID.