Strongly complete logics for coalgebras (Q2914235)

This work contributes to the growing field of coalgebraic logic by developing a correspondence between coalgebraic type functors and functorial algebraic syntax along Stone-type dualities. Generally, a type functor determines, via its coalgebras, a type of transition systems, while a functor on a category of algebras (e.g., Boolean algebras) induces logical syntax via its algebras. The principle pursued in this work is to induce the syntax functor from the type functor via a dual adjunction that becomes a dual equivalence when restricted to finite objects. A key result proved on the algebraic side is that a functor has a presentation by operations and equations iff it preserves sifted colimits. Results obtained using the method proposed include a Jónsson-Tarski-type theorem as well as strong completeness of the logic induced from the type functor; the latter result is limited to the case where the type functor preserves finite sets (thus including logics with finitely many modal operators but excluding, e.g., graded modal logic), a restriction lifted in [\textit{L. Schröder} and \textit{D. Pattinson}, LIPICS -- Leibniz Int. Proc. Inform. 3, 673--684 (2009; Zbl 1236.03060)] after online publication (2006) of the current work.