Completeness for the coalgebraic cover modality

Clemens Kupke, Alexander Kurz, Yde Venema

Research output: Contribution to journalArticle

13 Citations (Scopus)

Abstract

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.
Original languageEnglish
Article number2
JournalLogical Methods in Computer Science
Volume8
Issue number3
DOIs
Publication statusPublished - 31 Jul 2012

Fingerprint

Boolean algebra
Modality
Functor
Completeness
Cover
Algebra
Logic
Semantics
Acoustic waves
Adjunction
Valid Inequalities
Classical Logic
Pullback
Propositional Logic
Axiomatization
Soundness
Arbitrary

Keywords

  • Coalgebra
  • modal logic
  • relation lifting
  • completeness
  • cover modality
  • presentations by generators and relations

Cite this

Kupke, Clemens ; Kurz, Alexander ; Venema, Yde . / Completeness for the coalgebraic cover modality. In: Logical Methods in Computer Science. 2012 ; Vol. 8, No. 3.
@article{f5748db0d53f41bcab9e5372e5f11d76,
title = "Completeness for the coalgebraic cover modality",
abstract = "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.",
keywords = "Coalgebra, modal logic, relation lifting, completeness, cover modality, presentations by generators and relations",
author = "Clemens Kupke and Alexander Kurz and Yde Venema",
note = "DOI link not working",
year = "2012",
month = "7",
day = "31",
doi = "10.2168/LMCS-8(3:2)2012",
language = "English",
volume = "8",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
number = "3",

}

Completeness for the coalgebraic cover modality. / Kupke, Clemens; Kurz, Alexander; Venema, Yde .

In: Logical Methods in Computer Science, Vol. 8, No. 3, 2, 31.07.2012.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Completeness for the coalgebraic cover modality

AU - Kupke, Clemens

AU - Kurz, Alexander

AU - Venema, Yde

N1 - DOI link not working

PY - 2012/7/31

Y1 - 2012/7/31

N2 - 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.

AB - 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.

KW - Coalgebra

KW - modal logic

KW - relation lifting

KW - completeness

KW - cover modality

KW - presentations by generators and relations

UR - http://www.lmcs-online.org/ojs/viewarticle.php?id=828&layout=abstract

U2 - 10.2168/LMCS-8(3:2)2012

DO - 10.2168/LMCS-8(3:2)2012

M3 - Article

VL - 8

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 3

M1 - 2

ER -