Over words, two variables are as powerful as one quantifier alternation
Denis Thérien, Thomas Wilke · 1998
We show a property of strings is expressible in the two-variable fragment of fist-order logic if and only if it is expressible by both a Cs and a II2 sentence.We thereby establish:where UTL stands for the string properties expressible in the temporal logic with 'eventually in the future' and 'eventually in the past' as the only temporal operators and UL stands for the class of unambiguous languages.This enables us to show that the problem of determining whether or not a given temporal string property belongs to UTL is decidable (in exponential space), which settles a hitherto open problem.Our proof of Cs n II2 = F02 involves a new combina- torial characterization of these two classes and introduces a new method of playing Ehrenfeucht-Fraikse games to verify identities in semigroups.