The Alternation Hierarchy of First-Order Logic on Words is Decidable

TL;DR

This paper proves the decidability of whether a regular language can be expressed in specific fragments of first-order logic, resolving a question open since 1971, and introduces polynomial closure as a key concept.

Contribution

It establishes the decidability of the alternation hierarchy levels for first-order logic on words and develops a framework based on polynomial closure for regular language classes.

Findings

Decidability of the $oldsymbol{ ext{FO}[<]}$ fragments for regular languages.

Polynomial closure preserves decidability of separation problems.

Algorithm complexity is exponential, with a conjecture for polynomial-time complexity.

Abstract

We show that for any $i > 0$, it is decidable, given a regular language, whether it is expressible in the $\Sigma_i[<]$ fragment of first-order logic FO[<]. This settles a question open since 1971. Our main technical result relies on the notion of polynomial closure of a class of languages $\mathcal{V}$, that is, finite unions of languages of the form $L_0a_1L_1\cdots a_nL_n$ where each $a_i$ is a letter and each $L_i$ a language of $\mathcal{V}$. We show that if a class $\mathcal{V}$ of regular languages with some closure properties (namely, a positive variety) has a decidable separation problem, then so does its polynomial closure Pol($\mathcal{V}$). The resulting algorithm for Pol($\mathcal{V}$) has time complexity that is exponential in the time complexity for $\mathcal{V}$ and we propose a natural conjecture that would lead to a polynomial time blowup instead. Corollaries include the decidability of half levels of the dot-depth hierarchy and the group-based concatenation hierarchy.