10.2168/LMCS-8(3:2)2012
Kupke, Clemens
Clemens
Kupke
Kurz, Alexander
Alexander
Kurz
Venema, Yde
Yde
Venema
Completeness for the coalgebraic cover modality
episciences.org
2012
Computer Science - Logic in Computer Science
Mathematics - Logic
F.4.1, I.2.4, F.3.2
contact@episciences.org
episciences.org
2011-01-21T00:00:00+01:00
2016-11-21T15:27:32+01:00
2012-07-31
eng
Journal article
https://lmcs.episciences.org/896
arXiv:1206.4935
1860-5974
PDF
1
Logical Methods in Computer Science ; Volume 8, Issue 3 ; 1860-5974
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.