Two-variable descriptions of regularity

We prove that the class of all languages that are definable in Σ₁¹(FO²), that is, in (non-monadic) existential second-order logic with only two first-order variables, coincides with the regular languages. This provides an alternative logical description of regularity to both the traditional one in terms of monadic second-order logic, due to Buchi and Trakhtenbrot, and the more recent ones in terms of prefix fragments of Σ₁¹, due to Eiter, Gottlob and Gurevich. Our result extends to more general settings than words. Indeed, definability in Σ₁¹(FO²) coincides with recognizability by appropriate notions of automata on a large class of objects, including ω-words, trees, pictures and, more generally, all weakly deterministic, triangle-free transition systems