Clemens Kupke ; Alexander Kurz ; Yde Venema - Completeness for the coalgebraic cover modality

lmcs:896 - Logical Methods in Computer Science, July 31, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:2)2012
Completeness for the coalgebraic cover modalityArticle

Authors: Clemens Kupke ; Alexander Kurz ; Yde Venema

    We study the finitary version of the coalgebraic logic introduced by L. Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a so-called coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation. As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic, and we employ Pattinson's stratification method, showing that our derivation system can be stratified in countably many layers, corresponding to the modal depth of the formulas involved. In the proof of our main result we identify some new concepts and obtain some auxiliary results of independent interest. We survey properties of the notion of relation lifting, induced by an arbitrary but fixed set functor. We introduce a category of Boolean algebra presentations, and establish an adjunction between it and the category of Boolean algebras. Given the fact that our derivation system involves only formulas of depth one, it can be encoded as a endo-functor on Boolean algebras. We show that this functor is finitary and preserves embeddings, and we prove that the Lindenbaum-Tarski algebra of our logic can be identified with the initial algebra for this functor.


    Volume: Volume 8, Issue 3
    Published on: July 31, 2012
    Imported on: January 21, 2011
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,F.4.1, I.2.4, F.3.2
    Funding:
      Source : OpenAIRE Graph
    • Coalgebras, Modal Logic, Stone Duality; Funder: UK Research and Innovation; Code: EP/C014014/1
    • ExODA: Integrating Description Logics and Database Technologies for Expressive Ontology-Based Data Access; Funder: UK Research and Innovation; Code: EP/H051511/1
    • Coalgebraic Modal Logic: Fixpoints and Nested Modalities; Funder: UK Research and Innovation; Code: EP/F031173/1
    • Algebra and Coalgebra: the mathematical environments of modal logic; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 639.073.501

    12 Documents citing this article

    Consultation statistics

    This page has been seen 2337 times.
    This article's PDF has been downloaded 550 times.