Schroder, LutzPattinson, Dirk2015-12-13March 20-29783642120312http://hdl.handle.net/1885/83604We lay the foundations of a first-order correspondence theory for coalgebraic logics that makes the transition structure explicit in the first-order modelling. In particular, we prove a coalgebraic version of the van Benthem/Rosen theorem stating that both over arbitrary structures and over finite structures, coalgebraic modal logic is precisely the bisimulation invariant fragment of first-order logic.Keywords: Arbitrary structures; Bisimulations; Coalgebraic; Coalgebraic logic; Finite structures; First order logic; First-order; Modal logic; Transition structures; Formal logic; Computer software201010.1007/978-3-642-12032-9_232016-02-24