First-order separation over countable ordinals

TL;DR

This paper proves the decidability of first-order separation over countable ordinal words by extending algebraic structures and developing new concepts, building on prior work on finite and omega words.

Contribution

It introduces ordinal monoids with aperiodic merge and demonstrates the decidability of FO separation and related problems for countable ordinal words.

Findings

Decidability of first-order separation over countable ordinal words.

Development of ordinal monoids with aperiodic merge.

Computability of FO-pointlike sets and the covering problem.

Abstract

We show that the existence of a first-order formula separating two monadic second order formulas over countable ordinal words is decidable. This extends the work of Henckell and Almeida on finite words, and of Place and Zeitoun on $\omega$-words. For this, we develop the algebraic concept of monoid (resp. $\omega$-semigroup, resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp. $\omega$-semigroup, resp. ordinal monoid) that explicitly includes a new operation capturing the loss of precision induced by first-order indistinguishability. We also show the computability of FO-pointlike sets, and the decidability of the covering problem for first-order logic on countable ordinal words.