Monadic second-order logic on equivalence relations
Keywords:
decidability, elimination of second-order quantifiers, equivalence relations, finite model property, MSO sentencesAbstract
This paper is devoted to exploring expressible power of monadic second-order sentences over the class of all relational structures containing only finite number of equivalence relations which are in local agreement (i.e. for any point of the universe the corresponding equivalence classes with set theoretic inclusion form linear order). Using the pebble games we prove the finite model property and establish an effective translation of these sentences in the first-order language preserving the models. So, the monadic second-order language over the considered class of relational structures has the same expressible power as the first-order language and the monadic second-order theory of this class of structures is decidable.