Strongly Complete Logics for Coalgebras

TL;DR

This paper develops a uniform framework for finitary logics of set-based coalgebras, proving strong completeness for a broad class of functors that preserve algebraic structures, with implications for transition system modeling.

Contribution

It provides a general construction of strongly complete finitary logics from any set-functor that preserves sifted colimits, linking algebraic and coalgebraic structures.

Findings

Finitary presentation of functors via operations and equations

Extension of J{ó}nsson and Tarski's theorem to ind-completions

Strong completeness of the constructed logic for functors preserving sifted colimits

Abstract

Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the category of algebras for the functor is obtained compositionally from the presentations of the underlying category and of the functor. Part II investigates algebras for a functor over ind-completions and extends the theorem of J{\'o}nsson and Tarski on canonical extensions of Boolean algebras with operators to this setting. Part III shows, based on Part I, how to associate a finitary logic to any finite-sets preserving functor T. Based on Part II we prove the logic to be strongly complete under a reasonable condition on T.