Coalgebraic logic Original Research Article

We present a generalization of modal logic to logics which are interpreted on coalgebras of functors on sets. The leading idea is that infinitary modal logic contains characterizing formulas. That is, every model-world pair is characterized up to bisimulation by an infinitary formula. The point of our generalization is to understand this on a deeper level. We do this by studying a fragment of infinitary modal logic which contains the characterizing formulas and is closed under infinitary conjunction and an operation called Δ. This fragment generalizes to a wide range of coalgebraic logics. Each coalgebraic logic is determined by a functor on sets satisfying a few properties, and the formulas of each logic are interpreted on coalgebras of that functor. Among the logics obtained are the fragment of infinitary modal logic mentioned above as well as versions of natural logics associated with various classes of transition systems, including probabilistic transition systems. For most of the interesting cases, there is a characterization result for the coalgebraic logic determined by a given functor. We then apply the characterization result to get representation theorems for final coalgebras in terms of maximal elements of ordered algebras. The end result is that the formulas of coalgebraic logics can be viewed as approximations to the elements of a final coalgebra.