A logic of coequations

Abstract

By Rutten's dualization of the Birkhoff Variety Theorem, a collection of coalgebras is a covariety (i.e., is closed under coproducts, subcoalgebras, and quotients) iff it can be presented by a subset of a cofree coalgebra. We introduce inference rules for these subsets, and prove that they are sound and complete. For example, given a polynomial endofunctor of a signature Σ, the cofree coalgebra consists of colored Σ-trees, and we prove that a set T of colored trees is a logical consequence of a set 5 iff T contains every tree such that all recolorings of all its subtrees lie in S. Finally, we characterize covarieties whose presentation needs only n colors. © Springer-Verlag Berlin Heidelberg 2005.