On Distinguishing Sets of Structures by First-Order Sentences of Minimal Quantifier Rank

We investigate the distinguishability of sets of relational structures concerning a class of structures in the following sense: for a fixed class of structures, given two sets of structures in this class, find a first-order formula of minimal quantifier rank that distinguishes one set from the other. We consider the following classes of structures: monadic structures, equivalence structures, and disjoint unions of linear orders. We use results of the Ehrenfeucht–Fraisse game on these classes of structures in order to design an algorithm to find such a sentence. For these classes of structures, the problem of determining if the Duplicator has a winning strategy in an Ehrenfeucht–Fraisse game is solved in polynomial time. We also introduce the distinguishability sentences which are sentences that distinguish between two given structures. We define the distinguishability sentences based on necessary and sufficient conditions for a winning strategy in an Ehrenfeucht–Fraisse game. Our algorithm returns a boolean combination of such sentences. We also show that any first-order sentence is equivalent to a boolean combination of distinguishability sentences. Finally, we also show that our algorithm's running time is polynomial in the size of the input.