A complete deductive calculus for (implications of) coequations

We begin with a brief introduction to coalgebras for an endofunctor and discuss the duals of Birkhoff's variety theorem and the quasi-variety theorem. These theorems suggest a notion of coequations for categories of coalgebras. Namely, we take coequations to be predicates over the carrier of cofree coalgebras, where coequation satisfaction is interpreted in terms of projectivity. This development suggests the question: What is the dual of Birkhoff's completeness theorem? Previously, we have seen that the formal dual consists of two modal operators on coequations, that is, closure under deductive rules dualized to yield two interior operators. Now we extend this result by offering a simple deductive calculus for reasoning about coequations and show that it is complete. Furthermore, we also discuss a deductive calculus for implications between coequations and sketch the completeness proof for it.  

hosted by

social