Cut elimination in coalgebraic logics

Dirk Pattinson*, Lutz Schröder

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

18 Citations (Scopus)

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 LCK and LCKID.

Original languageEnglish
Pages (from-to)1447-1468
Number of pages22
JournalInformation and Computation
Volume208
Issue number12
DOIs
Publication statusPublished - Dec 2010
Externally publishedYes

Fingerprint

Dive into the research topics of 'Cut elimination in coalgebraic logics'. Together they form a unique fingerprint.

Cite this