From modal logic to terminal coalgebras

We define a modal logic whose models are coalgebras of a polynomial functor. Bisimilarity turns out to be the same as logical equivalence. Ideas and concepts of modal logic are directly applied to the theory of coalgebras: we give an axiomatization and define canonical coalgebras. That leads to a completeness result. Each canonical coalgebra proves to be terminal in a certain class of coalgebras. The approach also yields a functional characterization of the terminal coalgebra of all coalgebras with respect to a given polynomial functor.