Completeness for the coalgebraic cover modality (Q2904618)

Coalgebras represent an algebraic tool able to describe several kinds of state/transition-based systems. Coalgebraic logic investigates this structure from a logical point of view, aiming to provide a derivation system for it. The authors start from the Set-endofunctor \(T\), which defines coalgebras of a given type and gives a modal operator firstly introduced by Larry Moss. The paper gives a sound and complete derivation system for such a logic. A stratified method is used ranking formulas with respect to their modal depth, so that, e.g., the proof that two formulas of depth \(n\) are logical equivalent, uses only formulas of modal depth equal to \(n\). The method is also algebraic so that equations are used and the derivation system \(M\) can be described as an endofunctor on the category of Boolean algebras. Connections between \(T\) and \(M\) give the soundness and completeness result.NEWLINENEWLINE\(M\) is shown to be finitary and preserving embeddings, and the Lindenbaum-Tarski algebra for this coalgebraic modal logic can be identified with the initial algebra for this functor.