# An algebraic approach to MSO-definability on countable linear orderings

Olivier Carton, Thomas Colcombet, Gabriele Puppis

► To cite this version:

Olivier Carton, Thomas Colcombet, Gabriele Puppis. An algebraic approach to MSO-definability on countable linear orderings. The Journal of Symbolic Logic, 2018, 83 (3), pp.1147-1189. 10.1017/jsl.2018.7. hal-01470325v2

HAL Id: hal-01470325

https://hal.science/hal-01470325v2

Submitted on 29 May 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# An algebraic approach to
MSO-definability
on countable linear orderings

Olivier Carton

IRIF, Université Paris Diderot

Thomas Colcombet

CNRS – IRIF, Université Paris Diderot

Gabriele Puppis

CNRS – LaBRI, Université Bordeaux

## Abstract

We develop an algebraic notion of recognizability for languages of words indexed by countable linear orderings. We prove that this notion is effectively equivalent to definability in monadic second-order (MSO) logic. We also provide three logical applications. First, we establish the first known collapse result for the quantifier alternation of MSO logic over countable linear orderings. Second, we solve an open problem posed by Gurevich and Rabinovich, concerning the MSO-definability of sets of rational numbers using the reals in the background. Third, we establish the MSO-definability of the set of yields induced by an MSO-definable set of trees, confirming a conjecture posed by Bruyère, Carton, and Sénizergues.

## Contents

<table><tr><td>1</td><td>Introduction</td><td>2</td></tr><tr><td>2</td><td>Preliminaries</td><td>5</td></tr><tr><td>2.1</td><td>Linear orderings</td><td>5</td></tr><tr><td>2.2</td><td>Condensations</td><td>6</td></tr><tr><td>2.3</td><td>Words and languages</td><td>6</td></tr><tr><td>3</td><td>Algebras for countable words</td><td>7</td></tr><tr><td>3.1</td><td>Countable products</td><td>7</td></tr><tr><td>3.2</td><td>From countable products to algebras</td><td>8</td></tr><tr><td>3.3</td><td>From algebras to countable products</td><td>10</td></tr><tr><td>3.4</td><td>Existence of evaluation trees</td><td>14</td></tr><tr><td>3.5</td><td>Equivalence of evaluation trees</td><td>17</td></tr></table>
<table><tr><td>4</td><td>From monadic second-order logic to ⊗-algebras</td><td>25</td></tr><tr><td>5</td><td>From ⊗-algebras to monadic second-order logic</td><td>27</td></tr><tr><td>5.1</td><td>Ramseian splits</td><td>28</td></tr><tr><td>5.2</td><td>Inductive construction of formulas</td><td>28</td></tr><tr><td>6</td><td>Applications</td><td>33</td></tr><tr><td>6.1</td><td>Collapse of the quantifier hierarchy</td><td>34</td></tr><tr><td>6.2</td><td>Definability with the cuts at the background</td><td>35</td></tr><tr><td>6.3</td><td>Yields of tree languages</td><td>39</td></tr><tr><td>7</td><td>Conclusion</td><td>46</td></tr></table>

# 1 Introduction

The paper continues a long line of research aiming at understanding the notions of regularity for languages of infinite objects, e.g., infinite words and trees. The central objects in this paper are *words* indexed by countable linear orderings, i.e., total orders over finite or countable sets paired with functions mapping elements to letters in some finite alphabet. Accordingly, languages here are just sets of countable words. We use *monadic second-order (MSO) logic* as a formalism for describing such languages. In particular, an MSO formula may involve quantifications over positions of a word, as well as quantifications over sets of positions. A sentence naturally defines the language of all words that make the sentence true.

This paper provides a fine comprehension of the expressive power of MSO logic over countable linear orderings by proving a correspondence between definability in MSO and recognizability by suitable algebraic structures. More precisely, we introduce a generalization of the classical notion of finite monoid (i.e., a finite set equipped with an associative product), that we call $⊗$-monoid, and we extend accordingly the notion of recognizability by monoid morphism to capture a large class of languages of countable words. Differently from the classical setting, $⊗$-monoids are not finite objects, as the product mapping is defined over countable sequences of elements and a priori it is not clear how to represent this mapping by a finite table. To obtain finite presentations of the recognized languages, we follow an approach similar to [Wil93], namely, we associate with each $⊗$-monoid a finite number of operators with finite domain. We prove that, under natural conditions, the associated algebraic structure, called $⊗$-algebra, uniquely determines a $⊗$-monoid. The correspondence between $⊗$-monoids and $⊗$-algebras, together with the proposed notion of recognizability, gives a natural framework where languages of countable words can be represented and manipulated algorithmically. Our main contribution consists in proving that recognizability by $⊗$-monoids/algebras corresponds effectively to definability in MSO logic, exactly as it happens for regular languages of finite words and $ω$-words:

*The languages recognized by $⊗$-monoids are the same as the languages definable in MSO logic.*

Prior results (see related work below) also focused on MSO logic over countable linear orderings and similar correspondences with algebraic structures, but mostly
from the point of view of decidability of the logical theory. Our study gives a deeper
insight on the expressive power of MSO logic on these structures. For example, as
a by-product of our results we obtain that the quantifier hierarchy of MSO logic
collapses to its second level:

*Every language of countable words defined in MSO logic can be equally defined in the $∃∀$-fragment.*

The above result is reminiscent of the collapse of MSO to its existential frag-
ment when interpreted over $ω$, as shown by Büchi in [Bü62]. We also show that
our collapse result is optimal, in the sense that the first level of the quantifier
hierarchy does not capture the full expressive power of MSO logic on countable
linear orderings. This situation is also very similar to the setting of regular lan-
guages of infinite trees, where a collapse of MSO at the second level holds [Rab69].
Despite this similarity and the fact that recognizable languages of countable words
are MSO-interpretable from regular languages of infinite trees, our collapse result
does not follow immediately from Rabin’s result. Indeed, an MSO-interpretation
may exploit second-order quantifications to define linear orderings inside infinite
trees.

Our investigation on recognizability by $\ominus$-monoids provides also new insights
on the type of properties that can be expressed in MSO logic over *uncountable*
linear orderings. For example, we consider the following question that was raised
and left open by Gurevich and Rabinovich in [GR00]:

*Given a property for sets of rational numbers that is MSO-definable in the real line, is it possible to define it directly in the rational line? In other words, is it true that the presence of reals 'at the background' does not increase the expressive power of MSO logic?*

We answer positively the above question by building up on the correspondence
between MSO-definability and recognizability by $\ominus$-monoids. The latter expres-
siveness result is inherently non-effective since the MSO theory of the real line is
undecidable [She75], while that of the rational line is decidable.

Finally, we establish an interesting correspondence between MSO-definability
of languages of (possibly infinite) trees and MSO-definability of their yields:

*Define the yield of a tree as the set of leaves ordered by the infix relation.
Consider an MSO-definable tree language $L$ that is yield-invariant,
namely, such that for all trees $t, t'$ with the same yield, $t \in L$ iff $t' \in L$.
The set of yields of trees in $L$ is effectively MSO-definable.*

In [Tha67] a similar result was shown in the restricted setting of *finite trees*.

**Related work** Büchi initiated the study of MSO logic using the tools of language theory. He established that every language of $ω$-words (i.e., the particular case of words indexed by the ordinal $ω$) definable in MSO logic is effectively recognized by a suitable form of automaton [Bü62]. A major advance was obtained by Rabin, who
extended this result to infinite trees [Rab69]. One consequence of Rabin's result is that MSO logic is decidable over the class of all countable linear orderings. Indeed, every linear ordering can be seen as a set of nodes of the infinite tree, with the order corresponding to the infix ordering on nodes. Another proof of the decidability of the MSO theory of countable linear orderings has been given by Shelah using the composition method [She75]. This automaton-free approach to logic is based on syntactic operations on formulas and is inspired from Feferman and Vaught [FV59]. The same paper of Shelah is also important for another result it contains: the undecidability of the MSO theory of the real line (the reals with order). However, for infinite words as for infinite trees, the theory is much richer than simply the decidability of MSO logic. In particular, MSO logic is known to be equivalent to a number of different formalisms, such as automata, some forms of algebras, and, in the $ω$-word case, regular expressions. MSO logic is also known to collapse to its existential fragment when interpreted on the linear order $ω$, that is, every formula is equivalent to a formula consisting of a block of existential quantifiers followed by a first-order formula.

Another branch of research has been pursued to raise the equivalence between logic, automata, and algebra to infinite words beyond $ω$-words. In [Büc64], Büchi introduced $ω_1$-automata on transfinite words to prove the decidability of MSO logic for ordinals less than $ω_1$. Besides the usual transitions, $ω_1$-automata are equipped with limit transitions of the form $P \to q$, with $P$ set of states, which are used in a Muller-like way to process words indexed over ordinals. Büchi proved that these automata have the same expressive power as MSO logic over ordinals less than $ω_1$. The key ingredient is the closure under complementation of $ω_1$-automata. In [BC07], $ω_1$-automata have been extended to $\diamond$-automata by introducing limit transitions of the form $q \to P$ to process words over linear orderings. In [RC05], $\diamond$-automata are proven to be closed under complementation with respect to countable and scattered linear orderings (a linear ordering is scattered if it is nowhere dense, namely, if none of its suborders is isomorphic to the rational line). More precisely, $\diamond$-automata have the same expressive power as MSO logic over countable and scattered linear orderings [BBCR10]. However, it was already noticed in [BBCR10] that $\diamond$-automata are strictly weaker than MSO logic over countable (possibly non-scattered) linear orderings: indeed, the closure under complementation fails as there is an automaton that accepts all words with non-scattered domains, whereas there is none for scattered words.

Some of the results presented here appeared in preliminary form in the conference papers [CCP11] and [Col13].

**Structure of the paper** After the preliminaries in Section 2, we introduce in Section 3 the notions of $\otimes$-monoids and $\otimes$-algebras, and present the corresponding tools and results. In Section 4 we translate MSO formulas to $\otimes$-algebras and in Section 5 we establish the converse. In Section 6 we exploit the developed algebraic framework to solve three open problems that we discussed earlier, namely: (i) the collapse of the quantifier hierarchy of MSO logic, (ii) the correspondence between classical MSO-definability and definability with the reals 'at the background', and (iii) the MSO-definability of the set of yields induced by a regular yield-invariant
tree language.

**Acknowledgements** We are grateful to Achim Blumensath for his numerous comments on this work and to Alexander Rabinovich for the discussions on the subject and for introducing us to the question of definability with the reals at the background.

# 2 Preliminaries

In this section we recall some definitions for linear orderings, condensations, words, and languages.

## 2.1 Linear orderings

A *linear ordering* $\alpha = (X, <)$ is a set $X$ equipped with a total order $<$. By a slight abuse of terminology, we call a linear ordering *countable* when its domain is finite or countable. We write $\alpha^*$ to denote the reverse linear ordering $(X, >)$. Two linear orderings have same *order type* if there is an order-preserving bijection between their domains. We denote by $\omega, \omega^*, \zeta, \eta$ the order types of $(\mathbb{N}, <)$, $(-\mathbb{N}, <)$, $(\mathbb{Z}, <)$, $(\mathbb{Q}, <)$, respectively. Unless strictly necessary, we do not distinguish between a linear ordering and its order type.

Given a subset $I$ of a linear ordering $\alpha$, we denote by $\alpha|_I$ the *induced subordering*. Given two subsets $I, J$ of $\alpha$, we write $I < J$ iff $x < y$ for all $x \in I$ and all $y \in J$. A subset $I$ of $\alpha$ is said to be *convex* if for all $x, y \in I$ and all $z \in \alpha$, $x < z < y$ implies $z \in I$.

The *sum* $\alpha_1 + \alpha_2$ of two linear orderings $\alpha_1 = (X_1, <_1)$ and $\alpha_2 = (X_2, <_2)$ (up to renaming, assume that $X_1$ and $X_2$ are disjoint) is the linear ordering $(X_1 \uplus X_2, <)$, where $<$ coincides with $<_1$ on $X_1$, with $<_2$ on $X_2$, and, furthermore, it satisfies $X_1 < X_2$. More generally, given a linear ordering $\alpha = (X, <)$ and, for each $i \in X$, a linear ordering $\beta_i = (Y_i, <_i)$ (assume that the sets $Y_i$ are pairwise disjoint), we define the sum $\sum_{i \in \alpha} \beta_i$ to be the linear ordering $(Y, <')$, where $Y = \bigcup_{i \in X} Y_i$ and, for every $i, j \in X$, every $x \in Y_i$, and every $y \in Y_j$, $x' < y$ iff either $i = j$ and $x <_i y$ hold or $i < j$ holds.

A subset $I$ of a linear ordering $\alpha$ is *dense in* $\alpha$ if for every $x < y \in \alpha$, there exists $z \in I$ such that $x < z < y$. For example, $(\mathbb{Q}, <)$ is dense in $(\mathbb{R}, <)$ and $(\mathbb{R}, <)$ is dense in itself. If a linear ordering $\alpha$ is dense in itself, then we simply say that $\alpha$ is *dense*. A linear ordering $\alpha$ is *scattered* if all its dense suborderings are empty or singletons. For example, $(\mathbb{N}, <)$, $(\mathbb{Z}, <)$, and all the ordinals are scattered. Being scattered is preserved under taking a subordering. A scattered sum of scattered linear orderings also yields a scattered linear ordering.

Additional material on linear orderings can be found in [Ros82].
## 2.2 Condensations

A standard way to prove properties of linear orderings is to decompose them into basic objects (e.g., finite sequences, $\omega$-sequences, $\omega^*$-sequences, and $\eta$-orderings). This can be done by exploiting the notion of condensation.

Precisely, a condensation of a linear ordering $\alpha$ is an equivalence relation $\sim$ over $\alpha$ such that for all $x < y < z$, $x \sim z$ implies $x \sim y \sim z$. Equivalently, a condensation of $\alpha$ can be seen as a partition of $\alpha$ into convex subsets.

The order on $\alpha$ induces a corresponding order on the quotient $\alpha/\sim$, which is called the condensed ordering. This condensed ordering $\alpha/\sim$ inherits some properties from $\alpha$: if $\alpha$ is countable (resp., scattered), then $\alpha/\sim$ is countable (resp., scattered).

## 2.3 Words and languages

We use a generalized notion of word, which coincides with the notion of labelled linear ordering. Given a linear ordering $\alpha$ and a finite alphabet $A$, a word over $A$ with domain $\alpha$ is a mapping of the form $w : \alpha \to A$. The domain of a word $w$ is denoted $\text{dom}(w)$. Unless specifically required, we shall always consider words of countable domain, and up to isomorphism. The set of all words (of countable domain) over an alphabet $A$ is denoted $A^\omega$. The set of all words of non-empty (countable) domain over an alphabet $A$ is denoted $A^\oplus$. Given a word $w$ and a subset $I$ of $\text{dom}(w)$, we denote by $w|_I$ the subword resulting from restricting the domain of $w$ to $I$. If in addition $I$ is convex, then $w|_I$ is said to be a factor of $w$.

Certain words will play a crucial role in the sequel, so we introduce specific notation for them. For example, we denote the empty word by $\varepsilon$. A word $w$ is said to be an $\eta$-shuffle of set $A$ of letters if (i) the domain $\text{dom}(w)$ has order type $\eta$ and (ii) for every symbol $a \in A$, the set $w^{-1}(a) = \{x \in \text{dom}(w) | w(x) = a\}$ is dense in $\text{dom}(w)$. Recall that $\eta$ is – up to isomorphism – the unique countable dense linear ordering with no end-points. Likewise, for every finite set $A$, there is a unique, up to isomorphism, $\eta$-shuffle of $A$.

Given two words $u, v$, we denote by $uv$ the concatenation of $u$ and $v$, namely, the word with domain $\text{dom}(u) + \text{dom}(v)$, where each position $x \in \text{dom}(u)$ (resp., $x \in \text{dom}(v)$) is labelled by $u(x)$ (resp., $v(x)$). This is readily generalized to infinite concatenations of the form $\prod_{i \in \alpha} w_i$, for any linear ordering $\alpha$ and any sequences of words $(w_i)_{i \in \alpha}$, the resulting word having domain $\sum_{i \in \alpha} \text{dom}(w_i)$. The $\omega$-power of a word $w$ is defined as $w^\omega = \prod_{i \in \omega} w$. Similarly, we define the $\omega^*$-power $w^{\omega^*} = \prod_{i \in \omega^*} w$. By a slight abuse of terminology, we also define the $\eta$-shuffle of a tuple of words $w_1, \dots, w_k$ as the word

$$ \{w_1, \dots, w_k\}^{\eta} =^{\text{def}} \prod_{i \in \eta} w_{f(i)} $$

where $f$ is the unique $\eta$-shuffle of the set of letters $I = \{1, \dots, k\}$.

A $\oplus$-language (resp., $\oplus$-language) is any set of words (resp., non-empty words) over a fixed finite alphabet. The operations of concatenation, $\omega$-power, $\omega^*$-power, $\eta$-shuffle, etc. are extended to languages in the obvious way.
# 3 Algebras for countable words

In this section we present the algebraic objects that are suited for deriving a notion of recognizability for languages of countable words. As it was already the case for words with domain $\omega$, [PP04, Wil93], our definitions come in two flavors, $\oplus$-monoids (corresponding to $\omega$-monoids) and $\oplus$-algebras (corresponding to Wilke's algebras). We prove the equivalence of the two notions when the supports are finite.

## 3.1 Countable products

We introduce below a notion of product indexed by countable linear orderings that satisfies a generalized associativity property.

**Definition 1.** A (generalized) product over a set $S$ is a function $\pi$ from $S^{\oplus}$ to $S$ such that, for every $a \in S$, $\pi(a) = a$ and, for every family of words $(u_i)_{i \in \alpha} \in (S^{\oplus})^{\oplus}$,

$$ \pi(\prod_{i \in \alpha} \pi(u_i)) = \pi(\prod_{i \in \alpha} u_i). \qquad (\text{generalized associativity}) $$

The pair $(S, \pi)$ is called a $\oplus$-semigroup.

If the same definition holds, with $\pi$ function from $S^{\oplus}$ to $S$ and $(u_i)_{i \in \alpha} \in (S^{\oplus})^{\oplus}$, then $(S, \pi)$ is called a $\oplus$-monoid.

As an example, the function $\prod$ that maps any countable sequence of non-empty words to their concatenation is a generalized product over $A^{\oplus}$. Hence, $(A^{\oplus}, \prod)$ is a $\oplus$-semigroup; it is indeed the free $\oplus$-semigroup generated by $A$. Similarly, $(A^{\oplus}, \prod)$ is the free $\oplus$-monoid generated by $A$.

Given a $\oplus$-semigroup $(S, \pi)$, we call *neutral element* an element $1 \in S$ such that, for every word $w \in S^{\oplus}$, if $w|_{1} = 1$ is the subword of $w$ obtained by removing every occurrence of the element $1$ and $w|_{1} = 1$ is non-empty, then $\pi(w) = \pi(w|_{1})$. Note that the neutral element, if exists, is unique: given two neutral elements $1, 1' \in S$, we have $1 = \pi(1) = \pi(1'|_{1'}) = \pi(11') = \pi(11'|_{1}) = \pi(1') = 1'$.

At some places in the proofs it will be necessary to use $\oplus$-semigroups rather than $\oplus$-monoids. The two notions are however very close. On the one hand, any $\oplus$-monoid $(S, \pi)$ can be seen as a $\oplus$-semigroup by simply restricting its generalized product $\pi$ to $S^{\oplus}$. On the other hand, any $\oplus$-semigroup $(S, \pi)$ can be extended to a $\oplus$-monoid either by letting $\pi(\varepsilon) = 1$, where $\varepsilon$ is the empty word and $1$ is the (unique) neutral element of $(S, \pi)$, or, if $(S, \pi)$ has no neutral element, by introducing a fresh element $1' \notin S$ and by letting $\pi(\varepsilon) = 1$ and $\pi(w) = \pi(w|_{1'})$ for all words $w$ over $S \uplus \{1\}$.

A *morphism* from a $\oplus$-semigroup $(S, \pi)$ to another $\oplus$-semigroup $(S', \pi')$ is a mapping $h: S \to S'$ such that, for every word $(w_i)_{i \in \alpha} \in S^{\oplus}$,

$$ h(\pi(w)) = \pi'(\bar{h}(w)), $$

where $\bar{h}$ is the pointwise extension of $h$ to words. A *morphism of $\oplus$-monoids* is defined similarly, this time with $(w_i)_{i \in \alpha} \in S^{\oplus}$.
A $\oplus$-language $L \subseteq A^{\oplus}$ is *recognizable by a $\oplus$-semigroup* if there exists a morphism $h$ from $(A^{\oplus}, \Pi)$ to some finite $\oplus$-semigroup $(S, \pi)$ (here finite means that $S$ is finite) such that $L = h^{-1}(F)$ for some $F \subseteq S$ (equivalently, $h^{-1}(h(L)) = L$). Similarly, a $\oplus$-language $L \subseteq A^{\oplus}$ is *recognizable by a $\oplus$-monoid* if there exists a morphism $h$ from $(A^{\oplus}, \Pi)$ to some finite $\oplus$-monoid $(M, \pi)$ (here finite means that $M$ is finite) such that $L = h^{-1}(F)$ for some $F \subseteq M$ (equivalently, $h^{-1}(h(L)) = L$).

We are mainly interested in languages recognizable by finite $\oplus$-monoids. However, it is worth noticing that, with respect to membership of non-empty words, this notion is the same as recognizability by finite $\oplus$-semigroups: indeed, a language $L$ is recognizable by finite $\oplus$-monoids iff $L \setminus \{\varepsilon\}$ is recognizable by finite $\oplus$-semigroups.

## 3.2 From countable products to algebras

The notion of recognizability for $\oplus$-languages makes use of a product function $\pi$ that needs to be represented, a priori, by an infinite table. This is a not usable as it stands for finite presentations of languages, nor for decision procedures. That is why, given a finite $\oplus$-semigroup $(S, \pi)$, we define the following (finitely presentable) algebraic operators:

* the binary product $\cdot: S^2 \to S$, mapping any pair of elements $a, b \in S$ to the element $\pi(ab)$,

* the $\tau$-iteration $\tau: S \to S$, mapping any element $a \in S$ to the element $\pi(a^\omega)$ (thus, $\tau$ is the analogous of the $\omega$-power inside $S$),

* the $\tau^*$-iteration $\tau^*: S \to S$, mapping any element $a \in S$ to the element $\pi(a^{\omega^*})$ (thus, $\tau^*$ is the analogous of the $\omega^*$-power inside $S$),

* the $\kappa$-iteration $\kappa: \mathcal{P}(S) \setminus \{\emptyset\} \to S$, mapping any non-empty subset $\{a_1, \dots, a_k\}$ of $S$ to the element $\pi(\{a_1, \dots, a_k\}^\eta)$ ($\kappa$ is the analogous of the $\eta$-shuffle inside $S$).

Furthermore, if $(S, \pi)$ is a $\oplus$-monoid, we see the neutral element as a nullary operator induced by $\pi$, namely, as $1 = \pi(\varepsilon)$. One says that $\cdot, \tau, \tau^*, \kappa$ (and possibly 1) are *induced by* $\pi$. From now on, we shall use the operator $\cdot$ with infix notation (e.g., $a \cdot b$) and the operators $\tau, \tau^*, \kappa$, and $\kappa$ with superscript notation (e.g., $a^\tau, \{a_1, \dots, a_k\}^\kappa$). As shown below, the resulting structures $(S, \cdot, \tau, \tau^*, \kappa)$, $(S, 1, \cdot, \tau, \tau^*, \kappa)$ have the property of being, respectively, a $\oplus$-algebra and a $\oplus$-algebra.

**Definition 2.** A structure $(S, \cdot, \tau, \tau^*, \kappa)$, with $\cdot: S^2 \to S$, $\tau, \tau^*: S \to S$, and $\kappa: \mathcal{P}(S) \setminus \{\emptyset\} \to S$, is called a $\oplus$-algebra if:

(A1) $(S, \cdot)$ is a semigroup, namely, for every $a, b, c \in S$, $a \cdot (b \cdot c) = (a \cdot b) \cdot c$,

(A2) $\tau$ is compatible to the right, namely, for every $a, b \in S$ and every $n > 0$, $(a \cdot b)^n = a \cdot (b \cdot a)^n$ and $(a^n)^T = a^T$,
(A3) $\tau^*$ is compatible to the left, namely, for every $a, b \in S$ and every $n > 0$,
$(b \cdot a)^{\tau^*} = (a \cdot b)^{\tau^*} \cdot a$ and $(a^n)^{\tau^*} = a^{\tau^*}$,

(A4) $\kappa$ is compatible with shuffles, namely, for every non-empty subset $P$ of $S$, every element $c$ in $P$, every subset $P'$ of $P$, and every non-empty subset $P''$ of $\{P^\kappa, a \cdot P^\kappa, P^\kappa \cdot b, a \cdot P^\kappa \cdot b \mid a, b \in P\}$, we have

$$ 
\begin{align*}
P^{\kappa} &= P^{\kappa} \cdot P^{\kappa} = P^{\kappa} \cdot c \cdot P^{\kappa} \\
&= (P^{\kappa})^{\tau} = (P^{\kappa} \cdot c)^{\tau} \\
&= (P^{\kappa})^{\tau^{*}} = (c \cdot P^{\kappa})^{\tau^{*}} \\
&= (P' \cup P'')^{\kappa}.
\end{align*} 
$$

A $\oplus$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ is a $\oplus$-algebra $(M, \cdot, \tau, \tau^*, \kappa)$ with a distinguished element $1 \in M$ such that

(A5) $x \cdot 1 = 1 \cdot x = x$, $1^{\tau} = 1^{\tau^*} = \{1\}^{\kappa} = 1$, and $P^{\kappa} = (P \cup \{1\})^{\kappa}$, for all $x \in M$ and all non-empty $P \subseteq M$.

The typical $\oplus$-algebras and $\otimes$-algebras are:

**Lemma 3.** For every alphabet $A$, $(A^{\oplus}, \cdot, \omega, \omega^*, \eta)$ is a $\oplus$-algebra and $(A^{\otimes}, \cdot, \omega, \omega^*, \eta)$ is a $\otimes$-algebra<fnref n="1" />.

*Proof.* By a systematic analysis of Axioms A1-A5. □

<figure><img src="image_2.png" /></figure>

Furthermore, as we mentioned above, every $\oplus$-semigroup induces a $\oplus$-algebra and every $\otimes$-monoid induces a $\otimes$-algebra:

**Lemma 4.** For every $\oplus$-semigroup $(S, \pi)$, $(S, \cdot, \tau, \tau^*, \kappa)$ is a $\oplus$-algebra, where the operators $\cdot, \tau, \tau^*$, and $\kappa$ are those induced by $\pi$. Similarly every $\otimes$-monoid $(S, \pi)$, $(S, 1, \cdot, \tau, \tau^*, \kappa)$ is a $\otimes$-algebra, where the operators $\cdot, \tau, \tau^*$, $\kappa$, and $1$ are those induced by $\pi$.

*Proof.* The results are simply inherited from Lemma 3 by morphism. Let $(S, \pi)$ be a $\oplus$-semigroup inducing the operators $\cdot, \tau, \tau^*, \kappa$. The structure $(S^{\oplus}, \Pi)$ is also a $\oplus$-semigroup, which induces the operations of concatenation, $\omega$-power, $\omega^*$-power, and $\eta$-shuffle. Furthermore, the product $\pi$ can be seen as a surjective morphism from $(S^{\oplus}, \Pi)$ to $(S, \pi)$ (just a morphism of abstract algebras, not of $\oplus$-algebras). By definition of $\cdot, \tau, \tau^*, \kappa$, this morphism maps concatenation to $\cdot$, $\omega$-power to $\tau$-iteration, $\omega^*$-power to $\tau^*$-iteration, and $\eta$-shuffle to $\kappa$-iteration. It follows that any equality involving concatenation, $\omega$-power, $\omega^*$-power, and $\eta$-shuffle is also satisfied by the analogous operations $\cdot, \tau, \tau^*$, and $\kappa$. In particular, the axioms that, thanks to Lemma 3, are satisfied by the $\oplus$-algebra $(S^{\oplus}, \cdot, \omega, \omega^*, \eta)$ are directly transferred to $(S, \cdot, \tau, \tau^*, \kappa)$. The case of a $\otimes$-monoid is similar. □

<figure><img src="image_3.png" /></figure>

<footnote n="1">¹Similarly to what happens for Wilke's algebras [Wil93], $(A^{\oplus}, \cdot, \omega, \omega^*, \eta)$ is not the free $\oplus$-algebra generated by $A$, as the free algebra generated by a finite set is by definition countable, while $A^{\otimes}$ has the cardinality of the continuum.</footnote>
### 3.3 From algebras to countable products

Here, we aim at proving a converse to Lemma 4, namely, that every finite $\oplus$-algebra $(S, \cdot, \tau, \tau^*, \kappa)$ can be uniquely extended to a $\oplus$-semigroup $(S, \pi)$, and similarly for $\ominus$-algebras and $\ominus$-monoids (Theorem 11 and Corollary 12).

Let us fix a finite $\oplus$-algebra $(S, \cdot, \tau, \tau^*, \kappa)$. In this section, we assume that all words are over the alphabet $S$. The objective of the construction is to attach to each word $u$ (over the alphabet $S$) a ‘value’ in $S$. Furthermore, this value needs to be shown unique.

The key ingredient for associating a unique value in $S$ to each word $u \in S^{\oplus}$ is the notion of *evaluation tree*. Intuitively, this is an infinite tree describing a strategy for evaluating larger and larger factors of the word $u$. To define these objects, we need to first introduce the concept of *condensation tree*, which is a convenient representation of nested condensations of a linear ordering. This will provide the underlying structure of an evaluation tree. The nodes of a condensation tree are convex subsets of the linear ordering and the descendant relation is given by inclusion. The set of children of each node defines a condensation. Furthermore, in order to provide an induction parameter, we require that the branches of a condensation tree are finite (but their length may not be uniformly bounded).

**Definition 5.** A condensation tree over a linear ordering $\alpha$ is a set $T$ of non-empty convex subsets of $\alpha$ such that:

* $\alpha \in T$,

* for all $I, J$ in $T$, either $I \subseteq J$ or $J \subseteq I$ or $I \cap J = \emptyset$,

* for all $I \in T$, the union of all $J \in T$ such that $J \not\subseteq I$ is either $I$ or $\emptyset$,

* every subset of $T$ totally ordered by inclusion is finite.

Elements in $T$ are called *nodes*. The node $\alpha$ is called the *root* of the tree. Nodes minimal for $\subseteq$ are called *leaves*; the other nodes, including the root, are called *internal nodes*. A node $I \in T$ is a *descendant* of a node $J \in T$ (and accordingly $J$ is an *ancestor* of $I$) if $I \subseteq J$. If in addition we have $I \neq J$, then we say that $I$ is a *proper descendant* of $J$. Similarly, $I$ is a *child* of a node $J$ (and accordingly $J$ is the *parent* of $I$) if $I \not\subseteq J$ and, for all $K \in T$, $I \not\subseteq K$ implies $J \subseteq K$. According to the definition, if $I$ is an internal node of a condensation tree $T$ over $\alpha$, then it has a set of children that forms a partition of $I$ into convex subsets. We denote this partition by $\text{children}_T(I)$, and we observe that it naturally corresponds to a condensation of $\alpha|_I$. When the tree $T$ is clear from the context, we will denote by $\text{children}(I)$ the set of all children of $I$ in $T$ and, by extension, the corresponding condensation and the corresponding condensed ordering. Finally, we define the *subtree* of $T$ rooted at some of node $I$ of it as the condensation tree obtained by restricting $T$ to the descendants of $I$ (including $I$ itself).

We now introduce evaluation trees. Intuitively, these are condensation trees where each internal node has an associated value in $S$ that can be ‘easily computed’ from the values of its children. Here it comes natural to consider a word $u$ ‘easy
to compute' if it is isomorphic to either $ab, a^\omega, a^{\omega*}$, or $P^\eta$, for some elements $a, b \in S$ and some non-empty set $P \subseteq S$. Indeed, in each of these cases, the value of $u$ can be computed by a single application of the operations of the $\oplus$-algebra $(S, \cdot, \tau, \tau^*, \kappa)$. Formally, the words that are easily computable are precisely those that belong to the domain of the partial function $\pi_0$, defined just below:

**Definition 6.** Let $\pi_0$ be the partial function from $S^{\oplus}$ to $S$ such that:

* $\pi_0(ab) = a \cdot b$ for all $a, b \in S$,

* $\pi_0(e^\omega) = e^T$ for all idempotents $e \in S$ (i.e., all $e \in S$ such that $e \cdot e = e$),

* $\pi_0(e^{\omega*}) = e^{\tau*}$ for all idempotents $e \in S$,

* $\pi_0(P^\eta) = P^\kappa$ for all non-empty sets $P \subseteq S$,

* in all remaining cases, $\pi_0$ is undefined.

**Definition 7.** An evaluation tree over a word $u$ is a pair $\mathcal{T} = (T, \gamma)$, where $T$ is a condensation tree over the domain of $u$ and $\gamma$ is a function from $T$ to $S$ such that:

* every leaf of $T$ is a singleton of the form $\{x\}$ and $\gamma(\{x\}) = u(x)$,

* for every internal node $I$ of $T$, the partial function $\pi_0$ is defined on the word $\gamma(\text{children}(I))$ that has domain $\text{children}(I)$ and labels each position $J \in \text{children}(I)$ with $\gamma(J)$; in addition, we have $\gamma(I) = \pi_0(\gamma(\text{children}(I)))$.

The value of $(T, \gamma)$ is defined to be $\gamma(\alpha)$, i.e., the value of the root.

Let us turn back to the problem of associating a unique value in $S$ to each word $u \in S^{\oplus}$. Based on the previous definitions, we can solve this problem in two steps. First, we show that every word $u$ has an evaluation tree, and thus a possible value that can be associated with it. Then, we show that the associated value in fact does not depend on the choice of the evaluation tree over $u$, namely, that evaluation trees over the same word induce the same value. The next two propositions formalize precisely these two steps.

**Proposition 8.** For every word $u$, there exists an evaluation tree over $u$.

**Proposition 9.** Evaluation trees over the same word have the same value.

The proofs of the two propositions are quite technical and deferred to Sections 3.4 and 3.5, respectively. Before seeing those proofs in detail, we discuss the basic ingredients here. We then conclude the section by mentioning a few important consequences of the developed framework.

The proof of Proposition 8 resembles the construction used by Shelah in his proof of decidability of the monadic second-order theory of countable linear orderings [She75]. In particular, it uses a theorem of Ramsey [Ram29] and a lemma stating that every non-trivial word indexed by a countable dense linear ordering has an $\eta$-shuffle as a factor. Note that this latter lemma, and hence also Proposition 8, relies on the fact that the domain of the word is countable. The
proof of the proposition also makes use of Zorn's Lemma (or equally, the Axiom of Choice), so it is a proof in ZFC. On the other hand, we observe that it does not make any use of Axioms A1-A4.

Proposition 9 can be regarded as the core contribution of the paper, and its proof technique is quite original. For example, as opposed to Proposition 8, one cannot find any ingredient of the proof of Proposition 9 in [She75]. The proof heavily relies on the use of Axioms A1-A4. As a matter of fact, each axiom can be seen as an instance of Proposition 9 in some special cases of evaluation trees of small height. The proof also depends on Proposition 8, in the sense that it exploits in several places the existence of evaluation trees over arbitrary (countable) words.

Another key ingredient for the proof of Proposition 9, which is also reused in other proofs, is the formalization of a suitable induction principle on condensation and evaluation trees. More precisely, by exploiting the fact that all branches of a condensation tree are finite, one can associate with any condensation tree $T$ a countable ordinal rank($T$), called the rank of $T$. Intuitively, this is the smallest ordinal $\beta$ that enables a labelling of the nodes of $T$ by ordinals less than or equal to $\beta$ in such a way that the label of each node is strictly greater than the labels of its children.

**Lemma 10.** It is possible to associate with each condensation tree $T$ a countable ordinal rank($T$) in such a way that rank($T'$) < rank($T$) for all subtrees $T'$ of $T$ rooted at proper descendants of the root.

*Proof.* We associate with each node $I \in T$ a countable ordinal $\beta_I$ as follows. For every leaf $I$ of $T$, let $\beta_I = 0$. Then, given an internal node $I$ of $T$, we assume that $\beta_J$ is defined for every child $J$ of $I$, and we define $\beta_I$ as the ordinal $\sup\{\beta_J + 1 \mid J \in \text{children}(I)\}$ (note that this is either a successor ordinal or a limit ordinal, depending on whether the set $\{\beta_J + 1 \mid J \in \text{children}(I)\}$ has a maximum element or not). Since $T$ has no infinite branch, it follows that $\beta_I$ is defined for every node of $T$. We thus let $\text{rank}(T) = \beta_I$, where $I$ is the root of $T$. By construction, the function rank that maps any condensation tree $T$ to its rank $\text{rank}(T)$ satisfies the properties stated in the lemma. $\square$

Now, assuming that Propositions 8 and 9 hold, we can prove the desired correspondence between $\oplus$-semigroups and $\oplus$-algebras:

**Theorem 11.** Every finite $\oplus$-algebra $(S, \cdot, \tau, \tau^*, \kappa)$ is induced by a unique product $\pi$ from $S^\oplus$ to $S$.

*Proof.* Given a word $w$ with domain $\alpha$, one defines $\pi(w)$ to be the value of some evaluation tree over $w$ (the evaluation tree exists by Proposition 8 and the value $\pi(w)$ is unique by Proposition 9).

We prove that $\pi$ satisfies the generalized associativity property. Let $\sim$ be a condensation of the domain $\alpha$. For all classes $I \in \alpha/\sim$, let $\mathcal{T}_I$ be some evaluation tree over $w|_I$. Let also $\mathcal{T}'$ be some evaluation tree over the word $w' = \coprod_{I \in \alpha/\sim} \pi(w|_I)$. One constructs an evaluation tree $\mathcal{T}$ over $w$ by first lifting $\mathcal{T}'$ from the linear ordering $\alpha/\sim$ to $\alpha$ (this is done by replacing each node $J$ in
$\mathcal{T}'$ by $\cup J$) and then substituting each leaf of $\mathcal{T}'$ corresponding to some class $I \in \alpha/\sim$ with the evaluation tree $\mathcal{T}_I$. The last step is possible (namely, respects the definition of evaluation tree) because the value of each evaluation tree $\mathcal{T}_I$ is $\pi(w|_I)$, which coincides with the value $w'(I)$ at the leaf $I$ of $\mathcal{T}'$. By Proposition 9, the resulting evaluation tree $\mathcal{T}$ has the same value as $\mathcal{T}'$ and this proves that $\pi(w) = \pi(\prod_{I \in \alpha/\sim} \pi(w|_I))$.

It remains to prove that the above choice of $\pi$ indeed induces the operators $\cdot, \tau, \tau^*, \kappa$. This is done by a straightforward case analysis. $\square$

The result that we just proved immediately implies an analogous correspondence between $\otimes$-monoids and $\otimes$-algebras:

**Corollary 12.** Every finite $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ is induced by a unique product $\pi$ from $M^{\otimes}$ to $M$.

Finally, we discuss the algorithmic implications of the above results. In the same way as we talked of languages recognized by finite $\otimes$-monoids, we can equally talk of languages recognized by finite $\otimes$-algebras. Moreover, because finite $\otimes$-algebras are finite objects, this enables the possibility of manipulating and reasoning on recognized languages by means of algorithms. An example of such a possibility is given just below, in a theorem that shows the decidability of the emptiness problem for languages recognized by finite $\otimes$-algebras. The theorem also gives effective witnesses of non-empty languages, in the same spirit as some results of Laüchli and Leonard for models of first-order logic and weak monadic second-order logic [LJ66, LJ68]. Other examples of algorithmic manipulation of languages can be found in Section 4, where we will prove some closure properties of languages recognized by finite $\otimes$-algebras.

**Theorem 13.** The problem of testing whether $L \neq \emptyset$ for any language $L \subseteq A^{\otimes}$ recognized by a given finite $\otimes$-algebra is decidable. Moreover, if $L \neq \emptyset$, then a finite expression can be effectively constructed that represents some word in $L$ and is generated by the following grammar:

$$ w ::= \varepsilon \mid a \mid w \cdot w \mid w^{\omega} \mid w^{\omega*} \mid \{w, \dots, w\}^{\eta} \quad \text{for } a \in A. $$

*Proof.* Recall that a language $L \subseteq A^{\otimes}$ is recognized by a $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ if there is $F \subseteq M$ and a morphism $h : (A^{\otimes}, \Pi) \to (M, \pi)$ such that $L = h^{-1}(F)$, where $(M, \pi)$ is the $\otimes$-monoid induced by $(M, 1, \cdot, \tau, \tau^*, \kappa)$ (Corollary 12). To decide the emptiness problem, it is sufficient to describe an algorithm that, given $(M, 1, \cdot, \tau, \tau^*, \kappa)$ and $h : A \to M$ (which uniquely extends to a function from $(A^{\otimes}, \Pi)$ to $(M, \pi)$), computes the set

$$ h(A^{\otimes}) = \{1\} \cup \{h(u) \mid u \in A^{\otimes}\} $$

(note that $L = h^{-1}(F) \neq \emptyset$ iff $h(A^{\otimes}) \cap F \neq \emptyset$).

To compute the set $h(A^{\otimes})$, one can simply saturate the subset $\{1\} \cup h(A)$ of $M$ under the operations $\cdot, \tau, \tau^*, \kappa$. Formally, given $S \subseteq M$, we define the set generated by $S$ in $(M, 1, \cdot, \tau, \tau^*, \kappa)$ as the least set $\langle S \rangle$ that contains $S$ and satisfies the following closure properties:
* if $a, b \in \langle S \rangle$, then $a \cdot b \in \langle S \rangle$,

* if $a \in \langle S \rangle$, then $a^\tau \in \langle S \rangle$,

* if $a \in \langle S \rangle$, then $a^{\tau^*} \in \langle S \rangle$,

* if $\emptyset \neq P \subseteq \langle S \rangle$, then $P^\kappa \in \langle S \rangle$.

Clearly, the set $\langle S \rangle$ can be easily computed from $S$.

Below we prove that the set generated by $\{1\} \cup h(A)$, denoted $\langle\{1\} \cup h(A)\rangle$, coincide with $h(A^{\otimes})$. First, it is easy to see that $\langle\{1\} \cup h(A)\rangle \subseteq h(A^{\otimes})$, since $\{1\} \cup h(A) \subseteq h(A^{\otimes})$ and containments in $h(A^{\otimes})$ are preserved under all operations of the saturation. The opposite containment $h(A^{\otimes}) \subseteq \langle\{1\} \cup h(A)\rangle$ follows by Proposition 8 and some inductive argument. More precisely, one first observes that the value $h(w)$ of any word $w \in A^{\otimes}$ is the same as witnessed by some evaluation tree $T_w$. Then, one exploits a simple induction on $T_w$ – in fact, on the rank of the underlying condensation tree – to verify that the set $\langle\{1\} \cup h(A)\rangle$ contains the value of $T_w$.

The above arguments show that the set $h(A^{\otimes}) = \langle\{1\} \cup h(A)\rangle$ can be effectively constructed by a saturation procedure. To conclude, we observe that this procedure implicitly associates with each element of $\langle\{1\} \cup h(A)\rangle$ a corresponding finite expression, as generated by the grammar of the claim. $\square$

## 3.4 Existence of evaluation trees

We introduce a few additional ingredients for the proof of Proposition 8, namely, for showing the existence of evaluation trees over any word. We begin with a variant of Ramsey's theorem for additive labellings. Recall that $(S, \cdot, \tau, \tau^*, \kappa)$ is a finite $\oplus$-algebra and, in particular, $(S, \cdot)$ is a finite semigroup.

**Definition 14.** Let $(S, \cdot)$ be a semigroup. An additive labelling is a function $f$ that maps any two of points $x < y$ in a linear ordering $\alpha$ to an element $f(x, y)$ in $S$ in such a way that, for all $x < y < z$, $f(x, y) \cdot f(y, z) = f(x, z)$.

**Lemma 15 (Ramsey [Ram29]).** Given a linear ordering $\alpha$ with a minimum element $\perp$ and no maximum element, and given an additive labelling $f : \alpha \times \alpha \to (S, \cdot)$, there exist an $\omega$-sequence $\perp < x_1 < x_2 < \dots$ of points in $\alpha$ and two elements $a, e \in S$ such that:

* for all $y \in \alpha$, there is $x_i > y$,

* for all $i > 0$, $f(\perp, x_i) = a$,

* for all $j > i > 0$, $f(x_i, x_j) = e$.

Note that the conditions in the above lemma imply that $e$ is an idempotent: indeed, we have $e \cdot e = f(x_i, x_{i+1}) \cdot f(x_{i+1}, x_{i+2}) = f(x_i, x_{i+2}) = e$.

In the same spirit of Lemma 15, the following lemma shows that every countable dense word contains an $\eta$-shuffle as a factor. Even though this result appears already in [She75], we give a proof of it for the sake of self-containment.
**Lemma 16** (Shelah [She75]). Every word indexed by a non-empty non-singleton countable dense linear ordering contains a factor that is an $\eta$-shuffle.

*Proof.* Let $\alpha$ be a non-empty non-singleton countable dense linear ordering, let $A = \{a_1, \dots, a_n\}$ be a generic alphabet, and let $w$ be a word over $A$ with domain $\alpha$. For the sake of brevity, given a symbol $a \in A$, we denote by $w^{-1}(a)$ the set of all points $x \in \alpha$ such that $w(x) = a$. We then define $w_0 = w$ and $A_0 = \emptyset$, and we recursively apply the following construction for each index $1 \le i \le n$:

$$ 
\begin{align*}
A_i &= \begin{cases} A_{i-1} \cup \{a_i\} & \text{if } w_i^{-1}(a_i) \text{ is dense in } \operatorname{dom}(w_i), \\ A_{i-1} & \text{otherwise,} \end{cases} \\
w_i &= \begin{cases} w_{i-1} & \text{if } w_i^{-1}(a_i) \text{ is dense in } \operatorname{dom}(w_i), \\ w_{i-1}|_I & \text{otherwise, where } I \text{ is any open non-empty convex subset of } \alpha \text{ such that } w^{-1}(a_i) \cap I = \emptyset. \end{cases}
\end{align*}
$$

By construction, the domain of the factor $w_n$ is non-empty, non-singleton, countable, and dense. Moreover, for all symbols $a \in A$, either $w_n^{-1}(a_j)$ is dense in $\operatorname{dom}(w_n)$ or empty, depending on whether $a \in A_n$ or not. This shows that $w_n$ is an $\eta$-shuffle of the set $A_n$. $\square$

We are now ready to prove Proposition 8:

*Proof of Proposition 8.* Let $u$ be a word with countable domain $\alpha$. We say that a convex subset $I$ of $\alpha$ is *definable* if there is an evaluation tree over the factor $u|_I$. Similarly, we say that $I$ is *strongly definable* if every non-empty convex subset $J$ of $I$ is definable. We first establish the following claim:

**Claim 1.** For every ascending chain $I_0 \subseteq I_1 \subseteq \dots$ of strongly definable convex subsets of $\alpha$, the limit $I = \bigcup_{i \in \mathbb{N}} I_i$ is strongly definable.

*Proof of claim.* Let $J$ be a non-empty convex subset of $I$ and let $J_i = I_i \cap J$ for all $i \in \mathbb{N}$. We prove that $J = \bigcup_{i \in \mathbb{N}} J_i$ is definable, namely, we show how to construct an evaluation tree over the factor $u|_J$. Without loss of generality we assume that the $J_i$'s are non-empty. Note that all the $J_i$'s are strongly definable. Of course, if the sequence of the $J_i$'s is ultimately constant, then $J = J_i$ for a sufficiently large $i \in \mathbb{N}$ and the existence of an evaluation tree over $u|_J$ follows trivially from the fact that $J_i$ is strongly definable. We now consider the case when all the $J_i$'s coincide on the left. We can partition $J$ into a sequence of convex subsets $K_0 < K_1 < \dots$, where $K_0 = J_0$ and $K_{i+1} = J_{i+1} \setminus J_i$ for all $i \ge 1$. The convex subsets $K_i$ form a condensation of $J$ such that $J_i = K_0 \cup \dots \cup K_i$ for all $i \in \mathbb{N}$. For every $i < j$ in $\mathbb{N}$, we define $K_{i,j} = K_i \cup \dots \cup K_{j-1}$. We recall that every convex $J_j$, as well as every convex subset $K_{i,j}$ of it, is strongly definable. We can thus associate with each $K_{i,j}$ an evaluation tree $\mathcal{T}_{i,j}$ over $u|_{K_{i,j}}$. We denote by $c_{i,j}$ the value of $\mathcal{T}_{i,j}$. Using Lemma 15 (i.e., Ramsey's Theorem), one can extract a sequence $0 < i_1 < i_2 < \dots$ in $\omega$ such that $c_{i_1,i_2} = c_{i_2,i_3} = \dots$ (and moreover, this element is an idempotent). We can then construct an evaluation tree over $u|_J$ that has root $J$ and the convex
subsets $K_{0,i_1}$, $K_{i_1,i_2}$, ... for children, with the associated evaluation subtrees $\mathcal{T}_{0,i_1}$,
$\mathcal{T}_{i_1,i_2}$, ... This allows us to conclude that $J$ is a definable convex when the $J_i$'s
coincide on the left. The case where the $J_i$'s coincide on the right is symmetric.
Finally, in the general case, we can partition each set $J_i$ into two subsets $J_i'$ and $J_i''$
such that (i) $J_i' < J_i''$, (ii) the sequence of the $J_i'$s coincide on the right, and (iii)
the sequence of the $J_i''$s coincide on the left. Let $J' = \bigcup_{i \in \mathbb{N}} J_i'$ and $J'' = \bigcup_{i \in \mathbb{N}} J_i''$.
One knows by the cases above that there exist evaluation trees over $u|_{J'}$ and over
$u|_{J''}$. Finally, one can easily construct an evaluation tree over $u|_J = u|_{J' \cup J''}$ out of
the evaluation trees for $J'$ and $J''$. This proves that $J$ is definable and hence $I$ is
strongly definable.
□

Turning back to the main proof, let us now consider the set $\mathcal{C}$ of all
condensations $\mathcal{C}$ of $\alpha$ such that every class is strongly definable. Condensations in
$\mathcal{C}$ are naturally ordered by the 'finer than' relation. Let us consider a chain $(C_i)_{i \in \beta}$
of condensations in $\mathcal{C}$ ordered by the finer than relation, i.e., for all $j < i$ in $\beta$,
$C_j$ is finer than $C_j$. Since $\alpha$ is countable, one can assume that $\beta$ is countable, or
even better that $\beta = \omega$. Let us consider the *limit condensation* $\mathcal{C}$, i.e., the finest
condensation that is coarser than every $C_i$. Each class $I \in \mathcal{C}$ is the union of a
sequence of convex subsets $I_i$, with $I_i \in C_i$ for all $i \in \mathbb{N}$. From the assumption that
every condensation $C_i$ belongs to $\mathcal{C}$, we get that $I_i$ is strongly definable and from
the claim above, we conclude that $I$ is strongly definable as well. This shows that
the limit condensation $\mathcal{C}$ belongs to $\mathcal{C}$ and hence every chain of $\mathcal{C}$ has an upper
bound in $\mathcal{C}$.

It follows that we can apply Zorn's Lemma and deduce that $\mathcal{C}$ contains a maximal element, say $\mathcal{C}$. If $\mathcal{C}$ is a condensation with single class, this means that there exists an evaluation tree over $u$ and the proposition is established. Otherwise, we shall head toward a contradiction. Consider the condensed ordering induced by $\mathcal{C}$ (by a slight abuse of notation, we denote it also by $\mathcal{C}$). Two cases can happen: either $\mathcal{C}$ contains two consecutive classes or $\mathcal{C}$ is a dense linear order.

In the former case, we fix two consecutive classes $I, I' \in \mathcal{C}$, with $I < I'$. We
observe that each class of $\mathcal{C}$ is a limit of strongly definable convexes and hence,
by the previous claim, it is also strongly definable. It is then easy to see that
the union $I \cup I'$ of the two consecutive strongly definable convexes $I$ and $I'$ is also
strongly definable, which contradicts the definition of $\mathcal{C}$.

In the second case we have that the linear ordering $\mathcal{C}$ is dense in itself. As be-
fore, we recall that each class of $\mathcal{C}$ is strongly definable and we prove that there exist
non-trivial unions of classes of $\mathcal{C}$ that are strongly definable (a contradiction). We
begin by associating with each convex subset $J$ of a class $I$ of $\mathcal{C}$ an evaluation tree
$\mathcal{T}_J$ over $u|_J$ and we denote by $c_J$ the value induced by it. We then consider the
word $v = \bigcap_{I \in \mathcal{C}} c_I$. We know from Lemma 16 that that $v$ contains a factor that is an
$\eta$-shuffle, say, $v' = v|_{C'}$ for some convex $C' \subseteq \mathcal{C}$. Let $J = \bigcup_{I \in \mathcal{C}'} I$. To prove that $J$ is
strongly definable we consider a convex $K \subseteq J$ and we construct an evaluation tree
$\mathcal{T}_K$ over $u|_K$ as follows. First we observe that $K$ is the union of all non-empty
convexes of the form $I \cap K$, for $I \in \mathcal{C}'$, and that each set $I \cap K$ is contained in a
class of $\mathcal{C}$, hence it is definable and has value $c_{I \cap K}$. Now, one needs to distinguish
some cases depending on whether $\mathcal{C}'$ contains minimal/maximal convexes $I$ inter-
secting $K$. For the sake of simplicity, we only consider the case where $C'$ contains
a minimal convex $I_0$ such that $I_0 \cap K \neq \emptyset$, but no maximal convex $I$ such that
$I \cap K \neq \emptyset$. In this case, we recall that $v'$ is an $\eta$-shuffle and that its restriction to
the non-empty convexes $I \cap K$, with $I \in C'$, is the juxtaposition of the singleton
$c_{I_0 \cap K}$ and the $\eta$-shuffle $\prod_{I \in C''} (c_{I \cap K})$, where $C'' = \{I \in C' \mid I \cap K \neq \emptyset, I \neq I_0\}$. An
evaluation tree $\mathcal{T}_K$ over $u|_K$ can be constructed by appending to the root $K$ two
subtrees: the evaluation tree $\mathcal{T}_{I_0 \cap K}$ associated with the definable convex $I_0 \cap K$,
and the evaluation tree $\mathcal{T}_{K \setminus I_0}$ that consists of the node $K \setminus I_0$ and the direct sub-
trees $\mathcal{T}_{I \cap K}$, for all $I \in C''$. This shows that there is a non-trivial union $J$ of classes
of $C$ that is strongly definable, which contradicts the definition of $C$. $\square$

3.5 Equivalence of evaluation trees

We now turn towards proving Proposition 9, namely, the equivalence of
evaluation trees with respect to the induced values. As we already mentioned,
the proof is rather long and requires a series of technical lemmas.

For reasons that will be clear in the sequel, it is convenient to extend slightly the
domain of the partial function $\pi_0$ that computes values of ‘simple words’ (cf. Defi-
nition 6). Intuitively, such an extension adds prefixes and suffixes of finite length
to the elements of the original domain of $\pi_0$.

**Definition 6bis.** We extend the partial function $\pi_0$ in such a way that:

$\pi_0(a_1 \dots a_n) = a_1 \dots a_n \text{ for all } n \ge 1 \text{ and all } a_1, \dots, a_n \in S,$

$\pi_0(a b^{\omega}) = a \cdot b^{\tau}$ for all $a, b \in S,$

$\pi_0(a \omega^* b) = a^\tau \cdot b \text{ for all } a, b \in S,$

$\pi_0(a P^\eta b) = a \cdot P^\kappa b \text{ for all } a, b \in S \cup \{\epsilon\}$
(by a slight abuse of notation, we let $\epsilon \cdot s = s \cdot \epsilon = s$ for all $s \in S$),

* in all remaining cases, $\pi_0$ remains undefined.

The new definition of $\pi_0$ results in a more general notion of evaluation tree. Note
that the definition of rank of an evaluation tree still applies to this generalized
notion, since the rank was in fact defined on condensation trees independently of
$\pi_0$. The generalized notion of evaluation tree, together with the associated rank,
will give a strong enough invariant for having a proof by induction of the equivalence
of evaluation trees.<fnref n="2" />

The lemma below basically shows that if the (extended) partial mapping $\pi_0$ is
defined over a word, then it is also defined over all its factors. It is convenient here

<footnote n="2">²The extended definition of $\pi_0$ could have been introduced straight at the beginning, in place of Definition 6. Of course, all the results in the paper would still hold, but some proofs would become slightly more involved (in particular, those that show the correspondence between recognizability and MSO definability). This explains why we prefer to adopt a more restrictive definition of evaluation tree, and use the extended version only here for convenient.</footnote>
to allow also some change of letters at the extremities of the word and make some case distinctions for dealing with the empty word $\varepsilon$. This makes the statement of the following lemma a bit more technical.

**Lemma 17.** If $\pi_0$ is defined over a non-empty word of the form $u c v$, with $u, v \in S^{\oplus} \uplus \{\varepsilon\}$ and $c \in S \uplus \{\varepsilon\}$, then it is also defined over the words $u a$ and $b v$, for all $a, b \in S \uplus \{\varepsilon\}$ such that $a = b = \varepsilon$ implies $c = \varepsilon$. In addition, if $a = b = c = \varepsilon$ or $a \cdot b = c$, then $\pi_0(u c v) = \pi_0(u a) \cdot \pi_0(b v)$.

The proof of the lemma is straightforward by a case distinction, and thus omitted.

The next step consists in showing how to restrict a condensation tree to an arbitrary convex subset (further along, we will lift this operation to the generalized notion of evaluation tree):

**Definition 18.** Given a condensation tree $T$ over a linear ordering $\alpha$ and a convex subset $I$ of $\alpha$ (not necessarily an element of $T$), define the generalized subtree of $T$ rooted at $I$ as follows:

$$T|_{I} =^{\text{def}} \{I \cap J \mid J \in T, I \cap J \neq \emptyset\}.$$

The above operation can be seen as a further generalization of the notion of subtree that was given just after Definition 5. Below we prove that, not only $T|_{I}$ is a valid condensation tree, but also that this operation does not increase the rank.

**Lemma 19.** If $T$ is a condensation tree over $\alpha$ and $I$ is a convex subset of $\alpha$, then $T|_{I}$ is a condensation tree over $\alpha \cap I$. Furthermore, we have $\text{rank}(T|_{I}) \leq \text{rank}(T)$ and $(T|_{I})|_{J} = T|_{J}$ for all convex subsets $J$ of $I$.

*Proof.* We only prove that $T|_{I}$ is a condensation tree. The remaining claims follow easily from our definitions. The property stated in the first item of Definition 5 follows from the fact that $\alpha \in T$ and $\alpha \cap I = I \in T|_{I}$. To prove the property in the second item, consider two convexes $J, K$ in $T$. We have that either $J \subseteq K$ or $K \subseteq J$ or $J \cap K = \emptyset$. As a consequence, either $J \cap I \subseteq K \cap I$ or $K \cap I \subseteq J \cap I$ or $(J \cap I) \cap (K \cap I) = \emptyset$. Now, for the third item, consider two convexes $J, K$ in $T$ such that $K \cap I \in T|_{I}$ (or, equally, $K \cap I \neq \emptyset$) and $(K \cap I) \neq (J \cap I)$. Since $K \cap I$ is non-empty, this means that $J \cap K$ is non-empty too. Thus, either $K \subseteq J$ or $J \subseteq K$. If $J \subseteq K$ held, then we would have $(J \cap I) \subseteq (K \cap I)$, which would contradict $(K \cap I) \neq (J \cap I)$. We thus conclude that $K \subseteq J$. It remains to verify the property in the fourth item, namely, the fact that any subset of $T|_{I}$ that is totally ordered by inclusion is finite. Consider such a subset $C$. For each $J \in C$, define $T_{2J} = \{K \in T \mid K \cap I \supseteq J\}$. By construction, $T_{2J}$ is a subset of $T$ that is totally ordered by inclusion. In particular, $T_{2J}$ is finite and has a minimal element, denoted $\min(T_{2J})$. We define $C'$ as the set of all convexes of the form $\min(T_{2J})$, with $J \in C$. Since $J \subseteq J'$ implies $\min(T_{2J}) \subseteq \min(T_{2J'})$, we have that $C'$ is a subset of $T$ totally ordered by inclusion, and hence $C'$ is finite. Moreover, since each convex $J \in C$ can be written as $\min(T_{2J}) \cap I$, we have that, for all $J, J' \in C$, $J \neq J'$ iff $\min(T_{2J}) \neq \min(T_{2J'})$. Since $C'$ is finite, we conclude that $C$ is finite too. $\square$
Putting together all the previous definitions and lemmas, we can show that an
evaluation tree $\mathcal{T} = (T, \gamma)$ over a word $u$ provides not only a value for $u$, but also,
via restrictions to generalized subtrees, values for all the factors of $u$. Intuitively,
this means that the mapping $\gamma$ of $\mathcal{T}$ can be extended to all convex subsets $I$ of $\alpha$:

**Lemma 20.** For every evaluation tree $\mathcal{T} = (T, \gamma)$ over a word $u$ with domain $\alpha$ and every convex subset $I$ of $\alpha$, there is an evaluation tree $\mathcal{T}|_I = (T|_I, \gamma_I)$ such that $\gamma_I$ and $\gamma$ coincide over $(T|_I) \cap T = \{J \in T \mid J \subseteq I\}$.

In particular, by a slight abuse of notation, one can denote by $\gamma(I)$ the value associated with the convex $I$ in the evaluation tree $\mathcal{T}|_I$ (this notation is consistent with the value associated with $I$ in the evaluation tree $\mathcal{T}$, when $I \in T$).

*Proof.* Let us first assume that $I$ is an initial segment of $\alpha$, namely, for every $y \in I$ and every $x \le y$, $x \in I$. The proof is by induction on $T$, namely, on the rank of the underlying condensation tree. Let $C = \text{children}(\alpha)$ be the top-level condensation of $T$. We distinguish between two subcases.

If the condensation $\{I, \alpha \setminus I\}$ is coarser than $C$, then for all $K \in T|_I$, with $K \ne I$, we have $K \in T$. Hence it makes sense to define $\gamma_I(K) = \gamma(K)$. We complete the definition by letting $\gamma_I(I) = \pi_0(\gamma(C|_I))$, where $\gamma(C|_I)$ is the word with domain $C|_I = \{K \in C \mid K \subseteq I\}$ and with each position $J$ labelled by the value $\gamma(J)$ (thanks to Lemma 17 the function $\pi_0$ is defined on the word $\gamma(C|_I)$). It is easy to check that the $(T|_I, \gamma_I)$ thus defined is an evaluation tree over the factor $u|_I$ and that $\gamma_I$ and $\gamma$ coincide over $(T|_I) \cap T = \{K \in T \mid K \subseteq I\}$.

Otherwise, if the condensation $\{I, \alpha \setminus I\}$ is not coarser than $C$, then there exist three convex subsets $J_1 < J_2 < J_3$ of $\alpha$ such that (i) $\{J_1, J_2, J_3\}$ forms a partition coarser than $C$, (ii) $J_1 \subseteq I$, (iii) $J_3 \subseteq \alpha \setminus I$, and (iv) $J_2 \in C$ with $J_2 \cap I \ne \emptyset$ and $J_2 \setminus I \ne \emptyset$. In particular, we have that the convex $J_2 \cap I$ is included in a proper descendant of the root of $T$, and hence by Lemmas 10 and 19 $\text{rank}(T|_{J_2 \cap I}) < \text{rank}(T)$. We can thus apply the induction hypothesis to construct the evaluation tree $\mathcal{T}|_{J_2 \cap I} = (T|_{J_2 \cap I}, \gamma_{J_2 \cap I})$. Note that for every $K \in T|_{J_1}$ with $K \ne J_1$, we have $K \in T$. Hence it makes sense to define $\gamma_I(K) = \gamma(K)$. For every $K \in T|_{J_2}$, we define $\gamma_I(K) = \gamma_{J_2 \cap I}(K)$. Finally, we let $\gamma_I(I) = \pi_0(\gamma_I(C|_{J_1}) \gamma_{J_2 \cap I}(J_2 \cap I))$ (again this is well defined thanks to Lemma 17). It is easy to check that the $(T|_I, \gamma_I)$ thus defined is an evaluation tree over $u|_I$ and that $\gamma_I$ and $\gamma$ coincide over $(T|_I) \cap T = \{K \in T \mid K \subseteq I\}$.

The proof for the symmetric case, where $I$ is a final segment of $\alpha$, is analogous.

Finally, we consider the case where $I$ is not an initial segment, nor a final segment of $\alpha$. In this case it is possible to write $I$ as $I_1 \cap I_2$, where $I_1$ is an initial segment and $I_2$ is a final segment of $\alpha$. By Lemma 19 we have $T|_I = (T|_{I_1})|_{I_2}$, and hence it suffices to apply twice the cases for the initial/final segment discussed above. $\square$

Now that we have set up the basic tools for reasoning on evaluation trees and their restrictions, we begin to exploit the axioms of $\oplus$-algebras to prove a series of equivalence results. The first of these results can be seen as a form of associativity rule for the function $\pi_0$, but for which equality is required to hold only when every expression is defined:
**Lemma 21.** For every word $u$ of the form $\prod_{i \in \alpha} u_i$, with $\alpha$ countable linear ordering and $u_i \in S^{\oplus}$ for all $i \in \alpha$, if both $\pi_0(u)$ and $\pi_0(\prod_{i \in \alpha} \pi_0(u_i))$ are defined, then the two values are equal.

*Proof.* We prove the lemma by a case analysis, namely, by distinguishing the order type of $u$ (recall that, since $\pi_0(u)$ is defined, the order type of $u$ must be either finite, $\omega$, $\omega^*$, $\eta$, $1+\eta$, $\eta+1$, or $1+\eta+1$). For the sake of brevity, we let $v = \prod_{i \in \alpha} \pi_0(u_i)$.

If $u = a_1 \dots a_n$ for some $a_1, \dots, a_n \in S$, then $v$ has to be of the form $b_1 \dots b_m$, for some $m \ge 1$ and some $b_1, \dots, b_n \in S$. Since $\cdot$ is associative (see Axiom A1), we obtain $\pi_0(u) = a_1 \dots a_n = b_1 \dots b_m = \pi_0(v)$.

If $u = a e^{\omega}$ for some $a, e \in S$, with $e$ idempotent, then $v$ can be either of the form $c_1 \dots c_m$, for some $m \ge 1$ and some $c_1, \dots, c_m \in S$, or of the form $b f^{\omega}$, for some $b, f \in S$, with $f$ idempotent. If $v = c_1 \dots c_m$, say with $m \ge 2$ (the case $m=1$ is trivial), then we necessarily have $c_1 = a \cdot e^{n_1} = a \cdot e$ for some $n_1 \ge 0$, $c_i = e^{n_i} = e$ for all $2 \le i < m-1$ and some $n_2, \dots, n_{m-1} \ge 1$, and $c_m = e^{\tau}$. Axioms A1 and A2 together imply $e \cdot e^{\tau} = e \cdot (e \cdot e)^{\tau} = (e \cdot e)^{\tau} = e^{\tau}$. We thus have $\pi_0(u) = a \cdot e^{\tau} = c_1 \dots c_m = \pi_0(v)$. Otherwise, if $v = b d^{\omega}$, then, as above, we get $b = a \cdot e^{n_1} = a \cdot e$, for some $n_1 \ge 0$, and $f = e^{n_2} = e^{n_3} = \dots = e$, for some $n_2, n_3, \dots \ge 1$. Using Axioms A1 and A2 we finally derive $\pi_0(u) = a \cdot e^{\tau} = b \cdot f^{\tau} = \pi_0(v)$.

The case $u = e^{\omega^*} a$ is just symmetric to the previous case and uses Axiom A3 instead of Axiom A2.

Finally, the most interesting case is when $u = a P^{\eta} b$ for some non-empty set $P \subseteq S$ and some empty or singleton words $a, b \in S \smallsetminus \{\varepsilon\}$. We further distinguish some cases depending on the form of $v$:

* If $v = c_1 \dots c_m$, then the proof goes by induction on $m$. The interesting base case is $m=2$ (for $m=1$ the claim holds trivially). We further distinguish between five subcases. If the first factor $u_1$ has no last letter and the last factor $u_2$ has no first letter, then we have $c_1 = \pi_0(u_1) = a \cdot P^{\kappa}$ and $c_2 = \pi_0(u_2) = P^{\kappa} \cdot b$. Using Axiom A4, we get $\pi_0(u) = a \cdot P^{\kappa} \cdot b = (a \cdot P^{\kappa}) \cdot (P^{\kappa} \cdot b) = c_1 \cdot c_2 = \pi_0(v)$. If $u_1$ consists of a single letter, then this letter must be $a \neq \varepsilon$. Moreover, $u_2$ cannot have a first letter and hence, as above, we have $\pi_0(u_2) = P^{\kappa} \cdot b$. We thus derive $\pi_0(u) = a \cdot P^{\kappa} \cdot b = c_1 \cdot c_2 = \pi_0(v)$. If $u_1$ has a last letter, say $p$, but length greater than 1, then $p$ must belong to $P$ and $u_2$ has no first letter. We thus have $\pi_0(u) = a \cdot P^{\kappa} \cdot b = (a \cdot P^{\kappa} \cdot p) \cdot (P^{\kappa} \cdot b) = \pi_0(v)$. The cases where $u_2$ has length 1 and where $u_2$ has a first letter and length greater than 1 are symmetric. Finally, the induction for $m > 2$ is straightforward.

* If $v = c e^{\omega}$, then, by distinguishing some subcases as above, one verifies that $c = \pi_0(u_1)$ is either $a$ or $a \cdot P^{\kappa} \cdot p$, for some $p \in P \smallsetminus \{\varepsilon\}$, and that $e = \pi_0(u_2) = \pi_0(u_3) = \dots$ is either $P^{\kappa} \cdot q$ or $q \cdot P^{\kappa}$, for some $q \in P \smallsetminus \{\varepsilon\}$, depending on whether $u_1$ has a first letter or not. Depending on the various subcases, and using Axiom A4, we derive either $\pi_0(u) = a \cdot P^{\kappa} = a \cdot (P^{\kappa} \cdot q)^{\tau} = \pi_0(v)$, or $\pi_0(u) = a \cdot P^{\kappa} = (a \cdot P^{\kappa} \cdot p) \cdot (P^{\kappa} \cdot q)^{\tau} = \pi_0(v)$, or $\pi_0(u) = a \cdot P^{\kappa} = (a \cdot P^{\kappa}) \cdot (q \cdot P^{\kappa}) = \pi_0(v)$.

* If $v = e^{\omega^*} c$, then the claim holds by symmetry with the previous case.
* If $v = cR^\eta d$ for some non-empty set $R \subseteq S$ and some empty or singleton words $c, d \in S \upharpoonright \{\varepsilon\}$, then we prove that $R$ is included in $P \cup (P \upharpoonright \{\varepsilon\}) \cdot P^\kappa \cdot (P \upharpoonright \{\varepsilon\})$. Let us treat first the case $c = d = \varepsilon$. Since $v$ has no first nor final letter, this implies $a = b = \varepsilon$. Let us consider an element $r \in R$ and a corresponding factor $u_i$ of $u$, with $i \in \alpha$, such that $\pi_0(u_i) = r$. If $u_i$ consists of the single letter $r$, then we clearly have $r \in P$. Otherwise $u_i$ has more than one letter and, depending on the existence of a first/last letter in $u_i$, we get one of the four possibilities $r = P^\kappa, r = p \cdot P^\kappa, r = P^{\kappa,q}, r = p \cdot P^{\kappa,q}$, for suitable $p, q \in P$. This proves that $R$ is included in $P \cup (P \upharpoonright \{\varepsilon\}) \cdot P^\kappa \cdot (P \upharpoonright \{\varepsilon\})$. Using Axiom A4 we immediately obtain $\pi_0(u) = P^\kappa = R^\kappa = \pi_0(v)$. The general case where $c, d \in S \upharpoonright \{\varepsilon\}$, can be dealt with by using similar arguments plus Axiom A1.
□

**Corollary 22.** Let $u$ be a word with domain $\alpha$ such that $\pi_0(u)$ is defined and let $\mathcal{T} = (T, \gamma)$ be an evaluation tree over $u$. Then $\pi_0(u) = \gamma(\alpha)$.

*Proof.* We prove the claim by induction on $\mathcal{T}$. If $\mathcal{T}$ consists of a single node, then this node must be a leaf and $\alpha$ must be a singleton leaf, and hence the claim follows immediately by definition of evaluation tree. Otherwise, let $C = \text{children}(\alpha)$ be the top-level condensation. By Lemma 17, we know that $\pi_0(u|_I)$ is defined for all $I \in C$. We can then use the induction hypothesis on the evaluation tree $\mathcal{T}|_I$ and obtain $\pi_0(u|_I) = \gamma(I)$. Finally, using Lemma 21, we get $\pi_0(u) = \pi_0(\gamma(C)) = \gamma(\alpha)$. □

The following series of lemmas prove equalities between the value at the root of an evaluation tree and the values induced by $\pi_0$ under different condensations of the root. We first consider finite condensations, then $\omega$-condensations (and, by symmetry, $\omega^*$-condensations), and finally $\eta$-condensations. The gathering of those results will naturally entail that two evaluation trees over the same word have the same value (see Corollary 27).

**Lemma 23.** Given a word $u$ with domain $\alpha$, an evaluation tree $\mathcal{T} = (T, \gamma)$ over $u$, and a finite condensation $I_1 < \dots < I_n$ of $\alpha$, we have $\gamma(\alpha) = \gamma(I_1) \dots \gamma(I_n)$.

*Proof.* The proof is by induction on $\mathcal{T}$. If $\mathcal{T}$ consists of a single leaf, then $\alpha$ must be a singleton and hence $n=1$ and the claim follows trivially. Let us now consider the case where $\mathcal{T}$ has more than one node. We only prove the claim for $n=2$ (for $n=1$ it is obvious and for $n>2$ it follows from a simple induction). Let $C = \text{children}(\alpha)$ be the top-level condensation and let $J$ be the unique convex subset in $C$ that intersects both $I_1$ and $I_2$ (if $C$ does not contain such an element, then we let $J = \emptyset$). For the sake of brevity, we define, for both $i=1$ and $i=2$, $C_i = \{K \in C \mid K \subseteq I_i\}$, $u_i = \bigcap_{K \in C_i} \gamma(K)$, and $a_i = \gamma(J \cap I_i)$ (with the convention that $\gamma(J \cap I_i) = \varepsilon$ if $J = \emptyset$). Note that $C = C_1 \cup \{J\} \cup C_2$ if $J \neq \emptyset$ (resp., $C = C_1 \cup C_2$ if $J = \emptyset$) and hence $\gamma(\alpha) = \pi_0(u_1 \gamma(J) u_2)$ (we assume that $\gamma(J) = \varepsilon$ if $J = \emptyset$). Let us consider the case where $J$ is not empty (the case $J = \emptyset$ is similar). Since $J \in C$ and $C = \text{children}(\alpha)$, we have $\text{rank}(\mathcal{T}|_J) < \text{rank}(\mathcal{T})$ and hence we can apply the induction hypothesis to the evaluation tree $\mathcal{T}|_J$ and the condensation $\{J \cap I_1, J \cap I_2\}$ of $\alpha|_J$. We thus obtain $\gamma(J) = \gamma(J \cap I_1) \cdot \gamma(J \cap I_2) = a_1 \cdot a_2$ and hence $\gamma(\alpha) = \pi_0(u_1 (a_1 \cdot a_2) u_2)$. Lemma 17
then implies $\pi_0(u_1(a_1 \cdot a_2)u_2) = \pi_0(u_1a_1) \cdot \pi_0(u_2a_2)$. Similarly, Lemma 21 implies $\pi_0(u_1a_1) = \gamma(I_1)$ and $\pi_0(u_2a_2) = \gamma(I_2)$. Overall, we get $\pi_0(\alpha) = \gamma(I_1) \cdot \gamma(I_2)$. $\square$

**Lemma 24.** Given a word $u$ with domain $\alpha$, an evaluation tree $\mathcal{T} = (T, \gamma)$ over $u$, and an $\omega$-condensation $I_0 < I_1 < I_2 < \dots$ of $\alpha$ such that $\gamma(I_1) = \gamma(I_2) = \dots$ is an idempotent, we have $\gamma(\alpha) = \gamma(I_0) \cdot \gamma(I_1)^T$.

*Proof.* The proof is again by induction on $\mathcal{T}$. Note that the case of $\mathcal{T}$ consisting of a single leaf cannot happen. Let $C = \text{children}(\alpha)$ be the top-level condensation. We distinguish two cases depending on whether $C$ has a maximal element or not.

Suppose that $C$ has a maximal element, say $J_{\max}$, and $C \neq \{J_{\max}\}$ (the case where $C = \{J_{\max}\}$ can be considered as a degenerate case, which can be dealt with by similar arguments). We can find a condensation $K_1 < K_2$ of $\alpha$ that is coarser than $I_0 < I_1 < I_2 < \dots$ and such that $K_2 \subseteq J_{\max}$. By Lemma 23, we have $\gamma(\alpha) = \gamma(K_1) \cdot \gamma(K_2)$. Moreover, since $K_1$ is the union of a finite sequence of convex subsets $I_0, I_1, \dots, I_k$, by repeatedly applying Lemma 21, we obtain $\gamma(K_1) = \gamma(I_0) \cdot \gamma(I_1) \cdots \gamma(I_k) = \gamma(I_0) \cdot \gamma(I_1)$ (the last equality follows from the fact that $\gamma(I_1) = \gamma(I_2) = \dots$ is an idempotent). Finally, from the induction hypothesis (note that $\text{rank}(\mathcal{T}|_{K_2}) < \text{rank}(\mathcal{T}))$, we get $\gamma(K_2) = \gamma(I_1)^T$. We thus conclude that $\gamma(\alpha) = (\gamma(I_0) \cdot \gamma(I_1)) \cdot (\gamma(I_1)^T) = \gamma(I_0) \cdot \gamma(I_1)^T$.

If $C$ has no maximal element, then, using standard techniques and Ramsey's Theorem (Lemma 15), one can construct an $\omega$-condensation $J_0 < K_1 < J_1 < K_2 < J_2 < \dots$ of $\alpha$ such that:

* $\{J_0 \cup K_1, J_1 \cup K_2, \dots\}$ is coarser than $\{I_0, I_1, I_2, \dots\}$,

* $\{J_0, K_1 \cup J_1, K_2 \cup J_2, \dots\}$ is coarser than $C$,

* $\gamma(K_1 \cup J_1) = \gamma(K_2 \cup J_2) = \dots$ is an idempotent.

Let $\gamma(C)$ be the word with domain $C$ where each position $H \in C$ is labelled by the value $\gamma(H)$. By construction, we have $\gamma(\alpha) = \pi_0(\gamma(C))$. Moreover, since the condensation $\{J_0, K_1 \cup J_1, K_2 \cup J_2, \dots\}$ is coarser than $C$, by repeatedly applying Lemma 21, we obtain $\pi_0(\gamma(C)) = \pi_0(\gamma(J_0) \gamma(K_1 \cup J_1) \gamma(K_2 \cup J_2) \dots) = \gamma(J_0) \cdot \gamma(K_1 \cup J_1)^T$. Similarly, since $\{J_0 \cup K_1, J_1 \cup K_2, \dots\}$ is coarser than $\{I_0, I_1, I_2, \dots\}$ and $\gamma(I_1) = \gamma(I_2) = \dots$ is an idempotent, we have $\gamma(J_0 \cup K_1) = \gamma(I_0) \cdot \gamma(I_1)$ and $\gamma(J_1 \cup K_2) = \gamma(J_2 \cup K_3) = \dots = \gamma(I_1)$. Thus, by Axioms A1 and A2, we obtain $\gamma(J_0) \cdot \gamma(K_1 \cup J_1)^T = \gamma(I_0) \cdot \gamma(I_1)^T$. $\square$

We can gather all the results seen so far and prove the following corollary (recall that an ordering is scattered if all dense suborderings of it are empty or singletons):

**Corollary 25.** Given a word $u$ with domain $\alpha$, an evaluation tree $\mathcal{T} = (T, \gamma)$ over $u$, a scattered condensation $C$ of $\alpha$, and an evaluation tree $\mathcal{T}' = (T', \gamma')$ over the word $\gamma(C) = \prod_{I \in C} \gamma(I)$ with domain $C$, we have $\gamma(\alpha) = \gamma'(C)$.

*Proof.* As a preliminary remark, note that since the condensation $C$ is scattered, we have that, for every node $J$ in the evaluation tree $\mathcal{T}' = (T', \gamma')$, the condensation
of $J$ induced by $\mathcal{T}'$ is scattered as well. The proof is by induction on $\mathcal{T}'$. If $\mathcal{T}'$ consists of a single node, then $\gamma(C)$ is a singleton word of value $\gamma(\alpha)$ and hence the statement boils down to $\gamma(\alpha) = \gamma(\alpha)$. Otherwise, let $D$ be the childhood of the root $C$ of $\mathcal{T}'$. From the induction hypothesis, we know that for every $J \in D$, $\gamma'(J) = \gamma(\cup J)$, where $\cup J$ denotes the union of all convex subsets of $J$ (recall that $J \subseteq C$). Moreover, if we denote by $\cup D$ the condensation of $\alpha$ obtained from the substitution of each element $J \in D$ by $\cup J$, we have

$$ \gamma'(C) = \pi_0\left(\prod_{J \in D} \gamma'(J)\right) = \pi_0\left(\prod_{J \in D} \gamma(\cup J)\right) = \pi_0\left(\gamma(\cup D)\right). $$

Note that the condensation $\cup D$ of $\alpha$ has the same order type of the condensation $D$ of $C$, namely, it is either a finite condensation, an $\omega$-condensation, or an $\omega^*$-condensation. Therefore, using either Lemma 23 or Lemma 24 (or its symmetric variant), we obtain $\pi_0(\gamma(\cup D)) = \gamma(\alpha)$. $\square$

It remains to consider the case of dense condensations, which give rise to $\eta$-shuffles:

**Lemma 26.** Given a word $u$ with domain $\alpha$, an evaluation tree $\mathcal{T} = (T, \gamma)$ over $u$, and a dense condensation $C$ of $\alpha$ such that $\gamma(C) = \prod_{I \in C} \gamma(I)$ is isomorphic to a word of the form a $P^\eta$ b, for some elements $a, b \in S \stackrel{\omega}{=} \{\varepsilon\}$ and some non-empty set $P \subseteq S$, we have $\gamma(\alpha) = a \cdot P^\kappa \cdot b$.

*Proof.* We remark here that the proof works for any condensation $C$, independently of the form of the word $\gamma(C)$. However, the use of the following technical arguments does only make sense when $C$ is a dense condensation. We prove the lemma by induction on $\mathcal{T}$. As in the proof of Lemma 24, the case of $\mathcal{T}$ consisting of a single node cannot happen. Let $D = \text{children}(\alpha)$ be the top-level condensation and let $E$ be the finest condensation that is coarser than or equal to both $C$ and $D$ (note that $E$ exists since condensations form a lattice structure with respect to the 'coarser than' relation). Moreover, let $\sim$ be the condensation over the condensed ordering $C$ such that, for every $I, I' \in C$, $I \sim I'$ holds iff either $I = I'$ or there is $J \in D$ with $I \subseteq J$ and $I' \subseteq J$. This can naturally be seen as a condensation $C'$ over $\alpha$ which is at least as coarse as $C$: the classes of $C'$ are either the single classes of $C$ that are not contained in any class of $D$, or the unions of the classes of $C$ that are contained in the same class of $D$. Furthermore, it is easy to see that $E$ is at least as coarse as $C'$. Below, we disclose further properties of the condensations $C, D, E$, and $C'$.

Let us consider a class $I \in C'$. Two cases can happen: either $I$ is included in some $J \in D$, and in this case $\gamma(I) = \pi_0(\gamma(C|_I))$ holds thanks to the induction hypothesis, or $I$ belongs to $C$, and hence $\gamma(I) = \pi_0(\gamma(C|_I))$ follows trivially. We have just proved that

$$ \forall I \in C' \quad \gamma(I) = \pi_0(\gamma(C|_I)). \qquad (1) $$

Now, let $I, I'$ be two distinct classes in $C'$. We claim that there exist $x \in I$ and $x' \in I'$ that are not equivalent for $D$, namely,

$$ \exists x \in I \exists x' \in I' \forall J \in D \quad x \notin J \lor x' \notin J. \qquad (2) $$
The proof of this property is by case distinction. If $I$ is contained in some $J \in D$ and $I'$ is contained in some $J' \in D$, then we necessarily have $J \neq J'$ (otherwise, we would have $I = I'$ by definition of $C'$) and hence Property (2) holds. Otherwise, either $I$ is not contained in any class $J \in D$, or $I'$ is not contained in any class $J \in D$. Without loss of generality, we assume that $I$ is not contained in any class $J \in D$. This means that there exists $J \in D$ such that $I \cap J \neq \emptyset$ and $I \setminus J \neq \emptyset$. Let us pick some $x' \in I'$. Clearly, $x'$ belongs to some $J' \in D$. Then either $J \cap J' = \emptyset$ or $J = J'$. In the first case, one chooses $x \in I \cap J$, while in the second case one chooses $x \in I \setminus J$. This completes the proof of Property (2).

From the above property, we can deduce the following:

$$ \begin{array}{l} \text{If } I, I' \in C', I < I', \text{ and } I, I' \subseteq K \text{ for some } K \in E, \text{ then} \\ \text{there are only finitely many classes } I'' \in C' \text{ between } I \text{ and } I'. \end{array} \qquad (3) $$

Indeed, suppose that the above property does not hold, namely, that there are infinitely many classes $I'' \in C'$ between $I$ and $I'$. In particular, we can find an $\omega$-sequence of classes $I_1, I_2, \dots$ such that $I = I_1 < I_2 < \dots < I'$ or $I < \dots < I_2 < I_1 = I'$. We only consider the first case (the second case is symmetric). By applying Property (2) to the classes $I_1, I_2, \dots$, we can find some points $x_1 \in I_1, x'_1 \in I_2, x_2 \in I_3, x'_2 \in I_4, \dots$ such that, for all $i \ge 1$, $x_i$ and $x'_i$ are not equivalent for $D$ (i.e., for all $J \in D$, $x_i \notin J$ or $x'_i \notin J$). Let $X$ be the set of all points $x \in \alpha$, with $x < I_i$ for some $i \ge 1$, and let $X'$ be the set of all points $x' \in \alpha$, with $x' > I_j$ for all $j \ge 1$. Since $D$ is a condensation, we have that for all $x \in X$ and all $x' \in X'$, $x$ and $x'$ are not equivalent for $D$. Moreover, by construction, all such points $x$ and $x'$ are not equivalent for $C'$, and hence neither for $C$ (recall that $C$ is finer than $C'$). Since $E$ is the defined as the finest condensation that is coarser than or equal to both $C$ and $D$ and since $X \cup X' = \alpha$, it follows that there is no class $K \in E$ that intersects both $X$ and $X'$. In particular, since $I \subseteq X$ and $I' \subseteq X'$, it follows that there is no class $K \in E$ such that $I \subseteq K$ and $I' \subseteq K$, which is a contradiction. This completes the proof of Property (3).

We prove the following last property:

$$ \forall K \in E \quad \gamma(K) = \pi_0(\gamma(C|_K)). \qquad (4) $$

Let $K \in E$ and let $T' = (T', \gamma')$ be an evaluation tree over the word $\gamma(C'|_K)$ (such a tree exists according to Proposition 8). From Property (3) we know that the condensation of $C'|_K$ induced by the evaluation tree $T'$ is scattered. We can thus apply Corollary 25 and obtain $\gamma(K) = \gamma'(C'|_K)$. Moreover, the value $\pi_0(\gamma(C'|_K))$ is defined and hence, by Corollary 22, $\gamma'(C'|_K) = \pi_0(\gamma(C'|_K))$. By Property (1), we obtain $\gamma(C'|_K) = \prod_{I \in C'|_K} \gamma(I) = \prod_{I \in C'|_K} \pi_0(\gamma(C|_I))$. Finally, from the properties of condensation trees, we derive $\pi_0(\gamma(C'|_K)) = \pi_0(\prod_{I \in C'|_K} \pi_0(\gamma(C|_I))) = \gamma(C|_K)$. This completes the proof of Property (4).

Towards a conclusion, we consider an evaluation tree $T'' = (T'', \gamma'')$ over the word $\gamma(E)$ (such a tree exists thanks to Proposition 8). From Property (4) we know that $\gamma(E) = \prod_{K \in E} \gamma(K) = \prod_{K \in E} \pi_0(\gamma(C|_K))$. Moreover, By Corollary 22, we know that $\pi_0(\gamma(C'|_K)) = \gamma''(K)$ and hence $\prod_{K \in E} \pi_0(\gamma(C|_K)) = \gamma''(E)$. Similarly, since
$E$ is at least as coarse as $D$, Corollary 22 implies $\gamma''(E) = \pi_0(\gamma(D)) = \gamma(\alpha)$. This completes the proof of the lemma. $\square$

**Corollary 27.** Given a word $u$ with domain $\alpha$, an evaluation tree $\mathcal{T} = (T, \gamma)$ over $u$, a condensation $C$ of $\alpha$, and an evaluation tree $\mathcal{T}' = (T', \gamma')$ over the word $\gamma(C) = \prod_{I \in C} \gamma(I)$ with domain $C$, we have $\gamma(\alpha) = \gamma'(C)$.

*Proof.* The proof is exactly the same as for Corollary 25, with the only difference that we do not use the assumption that the condensation $C$ is scattered and we use Lemma 26 for treating the nodes $I'$ of $\mathcal{T}'$ for which the condensation *children*($I'$) is dense. $\square$

Finally, Proposition 9 follows easily from the previous corollary.

*Proof of Proposition 9.* Let $\mathcal{T} = (T, \gamma)$ and $\mathcal{T}' = (T', \gamma')$ be two evaluation trees over the same word $u$ with domain $\alpha$ and let $C$ be the finest condensation of $\alpha$, whose classes are the singleton sets. Clearly, the evaluation tree $\mathcal{T}'$ is isomorphic to an evaluation tree $\mathcal{T}'' = (T'', \gamma'')$ over the word $\gamma(C) = \prod_{I \in C} \gamma(I)$ with domain $C$. Using Corollary 27 we immediately obtain that $\gamma(\alpha) = \gamma''(C) = \gamma'(\alpha)$. $\square$

# 4 From monadic second-order logic to $\otimes$-algebras

Let us recall that *monadic second-order* (MSO) logic is the extension of first-order logic with set quantifiers. We assume the reader to have some familiarity with this logic, as well as with the technique used by Büchi to translate MSO formulas into equivalent automata. A good survey can be found in [Tho97].

Here, we show a relatively direct consequence of the results obtained in the previous section, namely, that MSO formulas can be effectively translated to $\otimes$-algebras:

**Theorem 28.** The MSO definable $\otimes$-languages are effectively recognizable.

Before turning to the proof of the above result, let us remark that we could have equally well used the composition method of Shelah for establishing Theorem 28. Indeed, given any MSO sentence $\psi$, one can construct effectively a $\otimes$-algebra recognizing the language defined by $\psi$ [She75].

Our proof of Theorem 28 follows Büchi's approach, namely, we establish a number of closure properties for recognizable $\otimes$-languages. Then, each construction of the logic will be translated into an operation on languages. To disjunction corresponds union, to conjunction corresponds intersection, to negation corresponds complementation, etc. We assume the reader to be familiar with this approach (in particular the coding of the valuations of free variables).

The $\otimes$-languages corresponding to the atomic predicates are easily shown to be recognizable. Similarly, the language operations of intersection, union, and complementation can be implemented easily by means of classical algebraic operations:
**Lemma 29.** The recognizable ⊗-languages are effectively closed under intersection, union, and complementation.

*Proof.* Given two ⊗-monoids $(M_1, \pi_1)$ and $(M_2, \pi_2)$ recognizing the languages $L_1 = h_1^{-1}(F_1)$ and $L_2 = h_2^{-1}(F_2)$, respectively, with $F_1 \subseteq M_1$, $F_2 \subseteq M_2$, and $h_1$ and $h_2$ morphisms to $(M_1, \pi_1)$ and $(M_2, \pi_2)$, respectively, we have that $A^{\oplus} \setminus L_1 = h_1^{-1}(M_1 \setminus F_1)$, $L_1 \cap L_2 = (h_1 \times h_2)^{-1}(F_1 \times F_2)$, and $L_1 \cup L_2 = (h_1 \times h_2)^{-1}((M_1 \times M_2) \setminus (F_1 \times F_2))$. In particular, the complement of $L_1$ is recognized by $(M_1, \pi_1)$, while the union and the intersection of $L_1$ and $L_2$ are recognized by the product ⊗-monoid $(M_1 \times M_2, \pi_1 \times \pi_2)$. Moreover, the latter product can be easily implemented at the level of ⊗-algebras: the operators of a ⊗-algebra that corresponds to $(M_1 \times M_2, \pi_1 \times \pi_2)$ can be obtained by applying component-wise the operators of some ⊗-algebras that correspond to $(M_1, \pi_1)$ and $(M_2, \pi_2)$. □

What remains to be proved is the closure under projection. Formally, given a language $L$ over some alphabet $A$, and a mapping $f$ from $A$ to another alphabet $B$, the projection of $L$ via $f$ is the language $f(L)$, where $f$ is extended in a pointwise manner to words and languages. The logical operation of existential quantification corresponds, at the level of the defined languages, to a projection. Hence, it remains to prove the following:

**Lemma 30.** The recognizable ⊗-languages are effectively closed under projections.

*Proof.* We first describe the construction for a given ⊗-monoid $(M, \pi)$, and then show how to adapt the construction at the level of ⊗-algebras. The projection is implemented, as usual, by a powerset construction, namely, by providing the definition of a generalized product over $\mathcal{P}(M)$. Given two words $u$ and $U$ over $M$ and $\mathcal{P}(M)$, respectively, we write $u \in U$ if $\text{dom}(u) = \text{dom}(U)$ and $u(x) \in U(x)$ for all $x \in \text{dom}(U)$. We then define the mapping $\tilde{\pi}$ from $\mathcal{P}(M)^{\oplus}$ to $\mathcal{P}(M)$ by letting

$$ \tilde{\pi}(U) =^{\text{def}} \{ \pi(u) \mid u \in U \} \quad \text{for all } U \in \mathcal{P}(M)^{\oplus}. $$

Let us show that $\tilde{\pi}$ is associative. Consider a word $U$ over $\mathcal{P}(M)$ and a condensation $\sim$ of its domain. Then,

$$ \begin{align*} \tilde{\pi}(U) &= \{\pi(u) \mid u \in U\} \\ &= \{\pi(\prod_{I \in \alpha/\sim} \pi(u|_I)) \mid u \in U\} \\ &= \{\pi(\prod_{I \in \alpha/\sim} a_I) \mid a_I \in \tilde{\pi}(U|_I) \text{ for all } I \in \alpha/\sim\} \\ &= \tilde{\pi}(\prod_{I \in \alpha/\sim} \tilde{\pi}(U|_I)), \end{align*} $$

where the second equality is derived from the associativity of $\pi$. Hence $(\mathcal{P}(M), \tilde{\pi})$ is a ⊗-monoid.

Next, we show that $(\mathcal{P}(M), \tilde{\pi})$ recognizes any projection of a language recognized by $(M, \pi)$. Let let $L \subseteq A^{\oplus}$ be a language recognized by $(M, \pi)$ via some morphism $h : (A, \prod) \to (M, \pi)$, namely, $L = h^{-1}(h(L))$, and let $f : A \to B$ be a projection. We claim that the projected language $L' = f(L)$ is recognized by $(\mathcal{P}(M), \tilde{\pi})$ via the morphism $g = h \circ f^{-1} : (B, \prod) \to (\mathcal{P}(M), \tilde{\pi})$. Clearly, we have
$g^{-1}(g(L')) \supset L'$. For the opposite containment, consider a word $v \in g^{-1}(g(L'))$. By construction, there is a word $v' \in L'$ such that $g(v') = g(v)$. Since $v' \in L' = f(L)$, there is $w' \in L$ such that $v' = f(w')$. Moreover, since $g(v') = g(v)$, there is $w$ such that $f(w) = v$ and $h(w') = h(w)$. Finally, since $L = h^{-1}(h(L))$, we conclude that $w \in L$, and hence $v = f(w) \in L'$.

Thanks to Lemma 4 and Corollary 12, the construction of $(\mathcal{P}(M), \tilde{\pi})$ can be performed at the level of $\otimes$-algebras. More precisely, any $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ uniquely determines a $\otimes$-monoid $(M, \pi)$, and from this, using the powerset construction, one defines the $\otimes$-monoid $(\mathcal{P}(M), \tilde{\pi})$, and finally the induced $\otimes$-algebra $(\mathcal{P}(M), \{1\}, \tilde{\tau}, \tilde{\tau}^*, \tilde{\kappa})$. The crux in this line of arguments is that the correspondence between the original $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ and the final $\otimes$-algebra $(\mathcal{P}(M), \{1\}, \tilde{\tau}, \tilde{\tau}^*, \tilde{\kappa})$ may be, a priori, not effective. Below we explain why, in fact, this correspondence is effective, namely, we explain how each operator of the $\otimes$-algebra $(\mathcal{P}(M), \{1\}, \tilde{\tau}, \tilde{\tau}^*, \tilde{\kappa})$ can be computed using the initial $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ and some saturation process.

We give the intuition for constructing the most difficult and interesting operator $\tilde{\kappa}$, that is, for computing $P^{\tilde{\kappa}} = \tilde{\pi}(P^{\eta})$ for any given non-empty subset $P = \{A_1, \dots, A_k\}$ of $\mathcal{P}(M)$, using the operators of the $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$. We recall that $P^{\tilde{\kappa}} = \{1\}$ if $A_1 = \dots = A_k = \{1\}$, otherwise $P^{\tilde{\kappa}} = (P \setminus \{1\})^{\tilde{\kappa}}$. We also recall that $P^{\tilde{\kappa}}$ must represent the set $\{\pi(u) \mid u \in U, U \in P^{\eta}\}$ and hence the computation of $P^{\tilde{\kappa}}$ is very similar to that of $\{\pi(u) \mid u \in A^{\otimes}\}$, which was done in the proof of Theorem 13. The difference here is that one needs to relativise $u$ to the words that belong to $U$, for some $U \in P^{\eta}$. This can be achieved by performing a product of the $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ with a $\otimes$-algebra that recognizes the single-word language $\{P^{\eta}\}$, and then applying the saturation process of Theorem 13 on the resulting $\otimes$-algebra. $\square$

# 5 From $\otimes$-algebras to monadic second-order logic

We have seen in the previous section that every MSO formula defines a recognizable $\otimes$-language. In this section, we prove the converse. Hereafter, we refer to the $\forall$-fragment (resp., $\exists$-fragment) of MSO logic as the set of formulas that start with a block of universal (resp., existential) set quantifiers, followed by a first-order formula. Similarly, the $\exists\forall$-fragment consists of formulas starting with a block of existential set quantifiers followed by a formula of the $\forall$-fragment.

**Theorem 31.** The recognizable $\otimes$-languages are effectively MSO definable. Furthermore, such languages are definable in the $\exists\forall$-fragment of MSO logic.

We fix for the remaining of the section a morphism $h$ from $(A^{\otimes}, \Pi)$ to a $\otimes$-monoid $(M, \pi)$, with $M$ finite, and a subset $F$ of $M$. Let also $1, \cdot, \tau, \tau^*, \kappa$ be defined from $\pi$. Our goal is to show that $L = h^{-1}(F)$ is MSO definable. It is sufficient for this to show that for every $a \in M$, the language

$$ \pi^{-1}(a) = \{w \in M^{\otimes} : \pi(w) = a\}, $$
can be defined by a suitable MSO sentence $\varphi_a^{\text{value}}$. From this it will follow that
that $L = \bigcup_{a \in F} h^{-1}(a)$ is defined by the disjunction $\bigvee_{a \in F} \hat{\varphi}_a^{\text{value}}$, where $\hat{\varphi}_a^{\text{value}}$ is obtained from $\varphi_a^{\text{value}}$ by replacing every occurrence of an atom $b(x)$, with $b \in M$, by $\bigvee_{c \in h^{-1}(b) \cap A} c(x)$.

A reasonable approach for defining $\pi^{-1}(a)$ is to use a formula which, given $u \in M^{\oplus}$, guesses some object that 'witnesses' $\pi(u) = a$. The only objects that we have seen so far and that are able to "witness" $\pi(u) = a$ are evaluation trees. Unfortunately, there is no way an MSO formula can guess an evaluation tree, since their height cannot be bounded uniformly. That is why we use another kind of object for witnessing $\pi(u) = a$: the so-called Ramseian split, which is introduced just below.

**5.1 Ramseian splits**

Ramseian splits are not directly applied to words, but to additive labellings. Recall
that an additive labelling $\sigma$ from a linear ordering $\alpha$ to a semigroup $(M, \cdot)$ (which,
in our case, will be induced by the $\oplus$-monoid $(M, \pi)$) is a function that maps
any pair of elements $x < y$ from $\alpha$ to an element $\sigma(x, y) \in M$ in such a way that
$\sigma(x, y) \cdot \sigma(y, z) = \sigma(x, z)$ for all $x < y < z$ in $\alpha$.

Given two positions $x < y$ in a word $u$, denote by $[x,y)$ the interval $\{z \mid x \le z < y\}$.
Given a word $u$ and two positions $x < y$ in it, we define $\sigma_u(x,y)$
to be the element $\pi(u|_{[x,y)})$ of the $\oplus$-monoid $(M, \pi)$. Quite naturally, $\sigma_u$ is an
additive labelling, since for all $x < y < z$, we have $\sigma_u(x,y) \cdot \sigma_u(y,z) = \pi(u|_{[x,y)}) \cdot \pi(u|_{[y,z)}) = \pi(u|_{[x,y]} w|_{[y,z)}) = \pi(u|_{[x,z)}) = \sigma_u(x,z)$.

**Definition 32.** A split of height $n$ of a linear ordering $\alpha$ is a function $g : \alpha \to \{1, \dots, n\}$. Two elements $x, y \in \alpha$ are called ($k$-)neighbours iff $g(x) = g(y) = k$ and $g(z) \le k$ for all $z \in \alpha|_{[x,y] \cup [y,x]}$ (note that the neighbourhood relation is an equivalence). The split $g$ is said to be Ramseian for an additive labelling $\sigma : \alpha \to M$ iff for all equivalence classes $X \subseteq \alpha$ of the neighbourhood relation, there is an idempotent $e \in M$ such that $\sigma(x,y) = e$ for all $x < y$ in $X$.

**Theorem 33 (Colcombet [Col10]).** For every finite semigroup $(M, \cdot)$, every linear ordering $\alpha$, and every additive labelling $\sigma$ from $\alpha$ to $(M, \cdot)$, there is a split of $\alpha$ which is Ramseian for $\sigma$ and which has height at most $2|M|$.

**5.2 Inductive construction of formulas**

Below we construct a formula that, given a word $u$ of domain $\alpha$, guesses a split of
$\alpha$ of height at most $2|M|$, and uses it for representing the function that associates
with each convex subset $I$ of $\alpha$ the value $\pi(u|_I)$ in $M$. For the sake of simplicity,
we fix a word $u$ of domain $\alpha$ and the corresponding additive labelling $\sigma_u$ over $\alpha$
that is induced by $u$. We remark, however, that all constructions that follow are
uniform and do not depend on the chosen word $u$.

In the following, we make extensive use of properties, functions, sets that are
first-order definable from other parameters. For instance, when we say that a set $X$
is first-order definable from some variables $\bar{Y}$, we mean that there exists a first-order formula $\xi(x, \bar{Y})$ that describes the membership of $x$ in $X$ on the basis of $\bar{Y}$, that is, $x \in X$ iff $\xi(x, \bar{Y})$ holds on the given interpretation of $x$ and $\bar{Y}$. In practice, this means that it is never necessary to quantify over $X$ for defining properties concerning $X$: it is sufficient to replace each predicate $x \in X$ by the corresponding formula $\xi(x, \bar{Y})$. This remark is crucial for understanding why the construction we provide yields a formula in the $\exists\forall$-fragment of MSO logic.

Recall that we aim at constructing, for each $a \in M$, a sentence $\varphi_a^{\text{value}}$ that holds over the word $u$ iff $\pi(u) = a$. The starting point is to guess:

1. a split $g$ of $\alpha$ of height at most $2|M|$, and;

2. a function $f$ mapping each position $x \in \alpha$ to an idempotent $f(x) \in M$.

The intention is that a choice of $g$ and $f$ is good when $g$ is a Ramseian split for $\sigma_u$ and the function $f$ maps each position $x$ to the idempotent $f(x)$ that arises when the neighbourhood class of $x$ is considered (cf. Definition 32). In this a case, by a slight abuse of terminology, we say that $(g, f)$ is a *Ramseian pair*.

Observe that neither $g$ nor $f$ can be represented by a single monadic variable. However, since both $g$ and $f$ are functions from $\alpha$ to sets of bounded size ($2|M|$ for $g$, and $|M|$ for $f$), one can guess them using a fixed number of monadic variables. This kind of encoding is quite standard, and from now on we shall use explicitly the mappings $g$ and $f$ in our formulas, rather than their encodings.

Knowing a Ramseian pair $(g, f)$ is an advance towards computing the value of a word. Indeed, Ramseian splits can be used as “accelerating structures” in the sense that every computation of $\pi(u|_I)$ for some convex $I$ becomes significantly easier when a Ramseian split is known, namely, it becomes first-order definable in terms of the Ramseian split. This is formalized by the following lemma.

**Lemma 34.** Given $a \in M$, one can construct a first-order formula $\text{eval}_a(g, f, X)$ such that for every convex subset $I$ of $\alpha$:

* if $(g, f)$ is Ramseian, then $\text{eval}_a(g, f, I)$ holds iff $\pi(u|_I) = a$,

* if both $\text{eval}_a(g, f, I)$ and $\text{eval}_b(g, f, I)$ hold, then $a = b$.

*Proof.* As already mentioned, we encode both functions $g$ and $f$ by tuples of monadic predicates. This allows us to use shorthands such as $g(x) = k$, where $x$ is a first-order variable and $1 \le k \le 2|M|$, for claiming that the point $x$ of the underlying word $u$ is mapped via $g$ to the number $k$. Similarly, we encode the convex subset $I$ of $\alpha$ by a monadic predicate and we write $x \in I$ as a shorthand for a formula that states that the point $x$ belongs to $I$.

We assume from now that $(g, f)$ is Ramseian. Under this assumption, it will be clear that the constructed formulas will satisfy the desired properties. We remark, however, that the following definitions make sense also in the case when $(g, f)$ is not Ramseian, in which case only the second condition of the lemma will be guaranteed.
Given a convex $I$, we denote by $\text{level}(g, I)$ the maximal value of $g(x)$ for $x$ ranging over $I$. Of course, the properties $\text{level}(g, I) = k$ and $\text{level}(g, I) \le k$ are first-order definable in terms of $g$ and $I$.

We will construct by induction on $k \in \{0, 1, \dots, 2|M|\}$ a partial function $\text{eval}^k$ that maps some triples $(g, f, I)$ to elements $\text{eval}^k(g, f, I) \in M$ in such a way that the following properties hold:

* $\text{eval}^k(g, f, I) = a$ is definable by a first-order formula, say $\text{eval}_a^k(g, f, I)$, for each $a \in M$,

* $\text{eval}^k(g, f, I)$ is defined iff $\text{level}(g, I) \le k$, and in this case it coincides with $\pi(u|_I)$ (provided $(g, f)$ is Ramseian).

The base case is when $k = 0$. In this case, we define $\text{eval}^k(g, f, I)$ to be the neutral element 1 when $I = \emptyset$, and we let $\text{eval}^k(g, f, I)$ be undefined when $I \ne \emptyset$. Of course, this is first-order definable and satisfies the expected induction hypothesis.

Let us now construct the partial function $\text{eval}^k(g, f, I)$ for any $k \ge 1$. First, if $\text{level}(g, I) < k$, then one simply outputs $\text{eval}^{k-1}(g, f, I)$. Otherwise, the convex subset $I$ can be uniquely partitioned into $X \subset J \subset Y$ in such a way that $X \cup J \cup Y = I$ and $J$ is the minimal convex subset containing $I \cap g^{-1}(k)$. Note that the sets $X$, $J$, and $Y$ are first-order definable in the parameters $I$ and $g$, that is, membership of any point $x$ in $X$ (resp., $J$, $Y$) is characterized by a first-order formula in the variables $x$, $I$, and $g$. Furthermore, fix $e$ to be $f(x)$ for some $x \in I \cap g^{-1}(k)$. From the assumption that $I$ has level $k$ for $g$, we know that all elements in $I \cap g^{-1}(k)$ are neighbours. In particular, the fact that $g$ is a Ramseian split for $\sigma_u$ means that $\sigma_u(x, y) = e$ for all $x < y$ chosen in $I \cap g^{-1}(k)$. The mapping $\text{eval}^k(g, f, I)$ is defined below by a case distinction (we remark that the following definitions are not symmetric with respect to the underlying order, and this reflects the asymmetry occurring in the definition of $\sigma_u$, that is, $\sigma_u(x, y) = \pi(u|_{[x,y]})$ for all $x < y \in \alpha$):

1. if $J$ is a singleton $\{x\}$, then

$$ \text{eval}^k(g, f, I) = \text{eval}^{k-1}(g, f, X) \cdot u(x) \cdot \text{eval}^{k-1}(g, f, Y), $$

2. if $J$ has distinct minimal and maximal elements and $y = \max(J)$, then

$$ \text{eval}^k(g, f, I) = \text{eval}^{k-1}(g, f, X) \cdot e \cdot u(y) \cdot \text{eval}^{k-1}(g, f, Y), $$

3. if $J$ has no minimal element but has a maximal element $y$, then

$$ \text{eval}^k(g, f, I) = \text{eval}^{k-1}(g, f, X) \cdot e^{\tau^*} \cdot u(y) \cdot \text{eval}^{k-1}(g, f, Y), $$

4. if $J$ has a minimal element but no maximal element, then

$$ \text{eval}^k(g, f, I) = \text{eval}^{k-1}(g, f, X) \cdot e^{\tau} \cdot \text{eval}^{k-1}(g, f, Y), $$

5. if $J$ has no minimal element and no maximal element, then

$$ \text{eval}^k(g, f, I) = \text{eval}^{k-1}(g, f, X) \cdot e^{\tau^*} \cdot e^{\tau} \cdot \text{eval}^{k-1}(g, f, Y). $$
One easily checks that the function eval^k can be defined by first-order formulas of the form eval_a^k(g, f, I), with a ∈ M. It is also easy to see that if (g, f) is Ramseian and level(g, I) ≤ k, then eval^k(g, f, I) coincides with π(u|I).

At this step, the first conclusion of the lemma is already satisfied by the first-order formulas eval_a^{2|M|}(g, f, I). The second point, however, is false in general. Indeed, we did not pay attention so far on what the formulas compute in the case where (g, f) is not Ramseian. In particular, it can happen that both formulas eval_a^{2|M|}(g, f, I) and eval_b^{2|M|}(g, f, I) hold for distinct elements a, b ∈ M. However, this can be easily fixed using the following formula:

$$ eval_a(g, f, I) =^{\text{def}} eval_a^{2|M|}(g, f, I) \wedge \bigwedge_{b \neq a} \neg eval_b^{2|M|}(g, f, I). $$

This formula ensures the second property of the lemma by construction, and behaves like eval_s whenever (g, f) is Ramseian. □

The formulas constructed in Lemma 34 can be seen as defining a partial function eval that maps g, f, I to some element a ∈ M (the second item in the lemma enforces that there is no ambiguity about the value, namely, that this is a function and not a relation). Hereafter, we simply use the notation eval(g, f, I) as if it were a function.

One needs now to enforce that eval(g, f, I) coincides with π(u|I), even without assuming that (g, f) is Ramseian. For this, one uses condensations. A priori, a condensation is not representable by monadic variables, since it is a binary relation. However, any set X ⊆ α naturally defines the relation ≈_X such that x ≈_X y iff either [x, y] ⊆ X, or [x, y] ∩ X = ∅. It is easy to check that this relation is a condensation. A form of converse result also holds:

**Lemma 35.** For every condensation ~, there is X such that ~ and ≈_X coincide.

*Proof.* It is easy to see that, given a linear ordering β, there exists a subset Y of β such that for all x < y in β, [x, y] intersects both Y and its complement β \ Y: indeed, one can first prove this for scattered linear orderings and for dense linear orderings, and then combine the results for these subcases using the fact that every linear ordering is a dense sum of non-empty scattered linear orderings [Ros82].

The lemma follows easily from the above argument: consider Y obtained from the claim above applied to the condensed ordering β = α/∼. We construct the desired set X in such a way that it contains the elements of the equivalence classes of ~ that belong to Y, i.e., X = {x | [x]~ ∈ Y}. It is easy to see that x ~ y iff x ≈_X y. □

Lemma 35 tells us that it is possible to work with condensations as if they were monadic variables. In particular, in the sequel we use variables for condensations and we tacitly assume that they are encoded by the sets obtained from Lemma 35.

Given a convex subset I of α and some condensation ~ of α|_I, we denote by u[I, ~] the word with domain β = (α|_I)/~ in which every ~-equivalence class J
is labelled by eval(g, f, J). One can easily define a formula consistency(g, f) that checks that, for all convex subsets I and all condensations ~ of α|I, the following conditions hold:

$$
(C1) \text{ if } I \text{ is a singleton } \{x\}, \text{ then } \mathrm{eval}(g, f, I) = u(x),
$$

$$
(C2) \text{ if } u[I, \sim] = ab \text{ for some } a, b \in M, \text{ then } \mathrm{eval}(g, f, I) = a \cdot b,
$$

$$
(C3) \text{ if } u[I, \sim] = e^{\omega} \text{ for some idempotent } e \in M, \text{ then } \mathrm{eval}(g, f, I) = e^{\tau},
$$

$$
(C4) \text{ if } u[I, \sim] = e^{\omega^*} \text{ for some idempotent } e \in M, \text{ then } \mathrm{eval}(g, f, I) = e^{\tau^*},
$$

$$
(C5) \text{ if } u[I, \sim] = P^{\eta} \text{ for some non-empty set } P \subseteq M, \text{ then } \mathrm{eval}(g, f, I) = P^{\kappa}.
$$

For some fixed $I$ and $\sim$, the above tests require access to the elements $u[I, \sim](J)$, where $J$ is a $\sim$-equivalence class of $\alpha|_I$. Since the property of $\sim$-equivalence for two positions $x, y \in \alpha|_I$ is first-order definable, we know that for every position $x \in \alpha|_I$, the element $\mathrm{eval}(g, f, [x]_{\sim})$ is first-order definable from $x$. This shows that the above properties can be expressed by first-order formulas and hence consistency($g, f$) is a formula in the $\forall$-fragment of MSO logic.

The last key argument is to show how the ‘local’ consistency constraints C1–C5
imply a ‘global’ consistency property. This is done by the following lemma.

**Lemma 36.** If consistency(g, f) holds, then eval(g, f, I) = π(u|I) for all convex subsets I of α.

*Proof.* Recall that, given a convex subset *I* of *α* and a condensation ~ of *α*|*, *u*[*I*, ~] is the word with domain *β* = (*α*|*)/~ in which every ~-equivalence class *J* is labelled by eval(*g*, *f*, *J*). Suppose that consistency(*g*, *f*) holds, namely, that for all convex subsets *I* of *α* and all condensations ~ of *α*|*, the conditions C1–C5 are satisfied.

To show that eval(g, f, I) = π(u|I) for all convex subsets I, we use again
evaluation trees. Precisely, we fix a convex subset I of α and an evaluation tree
T = (T, γ) over the word u|I (the evaluation tree exists thanks to Proposition 8),
and we prove, by an induction on T, that

$$
\mathrm{eval}(g, f, I) = \gamma(I).
$$

Since $\gamma(I) = \pi(u|I)$ (by Proposition 9), it follows that $\mathrm{eval}(g, f, I) = \pi(u|I)$.

If $\mathcal{T}$ consists of a single leaf, then $I$ is a singleton of the form $\{x\}$. Condition C1
then immediately implies $\mathrm{eval}(g, f, I) = u(x) = \gamma(I)$.

If the root of $\mathcal{T}$ is not a leaf, then we let $\sim$ be the condensation of $\alpha|_I$ induced
by the children of the root of $\mathcal{T}$ and we let $\beta = (\alpha|_I)/_{\sim}$ be the corresponding
condensed ordering (formally, $\beta = \mathbf{children}(I)$). Note that for every class $J \in \beta$, $\mathcal{T}|_J$
is a subtree of $\mathcal{T}$. From the induction hypothesis on the evaluation tree $\mathcal{T}|_J$, we
have $\mathrm{eval}(g, f, J) = \gamma(J)$ for all $J \in \beta$. Moreover, we know from the definition of
$u[I, \sim]$ that $u[I, \sim](J) = \mathrm{eval}(g, f, J)$, for all $J \in \beta$, and hence $u[I, \sim]$ is isomorphic
to the word $\coprod_{J \in \beta} \gamma(J)$. We also know from the definition of $\mathcal{T}$ that the image
under $\pi_0$ of the word $\coprod_{J \in \beta} \gamma(J)$ is defined. From this we derive that $\coprod_{J \in \beta} \gamma(J)$ is
isomorphic to one of the following words:
1. a word $ab$, for some $a, b \in M$,

2. an $\omega$-word $e^\omega$, for some idempotent $e \in M$,

3. an $\omega^*$-word $e^{\omega^*}$, for some idempotent $e \in M$,

4. a shuffle $P^\eta$, for some non-empty subset $P$ of $M$.

We only analyse the first two cases (the remaining cases are all similar).

If the word $\prod_{J \in \beta} \gamma(J)$ is of the form $ab$, with $a, b \in M$, then we let $J_1$ and $J_2$, with $J_1 < J_2$, be the two positions in it (recall that these are $\sim$-equivalence classes for $\alpha|_I$). Thanks to the inductive hypothesis, we have $\mathrm{eval}(g, f, J_1) = u[I, \sim](J_1) = \gamma(J_1) = a$ and $\mathrm{eval}(g, f, J_2) = u[I, \sim](J_2) = \gamma(J_2) = b$. From Condition C2, using the condensation $\sim$, we derive $\mathrm{eval}(g, f, I) = \mathrm{eval}(g, f, J_1 \cup J_2) = a \cdot b$, and from this we easily conclude that

$$ \mathrm{eval}(g, f, I) = a \cdot b = \pi_0(ab) = \pi_0(\gamma(J_1) \gamma(J_2)) = \gamma(I). $$

Let us now consider the case where $\prod_{J \in \beta} \gamma(J)$ is an $\omega$-word of the form $e^\omega$, for some idempotent $e \in M$. We denote by $J_1 < J_2 < \dots$ the positions in $\prod_{J \in \beta} \gamma(J)$ (recall that these are $\sim$-equivalence classes for $\alpha|_I$). As in the previous case, we know from the inductive hypothesis that $\mathrm{eval}(g, f, J_i) = u[I, \sim](J_i) = \gamma(J_i) = e$ for all $i = 1, 2, \dots$. We know from Condition C3 that $\mathrm{eval}(g, f, I) = \mathrm{eval}(g, f, J_1 \cup J_2 \cup \dots) = e^T$. Finally, we derive

$$ \mathrm{eval}(g, f, I) = e^T = \pi_0(e^\omega) = \pi_0\left(\prod_{J \in \beta} \gamma(J)\right) = \gamma(I). $$

<figure><img src="image_4.png" /></figure>

We conclude the section by showing how Lemma 36 implies Theorem 31. We claim that, given $a \in M$, the language $\pi^{-1}(a)$ is defined by the following sentence in the $\exists\forall$-fragment of MSO logic:

$$ \varphi_a^{\mathrm{value}} =^{\mathrm{def}} \exists g. \exists f. \mathrm{consistency}(g, f) \land \mathrm{eval}(g, f, \alpha) = a. $$

Let $\pi(u) = a$. One can find a Ramseian pair $(g, f)$ using Theorem 33. Lemma 34 then implies $\pi(u|_I) = \mathrm{eval}(g, f, I)$ for all convex subsets $I$. Since $\pi$ is a product, the constraints C1–C5 are satisfied and $\mathrm{consistency}(g, f)$ holds. This proves that $\varphi_a^{\mathrm{value}}$ holds. Conversely, if $\varphi_a^{\mathrm{value}}$ holds, then $\mathrm{consistency}(g, f)$ holds for some $(g, f)$. Lemma 36 then implies

$$ \pi(u) = \pi(u|_{\alpha}) = \mathrm{eval}(g, f, \alpha) = a. $$

# 6 Applications

In this section we present consequences of our results.
## 6.1 Collapse of the quantifier hierarchy

A first consequence of Theorems 28 and 31 is that the hierarchy of monadic quantifier alternation for MSO logic interpreted over countable words collapses to its $∃∀$-fragment. Clearly, since MSO logic is closed under complementation, it also collapses to its $∀∃$-fragment:

**Corollary 37.** Every $⊗$-language definable in MSO logic can be equally defined in the $∃∀$-fragment and in the $∀∃$-fragment.

Moreover, the collapse result is optimal, in the sense that there exist MSO definable languages that are not definable in the $∃$-fragment:

**Proposition 38.** The language $L_∀$ of countable scattered words over the singleton alphabet $\{a\}$ cannot be defined in the $∃$-fragment of MSO logic.

*Proof.* We first recall a folklore result that shows that the language $L_∀$ cannot be defined in first-order logic. The argument is based on Ehrenfeucht-Fraïssé games (we refer the reader to [Tho93, Hod93, Ros82] for basic knowledge on these games). One begins by fixing a number $n \in \mathbb{N}$ and suitable words $w \in L_∀$ and $w' \notin L_∀$, which may depend on $n$. One then considers $n$ rounds of the Ehrenfeucht-Fraïssé game over $w$ and $w'$, where two players, called Spoiler and Duplicator, alternatively mark positions in $w$ and $w'$ inducing partial isomorphisms. More precisely, at each round $k = 1, \dots, n$, Spoiler marks a position in one of the two words, say either $x_k \in \text{dom}(w)$ or $y_k \in \text{dom}(w')$ – intuitively this corresponds to quantifying existentially or universally over $w$. Duplicator responds by choosing a corresponding position in the other structure, say either $y_k \in \text{dom}(w')$ or $x_k \in \text{dom}(w)$. The responses of Duplicator must enforce an isomorphism between the induced substructures $w|_{\{x_1, \dots, x_k\}}$ and $w'|_{\{y_1, \dots, y_k\}}$. If Duplicator cannot move while preserving the invariant, he loses the game. If he survives $n$ rounds, he wins. We know from Fraïssé's Theorem that Duplicator can win the $n$-round game if, and only if, $w$ and $w'$ cannot be distinguished by any formula of first-order logic with $n$ nested quantifiers – in particular, if this happens for arbitrarily large $n \in \mathbb{N}$, then $L_∀$ cannot be defined in first-order logic.

Below, we show that, for all $n \in \mathbb{N}$, Duplicator has a strategy to survive $n$ rounds of the Ehrenfeucht-Fraïssé game induced by the words

$$w =^{\text{def}} a^{\omega} \in L_{\forall} \quad \text{and} \quad w' =^{\text{def}} a^{\omega} (a^{\omega} a^{\omega})^{\eta} \notin L_{\forall}.$$

Without loss of generality, we can assume that during the first round of the game the left endpoints of $w$ and $w'$ are marked. For the subsequent rounds, the strategy of Duplicator will enforce the following invariant: if the distance between two positions $x_i, x_j$ that are marked in $w$ at rounds $j < i$ is less than $2^{n-i}$, then so is the distance between the corresponding positions $y_i, y_j$ that are marked in $w'$, and vice versa. On the other hand, if at round $i$ Spoiler picks a position $x_i$ in $w$ that is at distance at least $2^{n-i}$ from all previously marked positions, then, Duplicator can responds by picking a position $y_i$ inside a factor $a^{\omega} a^{\omega}$ of $w'$ that has no marked positions, thus guaranteeing that $y_i$ is at distance at least $2^{n-i}$ from all
other marked positions. This strategy guarantees that Duplicator survives at least $n$ rounds of the game. The fact that winning strategies for Duplicator exist for all $n \in \mathbb{N}$, proves that $L_\nu$ is not definable in first-order logic.

Now, it is straightforward to generalize the above argument to show that, for every first-order formula $\varphi$ and every pair of finite words $u, v$ over a finite alphabet, the following implication holds:

$$ uv^{\omega} \models \varphi \quad \text{implies} \quad uv^{\omega} (v^{\omega*} v^{\omega})^{\eta} \models \varphi. \qquad (*) $$

We can use this result to show that the language $L_\nu$ cannot be defined in the $\exists$-fragment of MSO logic. Suppose, by way of contradiction, that there is a sentence $\psi = \exists \bar{X} \varphi(\bar{X})$ that defines $L_\nu$, where $\varphi$ is a first-order formula with free variables among $\bar{X} = X_1, \dots, X_m$. Since $a^\omega \in L_\nu$, we know that $\varphi$ is satisfied by an interpretation of the free variables $\bar{X}$, and that this interpretation can be encoded by an $\omega$-word $w$ over the alphabet $\{a\} \times \{0, 1\}^m$. By Büchi's result (or, equally, by Theorem 13), we can assume, again without loss of generality, that $w$ is ultimately periodic, namely, of the form $uv^\omega$, for some finite words $u, v$. By the indistinguishability result in $(\star)$, we know that $\varphi$ is also satisfied by $uv^\omega (v^{\omega*} v^\omega)^\eta$. It follows that $a^\omega (a^{\omega*} a^\omega)^\eta$ is a model of $\psi$. However, the latter word does not belong to $L_\nu$, and this contradicts the fact that $\psi$ defines $L_\nu$. $\square$

## 6.2 Definability with the cuts at the background

In [GR00] Gurevich and Rabinovich raised and left open the following question: given any MSO formula $\varphi(X_1, \dots, X_m)$, does there exist another MSO formula $\tilde{\varphi}(X_1, \dots, X_m)$ such that, for all sets of rational numbers $A_1, \dots, A_m$,

$$ (\mathbb{R}, <) \models \varphi(A_1, \dots, A_m) \quad \text{iff} \quad (\mathbb{Q}, <) \models \tilde{\varphi}(A_1, \dots, A_m) \quad ? $$

In other words, they considered question of whether the ability to use all points of the real line does give more expressive power for stating properties of predicates over the rational line – Gurevich and Rabinovich use the suggestive terminology that the formula $\varphi$ has access to the reals ‘at the background’. Note that here we implicitly use the fact that there is a fixed natural embedding of $(\mathbb{Q}, <)$ into $(\mathbb{R}, <)$.

Gurevich and Rabinovich answered positively the analogous question where the rational line is replaced by the order of the natural numbers:

**Theorem 39 ([GR00]).** For every MSO formula $\varphi(X_1, \dots, X_m)$, there is an MSO formula $\tilde{\varphi}(X_1, \dots, X_m)$ such that, for all sets $A_1, \dots, A_m \subseteq \mathbb{N}$,

$$ (\mathbb{R}, <) \models \varphi(A_1, \dots, A_m) \quad \text{iff} \quad (\mathbb{N}, <) \models \tilde{\varphi}(A_1, \dots, A_m). $$

We will not enter the details of this result, which is superseded by what follows. However, already in this case an interesting phenomenon occurs: the existence of the formula $\tilde{\varphi}$ is inherently non-effective, and this holds even if $\tilde{\varphi}$ is allowed to use extra predicates with a decidable MSO theory:
**Theorem 40 ([GR00]).** Let $\bar{B} = B_1, \dots, B_n \subseteq \mathbb{N}$ be a tuple of monadic predicates such that $(\mathbb{N},<, \bar{B})$ has a decidable MSO theory. There is no algorithm that transforms an MSO formula $\varphi(X_1, \dots, X_m)$ to an MSO formula $\tilde{\varphi}(X_1, \dots, X_m)$ such that

$$(\mathbb{R}, <) \models \varphi(A_1, \dots, A_m) \quad \text{iff} \quad (\mathbb{N}, <, \bar{B}) \models \tilde{\varphi}(A_1, \dots, A_m).$$

*Proof.* Assume that such an algorithm exists, and consider a generic MSO sentence $\varphi$. We can apply the algorithm to $\varphi$ to obtain a sentence $\tilde{\varphi}$ such that $(\mathbb{R}, <) \models \varphi$ iff $(\mathbb{N}, <, \bar{B}) \models \tilde{\varphi}$. Since the MSO theory of $(\mathbb{N}, <, \bar{B})$ is decidable, we could decide the MSO theory of $(\mathbb{R}, <)$. However, in [She75, GS82] it has been shown that MSO theory of the real line is undecidable. □

Despite the inherent difficulty due to the non-effectiveness of the transformation, we are able to answer positively the question raised by Gurevich and Rabinovich.

We begin by describing more precisely the relationship between the rational line and the real line. In fact, for technical reasons, it is convenient to work, rather than on the real line, on a larger structure that is obtained by completing the rational line with all Dedekind cuts.

**Definition 41.** A (Dedekind) cut of a linear ordering $\alpha$ is a subset $E$ of $\alpha$ such that $\alpha|_E$ is a prefix of $\alpha$.

The cuts of $\alpha$ are naturally ordered by the containment relation, that is, for all cuts $E, F$, we have $E < F$ iff $E \not\subset F$. A cut is *extremal* if it is empty or contains all elements of the linear order $\alpha$. Cuts can also be compared with the elements of $\alpha$ as follows: for all $x \in \alpha$ and all cuts $E$ of $\alpha$, we have $x < E$ (resp., $E < x$) iff $x \in E$ (resp., $x \notin E$). Note that every element $x$ of $\alpha$ has two adjacent cuts: $x^- = \{y \in \alpha | y < x\}$ and $x^+ = \{y \in \alpha | y \le x\}$. Cuts that are not of the form $x^-$ or $x^+$ are called *natural*.

**Definition 42.** The completion of a linear order $\alpha$, denoted $\hat{\alpha}$, is obtained from the disjoint union of the elements of $\alpha$ and the non-extremal cuts of $\alpha$, and it is equipped with the extended ordering defined above.

Note that the real line is obtained from the rational line using a similar notion of completion that only adds the non-extremal *natural* cuts. However, the difference between the real line and the completion, as defined above, of the rational line is negligible, especially as far as MSO definability of rational sets is concerned. In particular, since the natural cuts in $\hat{Q}$ are definable by first-order formulas, one can easily transform any MSO formula $\varphi(X_1, \dots, X_m)$ to an MSO formula $\varphi'(X_1, \dots, X_m)$ such that, for all sets $A_1, \dots, A_m \subseteq \mathbb{Q}$, $(\mathbb{R}, <) \models \varphi(A_1, \dots, A_m)$ iff $(\hat{Q}, <) \models \varphi'(A_1, \dots, A_m)$. As a consequence, to answer the question raised by Gurevich and Rabinovich, it is sufficient to prove the following result:

**Theorem 43.** For every MSO formula $\varphi(X_1, \dots, X_m)$, there is an MSO formula $\tilde{\varphi}(X_1, \dots, X_m)$ such that, for all countable linear orderings $\alpha$ and all sets $A_1, \dots, A_m \subseteq \alpha$,

$$\hat{\alpha} \models \varphi(A_1, \dots, A_m) \quad \text{iff} \quad \alpha \models \tilde{\varphi}(A_1, \dots, A_m).$$
Next, we generalize the notion of completion to words. We fix a dummy letter $c$ that is intended to label the cuts. The completion of a word $w : \alpha \to A$ is the word $\hat{w} : \hat{\alpha} \to A \uplus \{c\}$ defined by $\hat{w}(x) = w(x)$, for all elements $x \in \alpha$, and $\hat{w}(E) = c$ for all cuts $E \in \hat{\alpha} \setminus \alpha$.

A simple, yet important, property is the relationship between the operation of completion of a word and that of product of words, which is formalized in the following lemma (proof omitted). Intuitively, the completion of the product of a series of words is equivalent to a variant of the product on the completions of the words, where the variant of the product 'fills the missing cuts'.

**Lemma 44.** For all linear orderings $\alpha$ and all words $(u_i)_{i \in \alpha}$, we have

$$ (\widehat{\prod_{i \in \alpha} u_i}) = \widehat{\prod_{i \in \alpha} \hat{u}_i} $$

where the product variant $\widehat{\prod}$ is defined by $\widehat{\prod}_{i \in \alpha} \hat{v}_i = \prod_{i \in \hat{\alpha}} v'_i$, with $v'_i = v_i$ if $i \in \alpha$ and $v'_i = c$ if $i \in \hat{\alpha} \setminus \alpha$.

A language $L$ of countable words is said to be *MSO definable with the cuts at the background* if there exists an MSO sentence $\varphi$ such that $u \in L$ iff $\hat{u} \models \varphi$. The following proposition is similar to the claim of Theorem 28 (note that here we omit the part about effectiveness).

**Proposition 45.** *Languages of countable words that are MSO definable with the cuts at the background are recognizable by $\otimes$-monoids.*

*Proof.* Recall that the proof of Theorem 28 was based on closure properties of recognizable $\otimes$-languages under boolean operations and projections, which could be easily implemented at the level of the $\otimes$-algebras. Because in this proof we do not have to deal with effectiveness, it is convenient to work directly at the level of $\otimes$-monoids. In particular, the monoids recognizing the considered languages will be defined using logical types and Shelah's composition method [She75]. We shall consider MSO formulas up to syntactic equivalence, that is, up to associativity, commutativity, idempotency, and distributivity of conjunctions and disjunctions, commutativity of conjunctions with universal quantifications and disjunctions with existential quantifications, and renamings of quantified variables. Recall that, over a fixed finite signature with only relational symbols, there exist only finitely many sentences up to syntactic equivalence.

Let $\varphi$ be an MSO sentence defining, with the cuts at the background, a language $L \subseteq A^\otimes$. Let $k$ be the *quantifier rank of* $\varphi$, that is, the maximum number of nested quantifiers in $\varphi$. Given a word $u$ of possibly uncountable domain, we define its $k$-type $\text{type}_k(u)$ as the (finite) set of all sentences of quantifier rank at most $k$. We recall a simplified version of the composition theorem of Shelah, which shows that the type of a product of words is uniquely determined by the types of the words:

**Claim 1 (Shelah's composition theorem [She75].)** Let $\alpha$ be a (possibly uncountable) linear ordering and, for every $i \in \alpha$, let $u_i, v_i$ be words (of possibly uncountable
domains). We have

$$ \forall i \in \alpha \quad \mathrm{type}_k(u_i) = \mathrm{type}_k(v_i) \quad \text{implies} \quad \mathrm{type}_k\left(\prod_{i \in \alpha} u_i\right) = \mathrm{type}_k\left(\prod_{i \in \alpha} v_i\right). $$

To show that $L$ is recognizable, we need to construct a $\otimes$-monoid $(M, \pi)$ and a morphism $h$ from $A$ to $M$ such that $L = h^{-1}(h(L))$. For this, we define the function $\mathrm{type}_k^\wedge$ that maps any countable word to the $k$-type of its completion, that is, $\mathrm{type}_k^\wedge(w) = \mathrm{type}_k(\hat{w})$. The domain $M$ of the $\otimes$-monoid is precisely the range of the function $\mathrm{type}_k^\wedge$, that is,

$$ M =^{\mathrm{def}} \{\mathrm{type}_k^\wedge(w) \mid w \in A^{\otimes}\}. $$

We further let word be a function that maps any element $m \in M$ to a word $\mathrm{word}(m) \in A^{\otimes}$ such that $\mathrm{type}_k^\wedge(\mathrm{word}(m)) = m$. The product $\pi$ of the $\otimes$-monoid is defined as follows:

$$ \pi(\prod_{i \in \alpha} m_i) =^{\mathrm{def}} \mathrm{type}_k^\wedge(\prod_{i \in \alpha} \mathrm{word}(m_i)). $$

Even if we do not know yet that $\pi$ is a product (e.g., that it satisfies generalized associativity), we can easily verify that the function $\mathrm{type}_k^\wedge$ behaves like a morphism. Formally, for all countable linear orderings $\alpha$ and all words $u_i \in A^{\otimes}$, we have:

$$ \begin{align*} \mathrm{type}_k^\wedge(\prod_{i \in \alpha} u_i) &= \mathrm{type}_k(\widehat{\prod_{i \in \alpha} u_i}) \quad (\text{by definition of } \mathrm{type}_k^\wedge) \\ &= \mathrm{type}_k(\widehat{\prod_{i \in \alpha} \hat{u}_i}) \quad (\text{by Lemma 44}) \\ &= \mathrm{type}_k(\widehat{\prod_{i \in \alpha} \widehat{\mathrm{word}(\mathrm{type}_k^\wedge(u_i))}}) \quad (\text{by Claim 1}) \\ &= \mathrm{type}_k^\wedge(\prod_{i \in \alpha} \mathrm{word}(\mathrm{type}_k^\wedge(u_i))) \quad (\text{by Lemma 44}) \\ &= \pi(\prod_{i \in \alpha} u_i) \quad (\text{by definition of } \pi) \end{align*} $$

Moreover, since $\mathrm{type}_k^\wedge$ is surjective from $A^{\otimes}$ to $M$, the property of being a $\otimes$-monoid is transferred from $(A^{\otimes}, \prod)$ to $(M, \pi)$. Hence, $(M, \pi)$ is a $\otimes$-monoid. Finally, if we let $h = \mathrm{type}_k^\wedge$ and we consider two words $u, v \in A^{\otimes}$ such that $h(u) = u(v)$, we get $u \in L$ iff $\hat{u} = \varphi$ iff $\varphi \in \mathrm{type}_k^\wedge(u) = h(u)$ iff $\varphi \in \mathrm{type}_k^\wedge(v)$ iff $v \in L$. This shows that $L$ is recognized by the $\otimes$-monoid $(M, \pi)$ via the morphism $h = \mathrm{type}_k^\wedge$. $\square$

Proposition 45 combined with Theorem 31 shows that the languages definable in MSO logic with the cuts at the background are also definable in classical MSO logic:

**Corollary 46.** *Languages of countable words that are MSO definable with the cuts at the background are MSO definable.*

Finally, if we restate the above corollary in terms of relational structures, we get precisely the claim of Theorem 43.
## 6.3 Yields of tree languages

We conclude the section by considering another open problem related to countable words. More precisely, we will consider yields of trees, that is, words spelled out by frontiers of trees following the natural left-to-right order [Cou78, BCS09].<fnref n="3" /> We restrict ourselves to labelled binary trees, namely, trees in which every node has an associated label from a finite alphabet and every internal node has exactly two (ordered) successors. These trees may contain leaves as well as infinite paths.

**Definition 47.** The yield of a tree $t$ is the word $yield(t)$ whose domain is the set of leaves of $t$, ordered by the infix relation, such that $yield(t)(x) = t(x)$ for all leaves $x$.

Given two trees $t, t'$ and a set $X$ of leaves of $t$, we denote by $t[X/t']$ the tree resulting from the simultaneous substitution in $t$ of all leaves $x \in X$ by $t'$. This substitution operation is compatible with the analogous operation of substitution on yields, that is, for all $X \subseteq \text{dom}(yield(t))$, we have

$$ yield(t[X/t']) = yield(t)[X/yield(t')] $$

By a slight abuse of notation, given a letter $a$ occurring at some leaves of $t$, we denote by $t[a/t']$ the result of the simultaneous substitution in $t$ of all $a$-labelled leaves by $t'$, and similarly for $yield(t)[a/yield(t')]$.

Every word of countable domain can be seen as the yield of some tree. Indeed, this holds trivially for every word indexed over the rationals. Moreover, every word $w$ of countable domain can be obtained from a word $w'$ over the rationals by removing some positions. This latter operation of removing positions can be implemented at the level of trees by a substitution: if $w = yield(t)$ and $X \subseteq \text{dom}(w)$, then $w[X/\varepsilon] = yield(t[X/t_\varepsilon])$, where $t_\varepsilon$ is the infinite complete binary tree, whose yield is the empty word.

We can also extend the yield function to any language $T$ of trees by letting $yield(T) = \{yield(t) | t \in T\}$. Similarly, given a language $L$ of words, we define the corresponding tree language as $yield^{-1}(L) = \{t | yield(t) \in L\}$. We say that a tree language $T$ is *yield-invariant* if, for all trees $t, t'$ such that $yield(t) = yield(t')$, we have $t \in T$ iff $t' \in T$ (or, equally, if $T = yield^{-1}(yield(T))$).

It is known (see, for instance, [Tha67]) that the yield of a regular language $T$ of finite trees is a context-free language, and in general it is not regular. However, when the regular tree language $T$ is also yield-invariant, the yield language $yield(T)$ is shown to be regular [GS97]. A converse result also holds: if $L$ is a regular language of finite words, then $T = yield^{-1}(L)$ is yield-invariant and regular. The work [BCS09] raises the natural question of whether analogous properties hold between languages of possibly infinite trees and languages of words of countable domains. Below, we answer positively to this question by exploiting again the correspondence between MSO logic and $\mathfrak{B}$-algebras.

<footnote n="3">³We remark that a different notion of yield was introduced in [DT86], based on a specific continuous function that maps trees to finite or $\omega$-words.</footnote>
**Theorem 48.** Let $L$ be a language of countable words and let $T = \text{yield}^{-1}(L)$ be the corresponding yield-invariant language of trees. Then, $L$ is MSO definable iff $T$ is MSO definable.

The proof of the left-to-right direction is straightforward: if $L$ is defined by an MSO sentence $\varphi$, then we can construct another MSO sentence $\varphi'$ that, when interpreted on a tree, checks that the frontier satisfies $\varphi$; the sentence $\varphi'$ defines precisely the language $T = \text{yield}^{-1}(L)$.

The proof of the converse direction is not immediate, since, a priori, checking whether a given word $w$ belongs to $L$ requires guessing some tree $t \in T$ such that $\text{yield}(t) = w$. To show that $L$ is recognizable by $\oplus$-monoids, and hence definable in MSO logic, we will construct a $\oplus$-algebra on the basis of a suitable congruence defined from $T$.

**Definition 49.** Let $T$ be a tree language over the alphabet $A$ and let $c \notin A$ be a fresh letter that will be used as a placeholder for substitution. We denote by $\cong_T$ the equivalence on trees defined by $t_1 \cong_T t_2$ iff, for all trees $t$ labelled over the alphabet $A \uplus \{c\}$, we have $t[c/t_1] \in L \leftrightarrow t[c/t_2] \in L$. We say that a tree $t_1$ inhabits a $\cong_T$-equivalence class $[t_2]_{\cong_T} = t_1$ if $t_1 \cong_T t_2$.

We now show some simple but fundamental properties of the relation $\cong_T$. The first property is that $\cong_T$ correctly abstracts trees with the same yield, provided that the language $T$ is yield-invariant. Formally, if $T$ is yield-invariant and $t_1$ and $t_2$ are two trees such that $\text{yield}(t_1) = \text{yield}(t_2)$, then we have $t_1 \cong_T t_2$. It is also easy to verify that $\cong_T$ is a congruence with respect to the substitution operation, that is, $t_1 \cong_T t_2$ implies $t[c/t_1]_{\cong_T} = t[c/t_2]$.

Another crucial property that is used to prove Theorem 48 is based on Rabin's tree theorem [Rab69], which shows that MSO definable tree languages can be equivalently described by means of automata. Below, we recall some basic knowledge about tree automata, their problems, and the translation from MSO logic. We begin by introducing a variant of parity tree automaton that can parse trees containing leaves and/or infinite paths:

**Definition 50.** A parity tree automaton is a tuple $\mathcal{A} = (A, Q, I, \Delta, \Omega)$, where $A$ is a finite set of node labels, $Q$ is a finite set of states, $I \subseteq Q$ is a set of initial states, $\Delta \subseteq (Q \times A) \uplus (Q \times A \times Q \times Q)$ is a set of transition rules, and $\Omega: Q \to \mathbb{N}$ is a priority function. A successful run of $\mathcal{A}$ on a tree $t$ is a tree $\rho$ that has the same domain as $t$ and satisfies:

* $\rho(x_0) \in I$, where $x_0$ is the root of $\rho$;

* for all leaves $x$ of $\rho$, $(\rho(x), t(x)) \in \Delta$;

* for all internal nodes $x$ of $\rho$, $(\rho(x), t(x), \rho(x_1), \rho(x_2)) \in \Delta$, where $x_1$ and $x_2$ are the left and right successors of $x$, respectively;

* for all infinite paths $\pi$ in $\rho$, $\limsup (\Omega(\rho|_{\pi}))$ is even, where $\Omega(\rho|_{\pi})$ denotes the sequence of priorities associated with the states along the path $\pi$ and $\limsup (\Omega(\rho|_{\pi}))$ returns the maximal priority that occurs infinitely often in the sequence $\Omega(\rho|_{\pi})$.
The language recognized by A is the set $\mathcal{L}(A)$ of all trees $t$ that admit a successful run of A.

We recall that the emptiness problem for parity tree automata, that is, the problem of testing whether $\mathcal{L}(A) = \emptyset$ for any given parity tree automaton $A$, is decidable. The containment and equivalence problems can be reduced to the emptiness problem by exploiting effective closures of automata under intersection and complementation: indeed, we have $\mathcal{L}(A) \subseteq \mathcal{L}(A')$ iff $\mathcal{L}(A) \cap \mathcal{L}(A') = \emptyset$, where $A'$ denotes the automaton recognizing the complement of the language $\mathcal{L}(A')$. There is another fundamental problem that is known to be decidable, called membership problem. This amounts at testing whether a given tree $t$ belongs to the language recognized by a given parity tree automaton $A$. For this problem to make sense, however, we need to specify how the tree $t$ is provided in input. A simple solution is to restrict to regular trees, that is, trees that contain only finitely many non-isomorphic subtrees. It is easy to see that any regular tree can be finitely represented by a parity tree automaton $B$ that recognizes the singleton language $\{t\}$. The closure of parity tree automata under intersection implies that the membership problem is decidable: for every regular tree $t$ represented by the singleton language $\mathcal{L}(B) = \{t\}$, we have $t \in \mathcal{L}(A)$ iff $\mathcal{L}(B) \cap \mathcal{L}(A) \neq \emptyset$.

We recall below the correspondence between MSO sentences interpreted on trees and parity tree automata. A proof of this correspondence can be found in [Tho97] and is based on closure properties of parity tree automata under boolean operations and projections (originally, this was established by Rabin in [Rab69] using a different model of automaton).

**Theorem 51** (Translation of MSO to tree automata [Tho97]). One can effectively translate any MSO sentence $\varphi$ that defines a tree language $T$ into a parity tree automaton $A$ that recognizes $T$.

We are now ready to prove the following key lemma:

**Lemma 52.** For every MSO definable tree language $T$, $\cong_T$ has finite index, namely, there exist only finitely many $\cong_T$-equivalence classes. Moreover, given an MSO sentence defining $T$, one can decide whether $t_1 \cong_T t_2$, for any pair of regular trees $t_1$ and $t_2$, and one can compute a finite set of regular trees that inhabit all $\cong_T$-equivalence classes.

*Proof.* Let $\varphi$ be an MSO sentence defining the tree language $T$ and let $A = (A, Q, I, \Delta, \Omega)$ be the corresponding parity tree automaton recognizing $T$, obtained from Theorem 51. Given a generic tree $t$, we abstract the behaviour of $A$ on $t$ by introducing the $A$-type of $t$, defined as

$$ \text{type}_A(t) =^{\text{def}} \{q \in Q \mid t \in \mathcal{L}(A^q)\} $$

where $A^q$ is the automaton obtained from $A$ by replacing the set $I$ of initial states with the singleton $\{q\}$. Note that there are at most $2^{|Q|}$ different $A$-types of trees. Based on this, we can establish the first claim of the lemma by simply showing that the type-equivalence induced by $A$ refines the $\cong_T$-equivalence, namely, that for all trees $t_1$ and $t_2$, $\text{type}_A(t_1) = \text{type}_A(t_2)$ implies $t_1 \cong_T t_2$. Consider two trees
$t_1, t_2$ such that $\text{type}_A(t_1) = \text{type}_A(t_2)$ and another tree $t$ labelled over the extended alphabet $A \uplus \{c\}$.

We first prove that $\mathcal{A}$-types are compatible with tree substitutions, that is, knowing that $\text{type}_A(t_1) = \text{type}_A(t_2)$, we get

$$ \text{type}_{\mathcal{A}}(t[c/t_1]) = \text{type}_{\mathcal{A}}(t[c/t_2]). $$

Consider a state $q \in \text{type}_A(t[c/t_1])$, namely, such that $t[c/t_1] \in \mathcal{L}(\mathcal{A}^q)$. Let $\rho$ be a successful run of $\mathcal{A}^q$ on $t[c/t_1]$ and let $X$ be the set of $c$-labelled leaves of $t$. The set $X$ can be equally seen as a set of nodes of $\rho$. We partition $X$ into some subsets $X_{q'}$, where $q' \in Q$ and $X_{q'} = \{x \in X \mid \rho(x) = q'\}$, and for every $x \in X_{q'}$, we let $\rho_x$ be the subtree of $\rho$ starting at node $x$. Note that each subrun $\rho_x$, with $x \in X_{q'}$, is a successful run of the automaton $\mathcal{A}^{q'}$ on the tree $t_1$. This means that $q' \in \text{type}_A(t_1)$ for all non-empty sets $X_{q'}$. Since $\text{type}_A(t_1) = \text{type}_A(t_2)$, we derive that $q' \in \text{type}_A(t_2)$ for all non-empty sets $X_{q'}$. Thus, there exist successful runs $\rho'_x$ of $\mathcal{A}^{q'}$ on $t_2$, for all $x \in X_{q'}$. Next, we define the tree $\rho'$ by substituting in $\rho$ every subtree $\rho_x$ starting at node $x \in X$ with the tree $\rho'_x$ (note that the substitution is performed simultaneously on nodes that may not be leaves, but these nodes are still pairwise incomparable with respect to the descendant relation). Since $\rho(x) = \rho'(x)$ for all $x \in X$, we deduce that $\rho'$ is a successful run of $\mathcal{A}^q$ on $t[c/t_2]$. This proves that $q \in \text{type}_A(t[c/t_2])$. Symmetric arguments show that $q \in \text{type}_A(t[c/t_2])$ implies $q \in \text{type}_A(t[c/t_1])$.

Now that we know that $\text{type}_A(t[c/t_1]) = \text{type}_A(t[c/t_2])$, we can conclude the proof of the first claim by observing that

$t[c/t_1] \in L \text{ iff } \text{type}_A(t[c/t_1]) \cap I \neq \emptyset \text{ iff } \text{type}_A(t[c/t_2]) \cap I \neq \emptyset \text{ iff } t[c/t_2] \in L$ and hence $t_1 \cong_T t_2$. This shows that $\cong_T$ has finite index.

We turn to the proof of the second claim. Consider two regular trees $t_1$ and $t_2$ represented by singleton languages $\mathcal{L}(\mathcal{B}_1) = \{t_1\}$ and $\mathcal{L}(\mathcal{B}_2) = \{t_2\}$, respectively. Recall that $t_1 \cong_T t_2$ iff for all trees $t$ labelled over $A \uplus \{c\}$, either both trees $t[c/t_1]$ and $t[c/t_2]$ are inside $\mathcal{L}(\mathcal{A})$, or neither of them are. Further note that $t[c/t_i] \in \mathcal{L}(\mathcal{A})$ iff there is a state $q \in Q$ such that $t_i \in \mathcal{L}(\mathcal{A}^q)$ and $t \in \mathcal{L}(\mathcal{A}_q)$, where $\mathcal{A}_q$ is the automaton obtained from $\mathcal{A}$ by replacing the transition relation $\Delta$ with

$$ \Delta_q =^{\text{def}} (\Delta \cap (Q \times A \times Q \times Q)) \uplus (\Delta \cap (Q \times (A \setminus \{c\}))) \uplus (\{q, c\}) $$

(intuitively, $\mathcal{A}_q$ behaves exactly as $\mathcal{A}$ on all nodes of the tree $t$, with the only exception of the $c$-labelled leaves, which must be associated with state $q$). Using the above properties, we can restate the equivalence $t_1 \cong_T t_2$ as a (decidable) boolean
combination of emptiness problems:

$$
\begin{align*}
t_1 \cong_T t_2 \quad \text{iff} \quad & \bigwedge_{q \in Q} \bigvee_{q' \in Q} \left( \underbrace{B_1 \cap A^q \neq \emptyset}_{t_1 \in A^q} \wedge \underbrace{A_q \cap A_{q'} \neq \emptyset}_{\exists t \in A_q \cap A_{q'}} \wedge \underbrace{B_2 \cap A^{q'} \neq \emptyset}_{t_2 \in A^{q'}} \right) \\
& \wedge \bigwedge_{q' \in Q} \bigvee_{q \in Q} \left( \underbrace{B_1 \cap A^q \neq \emptyset}_{t_1 \in A^q} \wedge \underbrace{A_q \cap A_{q'} \neq \emptyset}_{\exists t \in A_q \cap A_{q'}} \wedge \underbrace{B_2 \cap A^{q'} \neq \emptyset}_{t_2 \in A^{q'}} \right) \\
& \wedge \bigvee_{q \in Q} \bigwedge_{q' \in Q} \left( \underbrace{B_1 \cap A^q = \emptyset}_{t_1 \notin A^q} \wedge \underbrace{B_2 \cap A^{q'} = \emptyset}_{t_2 \notin A^{q'}} \right) \vee \left( \underbrace{A_q \cup A_{q'} = \emptyset}_{\exists t \in A_q \cap A_{q'}} \wedge \right) \\
& \wedge \bigvee_{q' \in Q} \bigwedge_{q \in Q} \left( \underbrace{B_1 \cap A^q = \emptyset}_{t_1 \notin A^q} \wedge \underbrace{B_2 \cap A^{q'} = \emptyset}_{t_2 \notin A^{q'}} \right) \vee \left( \underbrace{A_q \cup A_{q'} = \emptyset}_{\exists t \in A_q \cap A_{q'}} \wedge \right).
\end{align*}
$$

(for simplicity, we identified automata and the recognized languages).

Finally, to compute a set of regular trees that inhabit all $\cong_T$-equivalence classes, we consider again $\mathcal{A}$-types. We first show how to associate with each $\mathcal{A}$-type $\sigma$ a corresponding regular tree $t_\sigma$ such that $\text{type}_\mathcal{A}(t_\sigma) = \sigma$. We do so by solving a series of emptiness problems. Indeed, we recall that an $\mathcal{A}$-type is any set $\sigma$ of states of $\mathcal{A}$ such that the language $\bigcap_{q \in \sigma} \mathcal{L}(\mathcal{A}^q) \cap \bigcap_{q \notin \sigma} \mathcal{L}(\overline{\mathcal{A}^q})$ is non-empty. Moreover, if the latter language is non-empty, then it contains a regular tree $t_\sigma$ that can be effectively constructed from $\sigma$. Clearly, we have $\text{type}_\mathcal{A}(t_\sigma) = \sigma$ and hence $t_\sigma$ can be used as a representant of the $\mathcal{A}$-type $\sigma$. Towards a conclusion, we can construct a list of regular trees $t_1, \dots, t_n$, one for each $\mathcal{A}$-type. Since the equivalence $\cong_T$ is refined by the type-equivalence induced by $\mathcal{A}$, we know that every $\cong_T$-equivalence class is inhabited by at least one tree among $t_1, \dots, t_n$. If needed, we can also exploit the decidability of $\cong_T$ to select a minimal subsequence $t_{i_1}, \dots, t_{i_m}$ of regular inhabitants of all $\cong_T$-equivalence classes. $\square$

We can now prove the right-to-left direction of Theorem 48. Let $T$ be a yield-invariant language defined by an MSO sentence $\varphi$. We will exploit Lemma 52 and the fact that $\cong_T$ is a yield-invariant equivalence compatible with tree substitutions to construct a $\otimes$-algebra $(M, 1, \cdot, \tau, \tau^*, \kappa)$ recognizing the language $L = \text{yield}(T)$. Formally, we define $M$ to be the set of all $\cong_T$-equivalence classes. We recall that this set is finite and that $\cong_T$-equivalence classes can be effectively manipulated through their *regular inhabitants*, that is, by means of *representants* that have the form of regular trees. We define the operators of the algebra as follows:

* $1$ is the $\cong_T$-equivalence class of the infinite complete tree $t_\epsilon$. Note that this tree $t_\epsilon$ has no leaves, and hence its yield is the empty word. Moreover, $t_\epsilon$ is regular, and hence it can be used as a regular inhabitant of its $\cong_T$-equivalence class.

* $\cdot$ is the function that maps any pair of $\cong_T$-equivalence classes $[t_1]\cong_T$ and $[t_2]\cong_T$ to the $\cong_T$-equivalence class

$$[t_1]\cong_T \cdot [t_2]\cong_T =^{\text{def}} [t_{a_1 a_2}[a_1/t_1][a_1/t_2]]\cong_T$$
where $t_{a_1a_2}$ is a fixed tree such that $\text{yield}(t) = a_1a_2$, and $a_1, a_2$ are distinct fresh letters not occurring in the alphabet of $t_1$ and $t_2$. For example, $t_{a_1a_2}$ can be chosen to be the tree

$$t_{a_1a_2} = \begin{smallmatrix} \bullet \\ a_1 \\ \cdot \\ a_2 \end{smallmatrix}$$

where the label $\bullet$ of the root is immaterial. Note that the $\cong_T$-equivalence class $[t_1]\cong_T \cdot [t_2]\cong_T$ is well defined thanks to the fact that $\cong_T$ is a congruence. Moreover, because the tree $t_{a_1a_2}$ is regular, a regular inhabitant of the class $[t_1]\cong_T \cdot [t_2]\cong_T$ can be effectively constructed from some regular inhabitants of $[t_1]\cong_T$ and $[t_2]\cong_T$.

* $\tau$ is the function that maps any $\cong_T$-equivalence class $[t_1]\cong_T$ to the $\cong_T$-equivalence class

$$[t_1]\cong_T =^{\text{def}} [t_\omega[a/t_1]]\cong_T$$

$$\text{where } t_\omega = \begin{smallmatrix} \bullet \\ a \\ \cdot \\ a \\ \vdots \\ a \end{smallmatrix}$$

Again, since $t_\omega$ is a regular tree, a regular inhabitant of the class $[t_1]\cong_T$ can be computed from a regular inhabitant of the class $[t_1]\cong_T$.

* $\tau^*$ is defined similarly to $\tau$, where $t_\omega$ is replaced by the tree

$$t_{\omega^*} = \begin{smallmatrix} \bullet \\ \cdot \\ \bullet \\ \cdot \\ \vdots \\ \bullet \\ a \\ \cdot \\ \cdot \\ \vdots \\ a \end{smallmatrix}$$

* $\kappa$ is the function that maps any set $\{[t_1]\cong_T, \dots, [t_k]\cong_T\}$ of $\cong_T$-equivalence classes to the $\cong_T$-equivalence class

$$\{[t_1]\cong_T, \dots, [t_k]\cong_T\}^{\kappa} =^{\text{def}} [t_\eta[a_1/t_1]\dots[a_k/t_k]]\cong_T$$

where $t_\eta$ is a fixed regular tree with $\text{yield}\{a_1, \dots, a_k\}^\eta$ and $a_1, \dots, a_k$ are fresh letters. For example, $t_\eta$ can be defined by a parity tree automaton so as to satisfy the following equation:

$$t_\eta = \begin{smallmatrix} \bullet \\ t_\eta \\ \cdot \\ a_1 \\ \cdot \\ t_\eta \\ \vdots \\ t_\eta \\ \cdot \\ \cdot \\ \vdots \\ t_\eta \\ \cdot \\ \cdot \\ \vdots \\ a_k \\ \cdot \\ \cdot \\ t_\eta \end{smallmatrix}$$
Below, we verify that the structure $(M, 1, \cdot, \tau, \tau^*, \kappa)$ obtained from the automaton $\mathcal{A}$ is indeed a $\otimes$-algebra, that is, it satisfies Axioms A1-A5 of Definition 2.

**Lemma 53.** The structure $(M, 1, \cdot, \tau, \tau^*, \kappa)$ obtained from $\cong_T$ is a $\otimes$-algebra.

*Proof.* The fact that the structure $(M, 1, \cdot, \tau, \tau^*, \kappa)$ satisfies Axioms A1-A5 follows almost directly from its definition and from the fact that the equivalence $\cong_T$ is yield-invariant, that is, $t_1 \cong_T t_2$ whenever $yield(t_1) = yield(t_2)$. For example, recall the definition of the binary operator $\cdot$: for all pairs of trees $t_1, t_2$, we have

$$[t_1]_{\cong_T} \cdot [t_2]_{\cong_T} = \left[ \begin{smallmatrix} \bullet \\ t_1 \\ \cdot \\ t_2 \end{smallmatrix} \right]_{\cong_T}.$$

From this, we easily deduce that $\cdot$ satisfies Axiom A1:

$$([t_1]_{\cong_T} \cdot [t_2]_{\cong_T}) \cdot [t_3]_{\cong_T} = \left[ \begin{smallmatrix} \bullet \\ t_1 \\ \cdot \\ t_2 \\ \cdot \\ t_3 \end{smallmatrix} \right]_{\cong_T} \quad \text{(by definition)}$$

$$= \left[ \begin{smallmatrix} \bullet \\ t_1 \\ \cdot \\ t_2 \\ \cdot \\ t_3 \end{smallmatrix} \right]_{\cong_T} \quad \text{(by yield-invariance)}$$

$$= [t_1]_{\cong_T} \cdot ([t_2]_{\cong_T} \cdot [t_3]_{\cong_T}). \quad \text{(by definition)}$$

We omit the analogous arguments showing that $1, \tau, \tau^*$, and $\kappa$ satisfy the remaining Axioms A2-A5. $\square$

Combining the above lemma, Corollary 12, and Theorem 31 gives the right-to-left direction of Theorem 48.

We also remark that, if the MSO definable tree language $T$ is not known to be yield-invariant, we can still construct the structure $(M, 1, \cdot, \tau, \tau^*, \kappa)$ from $\cong_T$. Below, we explain how to use this structure to decide whether $T$ is yield-invariant. We follow the same approach described in Section 5 and we construct, using the operators of $(M, 1, \cdot, \tau, \tau^*, \kappa)$, a family of MSO sentences of the form $\varphi_{\sigma}^{\text{value}}$, where $\sigma$ ranges over the set of possible $\cong_T$-equivalence classes. Given a word $w$, these sentences can be used to derive the $\cong_T$-equivalence class of some tree $t_w$ such that $yield(t_w) = w$. In particular, we can define in MSO logic a word language of the form $L = \{w | t_w \in \mathcal{L}(\mathcal{A})\}$. We can then use the left-to-right implication of Theorem 48 to derive an MSO sentence defining the tree language $T' = yield^{-1}(L)$. Now, if $T$ is yield-invariant, then $T' = yield^{-1}(L) = yield^{-1}(yield(T)) = T$, as shown by Theorem 48. Conversely, if $T' = T$, then $T$ is clearly yield-invariant. We thus reduced the problem of deciding whether an MSO definable tree language $T$ is yield-invariant to the equivalence problem for MSO sentences interpreted on trees, which is known to be decidable.

**Theorem 54.** *The problem of deciding whether a tree language $T$ defined by an MSO sentence is yield-invariant is decidable.*
# 7 Conclusion

We have introduced an algebraic notion of recognizability for languages of countable words and we have shown the correspondence with the family of languages definable in MSO logic. As a side-product of this result, we obtained that the hierarchy of monadic quantifier alternation for MSO logic interpreted over countable words collapses to its $∃∀$-fragment (or, equally, to its $∀∃$-fragment). The collapse result is optimal in the sense that there are recognizable languages that are not definable in the $∃$-fragment. Our techniques are then used to solve an open problem posed by Gurevich and Rabinovich, concerning the definability of properties of sets of rationals using MSO formulas interpreted over the real line (definability with the cuts at the background). Finally, we exploited the correspondence between logic and algebras to solve another open problem posed by Bruyère, Carton, and Sénizergues, concerning the characterization of properties of trees that can be defined in MSO logic and that are yield-invariant.

We conclude by mentioning the possibility of defining models of automata that extend those from [BC01] and that capture precisely the expressiveness of MSO logic over words of countable domains. However, such automata need to have complicated acceptance conditions in order to distinguish between scattered and non-scattered words and, more generally, to enjoy closure properties under boolean operations and projections. The definition of an automaton model for languages of countable words is thus not as natural as that of $\otimes$-monoid.

# References

[BBCR10] N. Bedon, A. Bès, O. Carton, and C. Rispal. Logic and Rational Languages of Words Indexed by Linear Orderings. *Theoretical Computer Science*, 46(4):737–760, 2010.

[BC01] V. Bruyère and O. Carton. Automata on Linear Orderings. In *Proceedings of the 26th International Symposium on Mathematical Foundations of Computer Science (MFCS)*, volume 2136 of LNCS, pages 236–247. Springer, 2001.

[BC07] V. Bruyère and O. Carton. Automata on linear orderings. *Journal of Computer and System Sciences*, 73(1):1–24, 2007.

[BCS09] V. Bruyère, O. Carton, and G. Sénizergues. Tree Automata and Automata on Linear Orderings. *RAIRO Theoretical Informatics and Applications*, 43:321–338, 4 2009.

[Büc64] J.R. Büchi. Transfinite automata recursions and weak second order theory of ordinals. In *Proceedings of the Int. Congress Logic, Methodology, and Philosophy of Science, Jerusalem 1964*, pages 2–23. North Holland, 1964.
[Bü62] J.R. Büchi. On a Decision Method in Restricted Second Order Arithmetic. In *Proceedings of the International Congress for Logic, Methodology and Philosophy of Science*, pages 1-11. Stanford University Press, 1962.

[CCP11] O. Carton, T. Colcombet, and G. Puppis. Regular Languages of Words Over Countable Linear Orderings. In *Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP)*, volume 6756 of LNCS, pages 125-136. Springer, 2011.

[Col10] T. Colcombet. Factorisation Forests for Infinite Words and Applications to Countable Scattered Linear Orderings. *Theoretical Computer Science*, 411:751-764, 2010.

[Col13] T. Colcombet. Composition with Algebra at the Background – On a Question by Gurevich and Rabinovich on the Monadic Theory of Linear Orderings. In *Proceedings of the 8th International Computer Science Symposium in Russia (CSR)*, volume 7913 of LNCS, pages 391-404. Springer, 2013.

[Cou78] B. Courcelle. Frontiers of Infinite Trees. *RAIRO Theoretical Informatics and Applications*, 12(4):319-337, 1978.

[DT86] M. Dauchet and E. Timmerman. Continuous Monoids and Yields of Infinite Trees. *RAIRO Theoretical Informatics and Applications*, 20(3):251-274, 1986.

[FV59] S. Feferman and R. Vaught. The First-order Properties of Products of Algebraic Systems. *Fundamenta Mathematicae*, 47:57-103, 1959.

[GR00] Y. Gurevich and A.M. Rabinovich. Definability and Undefinability with Real Order at The Background. *Journal of Symbolic Logic*, 65(2):946-958, 2000.

[GS82] Y. Gurevich and S. Shelah. Monadic Theory of Order and Topology in ZFC. *Annals of Mathematical Logic*, 23(2-3):179-198, 1982.

[GS97] F. Gécseg and M. Steinby. Tree languages. In G. Rozenberg and A. Salomaa, editors, *Handbook of Formal Languages, Vol. 3: Beyond Words*, pages 1-68. Springer, 1997.

[Hod93] Wilfrid Hodges. *Model Theory*, volume 42. Cambridge University Press, 1993.

[LJ66] H. Läuchli and J.Leonard. On the elementary theory of linear order. *Fundamenta Mathematicae*, 59(1):109-116, 1966.

[LJ68] H. Läuchli and J.Leonard. A decision procedure for the weak second order theory of linear order. In *Contributions to Mathematical Logic, Proceedings of Logic Colloquium, volume 50 of Studies in Logic and the Foundations of Mathematics*, pages 189-197. Elsevier, 1968.
[PP04] J.E. Pin and D. Perrin. *Infinite Words: automata, semigroups, logic and games*. Elsevier Science Publishers, 2004.

[Rab69] M.O. Rabin. Decidability of Second-order Theories and Automata on Infinite Trees. *Transactions of the American Mathematical Society*, 141:1-35, 1969.

[Ram29] F.P. Ramsey. On a Problem of Formal Logic. In *Proceedings of the London Mathematical Society*, volume 30, pages 264-286, 1929.

[RC05] C. Rispal and O. Carton. Complementation of Rational Sets on Countable Scattered Linear Orderings. *International Journal of Foundations of Computer Science*, 16(4):767-786, 2005.

[Ros82] J.G. Rosenberg. *Linear Orderings*. Academic Press, 1982.

[She75] S. Shelah. The Monadic Theory of Order. *Annals of Mathematics*, 102:379-419, 1975.

[Tha67] J.W. Thatcher. Characterizing Derivation Trees of Context-free Grammars Through a Generalization of Finite Automata Theory. *Journal of Computer and System Sciences*, 1(4):317-322, 1967.

[Tho93] W. Thomas. On the Ehrenfeucht-Fraïssé Game in Theoretical Computer Science. In *Theory and Practice of Software Development (TAP-SOFT)*, volume 668 of LNCS, pages 559-568. Springer, 1993.

[Tho97] W. Thomas. Languages, Automata, and Logic. In *Handbook of Formal Languages*, volume 3, pages 389-455. Springer, 1997.

[Wil93] T. Wilke. An Algebraic Theory For Regular Languages of Finite and Infinite Words. *International Journal of Algebra and Computation*, 3(4):447-489, 1993.