Final Coalgebras and the Hennessy-Milner Property
The existence of a final coalgebra is equivalent to the existence of a
formal logic with a set (small class) of formulas that has the
Hennessy-Milner property of distinguishing coalgebraic states up to
bisimilarity. This applies to coalgebras of any functor on the category
of sets for which the bisimilarity relation is transitive. There are
cases of functors that do have logics with the Hennessy-Milner
property, but the only such logics have a proper class of
formulas.
The main theorem gives a representation of states of the final
coalgebra as certain satisfiable sets of formulas. The key technical
fact used is that any function between coalgebras that is
truth-preserving and has a simple codomain must be a coalgebraic
morphism.