Decidable Characterization of FO2(<,+1) and locality of DA

TL;DR

This paper provides a new, simplified proof that determining whether a language is definable in FO2(<,+1) is decidable, and as a consequence, it establishes the locality of the variety DA.

Contribution

It introduces a self-contained, simplified proof of FO2(<,+1) definability decidability and derives the locality of DA as a corollary.

Findings

Decidability of FO2(<,+1) definability established.

Simplified proof method introduced.

Locality of DA proved as a corollary.

Abstract

Several years ago Th\'erien and Wilke exhibited a decidable characterization of the languages of words that are definable in FO2(<,+1). Their proof relies on three separate ingredients. The first one is the characterization of the languages that are definable in FO2(<) as those whose syntactic semigroup belongs to the variety DA. Then, this result is combined with a wreath product argument showing that being definable in FO2(<,+1) corresponds to having a syntactic semigroup in DA*D. Finally, proving that membership of a semigroup in DA*D is decidable requires a third ingredient: the "locality" of DA, a result proved by Almeida. In this note we present a new self-contained and simple proof that definability in FO2(<,+1) is decidable. We obtain the locality of DA as a corollary.