Journal of Logic and Computation Advance Access published online on December 17, 2008
Journal of Logic and Computation, doi:10.1093/logcom/exn096
Original Papers |
Rank-1 Modal Logics are Coalgebraic
DFKI-Lab and Department of Computer Science, University of Bremen, Germany.
E-mail: Lutz.schroeder{at}dfki.de
Department of Computing, Imperial College, London, UK.
E-mail: dirk{at}doc.ic.ac.uk
Received 28 November 2007.
| Abstract |
|---|
Coalgebras provide a unifying semantic framework for a wide variety of modal logics. It has previously been shown that the class of coalgebras for an endofunctor can always be axiomatized in rank 1. Here we establish the converse, i.e. every rank-1 modal logic has a sound and strongly complete coalgebraic semantics. This is achieved by constructing for a given modal logic a canonical coalgebraic semantics, consisting of a signature functor and interpretations of modal operators, which turns out to be final among all such structures. The canonical semantics may be seen as a coalgebraic reconstruction of neighbourhood semantics, broadly construed. A finitary restriction of the canonical semantics yields a canonical weakly complete semantics which moreover enjoys the Hennessy–Milner property. As a consequence, the machinery of coalgebraic modal logic, in particular generic decision procedures and upper complexity bounds, becomes applicable to arbitrary rank-1 modal logics, without regard to their semantic status; we thus obtain purely syntactic versions of such results. As an extended example, we apply our framework to recently defined deontic logics. In particular, our methods lead to the new result that these logics are strongly complete.
Keywords: Modal logic; coalgebra; neighbourhood frames; deontic logic; decision procedures