In modal logic, van Benthem's theorem characterizes propositional modal logic as the fragment of first-order logic that is invariant under bisimulation. The theorem was proven by Johan van Benthem in his doctoral thesis, Modal Correspondence Theory (1976). A formal statement and game-theoretic proof of van Benthem's theorem is provided by Otto.
Formal Statement The following is based on Otto. Consider formulas in first-order logic with the signature , where is a binary relation symbol and are unary relation symbols. A Kripke model is a structure with the same signature. A pointed Kripke model is a pair where is a Kripke model and . We write if for some bisimulation .
A formula with one free variable in first-order logic is invariant under bisimulation if for all pointed Kripke models , implies that .
Van Benthem's theorem states that the following are equivalent:
is invariant under bisimulation. is logically equivalent to a formula in propositional modal logic. The statement above shows that the fragment of first-order logic invariant under bisimulation can be translated into propositional modal logic. The converse is given by the standard translation, which shows that every formula in modal logic can be translated into a formula in first-order logic. These formulas are invariant under bisimulation, since modal logic is invariant under bisimulation.
Similar Results While van Benthem showed that the theorem holds over the class of (finite and infinite) Kripke models, Rosen showed that the theorem also holds over the class of finite Kripke models.
Theorems analogous to van Benthem's theorem have been found for various modal logics. For example, Janin and Walukiewicz showed that modal μ-calculus is the fragment of monadic second-order logic invariant under bisimulation.
References