| Publication type: |
Article |
| Author: |
Dirk Pattinson, Lutz Schröder |
| Title: |
Cut Elimination in Coalgebraic Logics |
| Volume: |
208 |
| Page(s): |
1447 – 1468 |
| Journal: |
Information and Computation |
| Year published: |
2010 |
| Abstract: |
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 CK and CK+ID. |
| Internet: |
http://dx.doi.org/10.1016/j.ic.2009.11.008 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/cut-ext.pdf |
| Keywords: |
Coalgebra modal logic cut elimination interpolation coalition logic conditiona logic |
| Status: |
Reviewed |
| Last updated: |
18. 03. 2011 |
