On Distinguishing Sets of Structures by First-Order Sentences of Minimal Quantifier Rank
Thiago Alves Rocha, Ana Teresa Martins, Francicleber Martins Ferreir · Electronic Notes in Theoretical Computer Science · 2019
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–Fraïssé 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–Fraïssé 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–Fraïssé 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.