Quantifier Alternation in First-order Logic with Two Variables over Words

It has long been known that every first-order formula over linear order is equivalent to one that uses only three bound variables.  This talk is about what properties of finite words can be defined if we use only two variables.

I'll survey some of the older results in this domain, especially those of Thérien and Wilke giving an effective characterization, in terms of the syntactic monoid, of the languages definable in two-variable logic. I will also present some recent work, done in collaboration with Andreas Krebs, extending this characterization to the levels of the quantifier alternation hierarchy in two-variable logic.  In my opinion, the answers to these questions, and especially the techniques used to obtain the answers, are more interesting than the questions themselves, and provide a nice glimpse into the power of algebraic techniques applied to these questions about logic.

If time permits, I will describe what happens when modular counting quantifiers are added into the mix, and speculate somewhat irresponsibly about a possible link to circuit complexity.