Characterization, Definability and Separation via Saturated Models

CARLOS ARECES; FACUNDO CARREIRO; SANTIAGO FIGUEIRA

THEORETICAL COMPUTER SCIENCE

ELSEVIER SCIENCE BV

Lugar: Amsterdam; Año: 2014 vol. 537 p. 72 - 86

0304-3975

Three important results about the expressivity of a modal logic L are theCharacterization Theorem (that identifies a modal logic L as afragment of a better known logic), theDefinability theorem (that provides conditions under which a classof L-models can be defined by a formula or a set of formulas of L),and the Separation Theorem (that provides conditions under which two disjoint classesof L-models can be separated by a class definable in L).We provide general conditions under which these results can beestablished for a given choice of model class and modal languagewhose expressivity is below first order logic. Besides some basicconstraints that most modal logics easily satisfy, the fundamentalcondition that we require is that the class of omega-saturated models inquestion has the Hennessy-Milner property with respect to the notionof observational equivalence under consideration.Given that the Characterization, Definability and Separation theorems are among the cornerstones in the model theory of L, this property can be seen as a test thatidentifies the adequate notion of observational equivalence for a particular modal logic.