Coalgebraic modal logic: soundness, completeness and decidability of local consequence

This paper studies finitary modal logics, interpreted over coalgebras for an endofunctor, and establishes soundness, completeness and decidability results. The logics are studied within the abstract framework of coalgebraic modal logic, which can be instantiated with arbitrary endofunctors on the ca...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2003-12, Vol.309 (1), p.177-193
Main Author: Pattinson, Dirk
Format: Article
Language:English
Subjects:
Exact sciences and technology
General logic
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Sciences and techniques of general use
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper studies finitary modal logics, interpreted over coalgebras for an endofunctor, and establishes soundness, completeness and decidability results. The logics are studied within the abstract framework of coalgebraic modal logic, which can be instantiated with arbitrary endofunctors on the category of sets. This is achieved through the use of predicate liftings, which generalise atomic propositions and modal operators from Kripke models to arbitrary coalgebras. Predicate liftings also allow us to use induction along the terminal sequence of the underlying endofunctor as a proof principle. This induction principle is systematically exploited to establish soundness, completeness and decidability of the logics. We believe that this induction principle also opens new ways for reasoning about modal logics: Our proof of completeness does not rely on a canonical model construction, and the proof of the finite model property does not use filtrations.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(03)00201-9