Model constructions for Moss' coalgebraic logic

We discuss two model constructions related to the coalgebraic logic introduced by Moss. Our starting point is the derivation system M _T for this logic, given by Kupke, Kurz and Venema. Based on the one-step completeness of this system, we first construct a finite coalgebraic model for an arbitrary M _T -consistent formula. This construction yields a simplified completeness proof for the logic M _T with respect to the intended, coalgebraic semantics. Our second main result concerns a strong completeness result for M _T , provided that the functor T satisfies some additional constraints. Our proof for this result is based on the construction, for an M _T -consistent set of formulas A, of a coalgebraic model in which A is satisfiable.