Pumping for ordinal-automatic structures 1

Abstract

An α-automaton (for α some ordinal) is an automaton similar to a Muller automaton that processes words of length α. A structure is called α-automatic if it can be presented by α-automata (completely analogous to the notion of automatic structures which can be presented by the well-known finite automata). We call a structure ordinal-automatic if it is α-automatic for some ordinal α. We continue the study of ordinal-automatic structures initiated by Schlicht and Stephan as well as by Finkel and Todorčević. We develop a pumping lemma for α-automata (processing finite α-words, i.e., words of length α that have one fixed letter at all but finitely many positions). Using this pumping, we provide counterparts for the class of ordinal-automatic structures to several results on automatic structures:

∙ Every finite word α-automatic structure has an injective finite word α-automatic presentation for all $α < ω_{1} + ω^{ω}$ . This bound is sharp.

∙ We classify completely the finite word $ω^{n}$ -automatic Boolean algebras. Moreover, we show that the countable atomless Boolean algebra does not have an injective finite-word ordinal-automatic presentation.

∙ We separate the class of finite-word ordinal-automatic structures from that of tree-automatic structures by showing that free term algebras with at least 2 generators (and one binary function) are not ordinal-automatic while the free term algebra with countable infinitely many generators is known to be tree-automatic.

∙ For every ordinal $α < ω_{1} + ω^{ω}$ , we provide a sharp bound on the height of the finite word α-automatic well-founded order forests.

∙ For every ordinal $α < ω_{1} + ω^{ω}$ , we provide a structure $F_{α}$ that is complete for the class of finite-word α-automatic structures with respect to first-order interpretations.

∙ As a byproduct, we also lift Schlicht and Stephans’s characterisation of the injectively finite-word α-automatic ordinals to the noninjective setting.

Keywords

Ordinal-automatic structures pumping lemma classification of Boolean algebras order forests

1. Introduction

Finite automata play a crucial role in many areas of computer science. In particular, finite automata have been used to represent certain infinite structures. The basic notion of this branch of research is the class of automatic structures (cf. [20]). A structure is automatic if its domain as well as its relations are recognised by (synchronous multi-tape) finite automata processing finite words. This class has the remarkable property that the first-order theory of any automatic structure is decidable. One goal in the theory of automatic structures is a classification of those structures that are automatic (cf. [7,19,22,23,25]). Besides finite automata reading finite or infinite words there are also finite automata reading finite or infinite trees. Using such automata as representation of structures leads to the notion of tree-automatic structures [2]. The classification of tree-automatic structures is less advanced but some results have been obtained in the last years (cf. [7,14,15]). Schlicht and Stephan [29] and Finkel and Todorčević [8] have started research on a new branch of automatic structures based on automata processing α-words where α is some ordinal. An α-word is a map $α \to Σ$ for Σ some finite alphabet. Büchi [4] already introduced an extension of finite automata, which we call α-automata, that processes α-words. If α is countable, α-automata enjoy basically all the good properties of finite automata whence structures represented by α-automata have uniformly decidable first-order theories. Strictly speaking, there are a priori several classes of structures that one could call α-automatic. As for usual words or trees, one can distinguish between injective or noninjective representations and one can decide whether the representing automata should be deterministic or nondeterministic. Moreover, the mentioned works of Schlicht and Stephan and Finkel and Todorčević even disagree on the definition on the input to an α-automata: while Finkel and Todorčević allow any α-word as input, Schlicht and Stephan only allow α-words that are labelled by a fixed symbol ◇ at all but finitely many positions (we call such words finite α-words). In this article, we focus on finite word α-automatic structures with noninjective presentations by nondeterministic ordinal-automata. If a structure is presentable in this setting, we call it $(α)$ -automatic (where $(α)$ refers to the fact that it is automatic over words from $Σ^{(α)}$ for some finite alphabet Σ). Schlicht and Stephan [29] classified the ordinals that allow injective $(α)$ -automatic presentations and provided bounds on the finite-condensation ranks of scattered linear orders that are injectively $(α)$ -automatic. Finkel and Todorčević [9,11] lifted the former result in the case of ordinals of the form $ω^{n}$ where n is a natural number to the infinite word setting: an ordinal is (infinite word) injectively $(ω^{n})$ -automatic if and only if it is finite word injectively $(ω^{n})$ -automatic if and only if it is below $ω^{ω^{n}}$ (where the latter equivalence is Schlicht and Stephan’s result).

We should also mention that Finkel and Todorčević [8,10] showed that the isomorphism problem of infinite word $ω^{n}$ -automatic Boolean Algebras is independent of the axiomatic system ZFC.

Moreover, there is a connection between automata and ordinals and monadic second-order logic in the work of Büchi and more recently Neeman [26,27].

We develop the theory of finite word α-automatic structures and obtain the following counter-parts to results from the setting of automatic structures.

Emptiness of α-automata is decidable in polynomial time.

For $α < ω_{1} + ω^{ω}$ (where $ω_{1}$ denotes the first uncountable ordinal), the finite word α-automata can be determinised whence the class of languages of finite word α-automata are closed under complementation. The bound on α is strict in the sense that both results fail if $α ⩾ ω_{1} + ω^{ω}$ .

Note that the bound is rather surprising. Büchi has already pointed out that in the setting of α-automata where the input may be an infinite α-word, complementation and determinisation are only possible if $α < ω_{1}$ .

Together with the fact that there is an $(α)$ -automatic well-order of all finite α-words, the classical techniques allow to show that for each $α < ω_{1} + ω^{ω}$ , the class of $(α)$ -automatic structures coincides with the class of $(α)$ -automatic structures with injective presentations by deterministic automata.

We lift the classical Pumping Lemma to the finite word α-automata setting. This allows to adapt other techniques from the classical setting to prove limitations on the class of $(α)$ -automatic structures as follows:

We classify the $(ω^{n})$ -automatic Boolean algebras (cf. [22] for the classical word-automatic case). A Boolean algebra $B$ is $(ω^{n})$ -automatic if and only if it is isomorphic to the interval algebra $I_{α}$ for some ordinal $α < ω^{n + 1}$ . Moreover, we can show that atomless Boolean algebras are not injectively finite word $(α)$ -automatic. This contrasts the fact that the countable atomless Boolean algebra has a tree-automatic presentation.

The free (semi)-group and the free term algebras with at least two generators are not $(α)$ -automatic. This result is a stronger separation result than the previous one because it even holds for noninjective presentations. The latter is the first example of a tree-automatic structure which is not $(α)$ -automatic for any ordinal α. Since Schlicht and Stephan [29] showed that there are ordinals that are $(α)$ -automatic but not tree-automatic for all $α > ω^{ω}$ , our result completes the separation of the class of tree-automatic structures and the class of finite-word ordinal-automatic structures.

The pumping lemma also allows to lift a classical result of Blumensath [2] to this setting. There is an $(α)$ -automatic structure that is complete under first-order interpretations for the class of $(α)$ -automatic structures, i.e., there is a structure $F_{α}$ such that $F_{α}$ is $(α)$ -automatic and every $(α)$ -automatic structure $A$ is first-order interpretable in $F_{α}$ .

Exhibiting a connection between $(α)$ -automatic order trees and $(α)$ -automatic ordinals from Kartzow et al. [17] (first used by Kuske et al. [25] in the finite word case), we derive a bound on the (ordinal) height (also called the rank) of well-founded $(α)$ -automatic order forests: for each ordinal $γ < ω_{1} + ω$ , an $(ω^{γ})$ -automatic order forest has height strictly below $ω^{γ + 1}$ . We construct examples which show the bound to be strict.

We would like to thank the anonymous referees for detailed comments.

1.1. Outline of the paper

In Section 2 we briefly recall some basic facts and fix some notation. Section 3 introduces α-automata and $(α)$ -automatic structures and discusses basic properties of these concepts. For this purpose we prove two pumping lemmas for α-automata in Section 3.2. These can be seen as the most important technical contribution underlying all of our results. For instance, the basic results that emptiness of α-automata is decidable (Section 3.3) and that α-automata can be determinised if $α < ω_{1} + ω^{ω}$ (Section 3.4) rely on these pumping arguments. Section 4 then introduces structures that are complete under first-order interpretations for the class of $(α)$ -automatic structures. After this, Section 5 contains a second series of technical results. Here we lift the notion of growth lemma from the classical automatic structures setting to our setting. These results can be seen as a way of transforming the pumping lemmas into statements about $(α)$ -automatic Boolean Algebras, (semi-)groups, term algebras, etc. Sections 6 and 7 then apply the growth lemmas first to Boolean Algebras and then to free (semi-)groups and free term algebras. Finally, Section 8 contains our results on $(α)$ -automatic forests.

2. Preliminaries

In this section, we briefly recall some basic facts and fix some notation.

2.1. Ordinals

As usual, we identify an ordinal α with the set of smaller ordinals ${β ∣ β < α}$ . We say α has countable cofinality if $α = 0$ or there is a sequence ${(α_{i})}_{i \in ω}$ of ordinals such that $α = sup {α_{i} + 1 ∣ i \in ω}$ . Otherwise we say α has uncountable cofinality. We denote the first uncountable ordinal by $ω_{1}$ . Note that it is the first ordinal with uncountable cofinality.

For every ordinal α and every $n \in N$ , let $α_{\sim n}$ be the ordinal of the form $α_{\sim n} = ω^{n + 1} β$ for some ordinal β such that $\begin{matrix} α = α_{\sim n} + ω^{n} m_{n} + ω^{n - 1} m_{n - 1} + \dots + m_{0} \end{matrix}$ for some natural numbers $m_{0}, \dots, m_{n}$ .

2.2. Logics

We assume that the reader is familiar with first-order logic and its usual extensions. $FO$ denotes first-order logic. $FO (\exists^{\infty})$ is its extension by the quantifier “there are infinitely many”. Given a signature σ, the set of positive existential first-order formulas, denoted by $\exists^{*} Pos$ is the set of formulas build from the relations in σ using ∃, ∧, and ∨. Similarly, $\forall^{*} \exists^{*} Pos$ denotes the set of formulas of the form $\forall x_{1} \forall x_{2} \dots \forall x_{n} φ$ where $φ \in \exists^{*} Pos$ , and $\forall^{*} \exists^{*} {Pos}_{\neq}$ its extension where we also allow inequality as an additional binary relation.

3. Ordinal-automatic structures

First of all, we agree on the following convention: Throughout the whole article, every alphabet Σ contains a distinguished blank symbol which is denoted by $◇_{Σ}$ or, if the alphabet is clear from the context, just by ◇. Moreover, for alphabets $Σ_{1}, \dots, Σ_{r}$ , the distinguished symbol of the alphabet $Σ_{1} \times \dots \times Σ_{r}$ will always be $◇_{Σ_{1} \times \dots \times Σ_{r}} = (◇_{Σ_{1}}, \dots, ◇_{Σ_{r}})$ .

For any limit ordinal $β ⩽ α$ , A an arbitrary set and a map $w : α + 1 \to A$ we introduce the following notation for the set of images cofinal in β: $\begin{matrix} lim_{β} w : = {a \in A ∣ \forall β^{'} < β \exists β^{'} < β^{″} < β w (β^{″}) = a} . \end{matrix}$

Definition 3.1.
An $(α)$ -word (over Σ) (called a finite α-word over Σ) is a map $w : α \to Σ$ whose support, i.e. the set $\begin{matrix} supp (w) = {β \in α ∣ w (β) \neq ◇}, \end{matrix}$ is finite. The set of all $(α)$ -words over Σ is denoted by $Σ^{(α)}$ . We write $◇^{α}$ for the constantly ◇ valued word $w : α \to Σ$ , $w (β) = ◇$ for all $β < α$ , which we also call the empty input of length α.
Definition 3.2.
If $γ ⩽ δ ⩽ α$ are ordinals and $w : α \to Σ$ some $(α)$ -word, we denote by $w ↾_{[γ, δ)}$ the restriction of w to the subword between position γ (included) and δ (excluded).

3.1. Ordinal automata

Büchi [4] has already introduced automata that process $(α)$ -words. These behave like usual finite automata at successor ordinals while at limit ordinals a limit transition that resembles the acceptance condition of a Muller-automaton is used.

Definition 3.3.
An (ordinal-)automaton is a tuple $A = (S, Σ, I, F, Δ)$ where S is a finite set of states, Σ an alphabet, $I \subseteq S$ the initial and $F \subseteq S$ the final states and Δ is a subset of $(S \times Σ \times S) \cup (2^{S} \times S)$ called the transition relation.

Transitions in $S \times Σ \times S$ are called successor transitions and transitions in $2^{S} \times S$ are called limit transitions.
Definition 3.4.
A run of $A$ on the $(α)$ -word $w \in Σ^{(α)}$ is a map $r : α + 1 \to S$ such that
$(r (β), w (β), r (β + 1)) \in Δ$ for all $β < α$

$({lim}_{β} r, r (β)) \in Δ$ for all limit ordinals $β ⩽ α$ .
The run r is accepting if $r (0) \in I$ and $r (α) \in F$ . For $q, q^{'} \in S$ , we write $q \overset{w}{\underset{A}{⟶}} q^{'}$ if there is a run r of $A$ on w with $r (0) = q$ and $r (α) = q^{'}$ .

In the following, we always fix an ordinal α and then concentrate on the set of $(α)$ -words that a given ordinal automaton accepts. In order to stress this fact, we will call the ordinal-automaton an $(α)$ -automaton. Definition 3.5.
Let α be some ordinal and $A$ be an $(α)$ -automaton. The $(α)$ -language of $A$ , denoted by $L_{(α)} (A)$ , consists of all $(α)$ -words $w \in Σ^{(α)}$ which admit an accepting run of $A$ on w. Whenever α is clear from the context, we may omit the subscript α and use just $L (A)$ instead of $L_{(α)} (A)$ .

3.2. Two pumping lemmas

The pumping lemma for finite automata on finite words is perhaps one of the best known theorems in theoretical computer science. It states that a part of a long word accepted by an automaton can be repeated arbitrarily often and the word still is in the language. An analogous argument holds for $(α)$ -automata. More precisely, in each ω-copy of α we can pump within this ω-copy if the word contains a letter different from ◇ at a position far away from the minimal element of this ω-copy. Moreover, we prove a pumping lemma concerning different ω-copies. If $α ⩾ ω^{2}$ , every finite $(α)$ -word contains large subwords which are constantly labelled by ◇. We call such a subword a gap (of the support of the word). Given $α = ω^{β}$ some ordinal, if an $(α)$ -automaton with n states accepts an $(α)$ -word w with a gap of size at least $ω^{n}$ and $α > ω^{n + 1}$ then we can pump this gap to size $ω^{γ}$ for each $ω^{n} ⩽ ω^{γ} < α$ in the sense that if $w = w_{1} w_{2} w_{3}$ is accepted by the automaton where $w_{2}$ is a constant map (with value ◇) and $w_{2}$ has size $ω^{γ} < α$ then $w^{'} = w_{1} w_{2}^{'} w_{3}$ is also accepted for all words $w_{2}^{'}$ that are constant maps with value ◇ of length at least $ω^{n}$ and shorter than α. Note that $| w_{2}^{'} | < α$ implies that $w^{'}$ is still an $(α)$ -word. Note that Wojciechowski [30] also proved a lemma that is similar to the shrinking part of our pumping lemma. He proved that if there is a run r of an $(ω^{k})$ -automaton $A$ from state q to state p such that $| {lim}_{α} (r) | < k$ then there is also a run $r^{'}$ of $A$ (seen as a $(β)$ -automaton for a certain $β < ω^{k}$ ) from state q to state p on a word of length β.

As stated in Definition 3.1, we call $w : η \to {◇}$ the empty input (of length η) for each ordinal η. We first state two pumping lemmas: the first for $(α)$ -automata where α is an ordinal of countable cofinality and the second for $(α)$ -automata where α is of uncountable cofinality. Afterwards we give an example that the first pumping lemma does not hold for ordinals of uncountable cofinality. Finally, we prove both Pumping Lemmas.

Proposition 3.6 (First pumping).

Let $α ⩾ 1$ be an ordinal of countable cofinality and let $A = (S, Σ, I, F, Δ)$ be an automaton with $| S | ⩽ m$ . For all $s_{0}, s_{1} \in S$ , $\begin{array}{l} s_{0} \overset{◇^{ω^{m}}}{\underset{A}{⟶}} s_{1} ⟺ s_{0} \overset{◇^{ω^{m} α}}{\underset{A}{⟶}} s_{1} . \end{array}$

Proposition 3.7 (Second pumping).

Let $α ⩾ 1$ be an ordinal of uncountable cofinality and let $A = (S, Σ, I, F, Δ)$ be an automaton with $| S | ⩽ m$ . For all $s_{0}, s_{1} \in S$ , the following are equivalent:

$s_{0} \overset{◇^{ω^{m} α}}{\underset{A}{⟶}} s_{1}$ ,

there is a state $s^{'} \in S$ , a set $S_{lim} \subseteq S$ , a transition $(S_{lim}, s_{1})$ and runs on empty input $\begin{array}{l} r_{1} : ω^{m} + 1 \to S with r_{1} (0) = s_{0}, r_{1} (ω^{m}) = s^{'}, lim_{ω^{m}} r_{1} = S_{lim} and \\ r_{2} : ω^{m} + 1 \to S with r_{2} (0) = s^{'}, r_{2} (ω^{m}) = s^{'}, lim_{ω^{m}} r_{2} = im (r_{2}) = S_{lim}, \end{array}$ and

there is a run $r : s_{0} \overset{◇^{ω^{m + 1}}}{\underset{A}{⟶}} s_{1}$ such that ${lim}_{ω^{m} i} r = {lim}_{ω^{m + 1}} r$ for all $1 ⩽ i < ω$ .

The following example, which is copied from Wojciechowski [30], shows that Proposition 3.6 does not hold for ordinals with uncountable cofinality. The automaton used in this example is extended in Example 3.2 below to show that complementation of $(ω_{1} + ω^{ω})$ -automata is in general not possible.

Example 3.1.
Let $A = ({s_{1}, s_{2}, s_{3}}, {◇}, {s_{1}}, {s_{3}}, Δ)$ where Δ consists of
$(s_{i}, ◇, s_{j})$ for all $i, j \in {1, 2}$ ,

$({s_{1}}, s_{1})$ , $({s_{1}}, s_{2})$ , $({s_{2}}, s_{3})$ and $({s_{1}, s_{2}}, s_{3})$ .
There are runs of $A$ starting in $s_{1}$ and ending in $s_{3}$ on every word $◇^{α}$ where α is a limit ordinal of countable cofinality, but no run of $A$ from $s_{1}$ to $s_{3}$ on the empty word of length $ω_{1}$ . Fixing a sequence ${(α_{i})}_{i \in N}$ with $α_{i} < α$ and $sup {α_{i} + 1 ∣ i \in N} = α$ , a run on $◇^{α}$ is given by $\begin{matrix} r (β) = \{\begin{matrix} s_{3} & if β = α, \\ s_{2} & if β = α_{i} for some i \in N, \\ s_{1} & otherwise. \end{matrix} \end{matrix}$

Now heading for a contradiction assume that r is a run of $A$ on the empty word of length $ω_{1}$ which ends in state $s_{3}$ . Thus, $Γ = {γ < ω_{1} ∣ r (γ) = s_{2}}$ is cofinal and hence uncountable. Let $γ_{1}$ be the minimal element of Γ and $γ_{i + 1}$ the minimal element of $Γ ∖ {γ_{1}, \dots, γ_{i}}$ . $Γ_{ω} : = ⋃_{i \in ω} γ_{i}$ is a countable initial segment of Γ. Thus, state $s_{2}$ occurs cofinal at $sup (Γ_{ω}) < ω_{1}$ in r. But this implies that $r (sup (Γ_{ω})) = s_{3}$ whence there is no applicable transition from $sup (Γ_{ω})$ to $sup (Γ_{ω}) + 1$ . As desired, we have arrived at a contradiction.

The rest of this section provides proofs for both Pumping Lemmas. The proofs are lenghty because one has to deal with several case distinctions but the underlying idea of exhibiting state repetitions in a given run is the same as in the case of pumping for finite automata. The next two lemmas provide a proof of the First Pumping Proposition. Note that the condition on the cofinality of γ is only crucial for the first part, i.e., for pumping some run from $ω^{m}$ to $ω^{m} γ$ . The possibility to shrink a run from length $ω^{m} γ$ to $ω^{m}$ is independent of the cofinality of γ.
Lemma 3.8.
Let $m \in N$ , and let $γ > 0$ be some ordinal with countable cofinality. Let $A = (S, Σ, I, F, Δ)$ be an ordinal automaton. Suppose that $S_{lim} \subseteq S^{+} \subseteq S$ and $s \in S^{+}$ with $| S_{lim} | ⩽ m$ .

If there is a run $r : ω^{m} + 1 \to S$ of $A$ on empty input with $\begin{matrix} r (0) = s, lim_{ω^{m}} r = S_{lim}, and im (r) = S^{+}, \end{matrix}$ then there is a run $\bar{r} : ω^{m} γ + 1 \to S$ of $A$ on empty input with $\begin{matrix} \bar{r} (0) = s, lim_{ω^{m} γ} \bar{r} = S_{lim}, im (\bar{r}) = S^{+} and \bar{r} (ω^{m} γ) = r (ω^{m}) . \end{matrix}$
Proof.
The proof is by induction on m and $| S_{lim} |$ .
First suppose that $S_{lim} = S^{+}$ . Then $r (ω^{m}) = r (α_{0})$ for some $α_{0} < ω^{m}$ . Let $\begin{matrix} \bar{r} (δ) = \{\begin{matrix} r (δ) & if δ < ω^{m}, \\ r (α_{0} + δ^{'}) & if δ = ω^{m} β + δ^{'} with 1 ⩽ β < γ and δ^{'} < ω^{m}, \\ r (ω^{m}) & if δ = ω^{m} γ . \end{matrix} \end{matrix}$

Now suppose that $S_{lim} ⊊ S^{+}$ . Choose $n_{0} \in N$ with $r ([ω^{m - 1} n_{0}, ω^{m})) \subseteq S_{lim}$ .

If there is an $n \in N$ such that $\begin{matrix} n ⩾ n_{0} and lim_{(ω^{m - 1} (n + 1))} r = S_{lim}, \end{matrix}$ choose $β \in [ω^{m - 1} n, ω^{m - 1} (n + 1))$ with $r (β) = r (ω^{m - 1} (n + 1))$ such that $r ([β, ω^{m - 1} (n + 1))) = S_{lim}$ . Let $\begin{matrix} \bar{r} (δ) = \{\begin{matrix} r (δ) & if δ ⩽ ω^{m - 1} (n + 1), \\ r (β + δ^{'}) & if δ = ω^{m - 1} β^{'} + δ^{'} with n + 1 ⩽ β^{'} < ω γ and δ^{'} < ω^{m - 1}, \\ r (ω^{m}) & if δ = ω^{m} γ . \end{matrix} \end{matrix}$

Assume that there is no such n and that γ is a limit ordinal. Let $n_{0} = β_{0} < β_{1} < \dots$ be such that ${sup}_{i \in ω} ω^{m - 1} β_{i} = ω^{m} γ$ . We may assume that for $i ⩾ 1$ each $β_{i}$ is a successor ordinal. We can pump $\begin{matrix} r ↾_{[ω^{m - 1} n, ω^{m - 1} (n + 1)]} \end{matrix}$ to a run $\begin{matrix} {\bar{r}}_{n} : [ω^{m - 1} β_{n}, ω^{m - 1} β_{n + 1}] \to S \end{matrix}$ for $n ⩾ n_{0}$ by the induction hypothesis for $m - 1$ . Finally, define $\bar{r}$ by $\begin{matrix} \bar{r} (δ) = \{\begin{matrix} r (δ) & if δ < ω^{m - 1} \cdot n_{0}, \\ {\bar{r}}_{n} (δ) & if δ \in [ω^{m - 1} β_{n}, ω^{m - 1} β_{n + 1}), \\ r (δ) & if r = ω^{m} \cdot γ . \end{matrix} \end{matrix}$

Assume that there is no such n and $γ = \bar{γ} + 1$ is a successor ordinal. Note that $r ([ω^{m - 1} n_{0}, ω^{m - 1} (n_{0} + 1))) ⊊ S_{lim}$ . Thus, we can apply the induction hypothesis for $m - 1$ to this subrun and obtain a run $r^{'}$ of length $ω^{m - 1} ((ω \cdot \bar{γ}) + 1)$ . Composition of $r ↾_{[0, ω^{m - 1} n_{0})}$ with $r^{'}$ and $r ↾_{[ω^{m - 1} (n_{0} + 1), ω^{m}]}$ yields a run r on the empty input of length $\begin{matrix} ω^{m - 1} n_{0} + ω^{m - 1} (ω \cdot \bar{γ} + 1) + ω^{m} = ω^{m} \cdot (\bar{γ} + 1) = ω^{m} γ . \end{matrix}$
□
Lemma 3.9.
Let $m \in N$ , $γ > 0$ some ordinal and $A = (S, Σ, I, F, Δ)$ be an automaton. Suppose that $S_{lim} \subseteq S^{-} \subseteq S$ and $s \in S^{-}$ with $| S^{-} | ⩽ m$ . If there is a run $r : ω^{m} γ + 1 \to S$ of $A$ on empty input with $\begin{matrix} r (0) = s, lim_{ω^{m} γ} r = S_{lim}, and r ({δ ∣ δ < ω^{m} γ}) = S^{-}, \end{matrix}$ then there is a run $\bar{r} : ω^{m} + 1 \to S$ of $A$ on empty input with $\begin{matrix} \bar{r} (0) = s, lim_{ω^{m}} \bar{r} = S_{lim}, \bar{r} ({δ ∣ δ < ω^{m}}) = S^{-} and \bar{r} (ω^{m}) = r (ω^{m} γ) . \end{matrix}$
Proof.
The proof is by induction on m, $| S^{-} |$ and γ. The claim is obvious for $m = 1$ or $γ = 1$ . Thus, we assume that $γ ⩾ 2$ and $m ⩾ 2$ and that the claim holds for all tuples $(m^{'}, {S^{-}}^{'}, γ^{'})$ where $m^{'} < m$ , or $m^{'} = m$ and $| {S^{-}}^{'} | < | S^{-} |$ , or $m^{'} = m$ and $| {S^{-}}^{'} | = | S^{-} |$ and $γ^{'} < γ$ .
Suppose that $S_{lim} ⊊ S^{-}$ . Let $α_{0}$ denote the least ordinal below $ω^{m} γ$ such that only states $s \in S_{lim}$ appear in $r ([α_{0}, ω^{m} γ))$ . There are two subcases:

First suppose that $α_{0} < ω^{m} β$ for a minimal $β < γ$ . Note that $[α_{0}, ω^{m} β)$ is isomorphic to $ω^{m}$ and $[α_{0}, ω^{m} γ)$ is isomorphic to $ω^{m} \cdot δ$ for some $δ ⩽ γ$ . Since ${S^{-}}^{'} : = r ([α_{0}, ω^{m} γ)) \subseteq S_{lim} ⊊ S^{-}$ , we can shrink $r ↾_{[α_{0}, ω^{m} γ]}$ to a run $\hat{r}$ with domain $[α_{0}, ω^{m} β]$ by the induction hypothesis for m and the smaller set ${S^{-}}^{'}$ . Since $β < γ$ we can finally apply the induction hypothesis to the shorter run that is the composition of $r ↾_{[0, α_{0})}$ and $\hat{r}$ and obtain the desired run $\bar{r}$ .

Second suppose that $α_{0} ⩾ ω^{m} β$ for all $β < γ$ . We conclude immediately that γ is a successor, i.e., $γ = \bar{γ} + 1$ and $α_{0} ⩾ ω^{m} \bar{γ}$ . Now we distinguish the following cases.

Assume that $\bar{γ} = 1$ and that $r (ω^{m}) \in {lim}_{(ω^{m})} r$ . Then there is a $β < ω^{m}$ such that $r (β) = r (ω^{m})$ and for each state $s \in S^{-}$ such that s occurs in r strictly before $ω^{m}$ also occurs before β. Then the composition of $r ↾ [0, β)$ with $r ↾ [ω^{m}, ω^{m} γ]$ yields the desired run.

Assume that $\bar{γ} = 1$ and that $r (ω^{m}) \notin {lim}_{(ω^{m})} r$ . Thus, there is some $β < ω^{m}$ such that $r ([β, ω^{m})) \subseteq S^{-} ∖ {r (ω^{m})}$ . Thus, we can apply the induction hypothesis for smaller m and $S^{-}$ shrinking $r ↾ [β, ω^{m})$ to a run $\hat{r}$ on domain $[β, β + ω^{m - 1})$ with $\hat{r} ([β, β + ω^{m - 1})) = r ([β, ω^{m}))$ and ${lim}_{(β + ω^{m - 1})} \hat{r} = {lim}_{(ω^{m})} r$ . Since $β < ω^{m - 1} \cdot k$ for some $k \in N$ , composition of $r ↾ [0, β)$ with $\hat{r}$ and $r ↾ [ω^{m}, ω^{m} γ)$ yields the desired run $\bar{r}$ of length $ω^{m}$ .

If $\bar{γ} > 1$ , we apply the induction hypothesis (for smaller $S^{-}$ or smaller γ) to $r ↾ [0, ω^{m} \bar{γ}]$ and shrink this run to a run $\bar{r}$ of length $ω^{m} + 1$ . The composition of $\bar{r}$ and $r ↾ [ω^{m} \bar{γ}, ω^{m} γ)$ is a run of length $ω^{m} \cdot 2$ and we can apply one of the previous two cases.

Suppose that $S_{lim} = S^{-}$ . We distinguish the following subcases:

Suppose that there is some $β < γ$ with ${lim}_{(ω^{m} β)} r = S^{-}$ . Then we can apply the induction hypothesis for $(m, S^{-}, β)$ to the run $r ↾_{[0, ω^{m} β]}$ and obtain a run $\hat{r} : ω^{m} + 1 \to S^{-}$ such that $\hat{r} (0) = 0$ , ${lim}_{(ω^{m})} \bar{r} = S_{lim}$ , and $\bar{r} ({δ ∣ δ < ω^{m}}) = S^{-}$ . Since ${lim}_{(ω^{m})} \hat{r} = {lim}_{(ω^{m} γ)} r$ , we can define the run $\bar{r}$ by $\begin{matrix} \bar{r} (δ) = \{\begin{matrix} \hat{r} (δ) & if δ < ω^{m}, \\ r (ω^{m} γ) & if δ = ω^{m} . \end{matrix} \end{matrix}$

Suppose that for each $β < γ$ , there is an $s \in S^{-}$ such that $s \notin {lim}_{(ω^{m} β)} r$ . There are the following subcases:

First suppose that $γ = \bar{γ} + 1$ . Since $S^{-} = S_{lim}$ , there is a $β_{0} \in [ω^{m} \bar{γ}, ω^{m} γ)$ with $r (β_{0}) = r (0)$ . Let $\bar{r} (δ) = r (β_{0} + δ)$ for $δ ⩽ ω^{m}$ .

Suppose that $γ = ω$ . By assumption, for each i, there is some $α_{i}$ with $ω^{m} i ⩽ α_{i} < ω^{m} (i + 1)$ and a state $s_{i} \in S^{-}$ such that $s_{i} \neq r (β)$ for all $α_{i} ⩽ β < ω^{m} (i + 1)$ . Thus, we can apply the induction hypothesis for $m - 1$ and smaller $S^{-}$ to each $r ↾ [α_{i}, ω^{m} (i + 1))$ and shrink it to a run of size $ω^{m - 1}$ . Note that the length of $r ↾ [ω^{m} i, α_{i}]$ is also bounded by some $ω^{m - 1} \cdot k_{i}$ . Thus, composition of these runs yields the desired run of length $ω^{m}$ .

Suppose that $γ ⩾ ω \cdot 2$ is a limit ordinal. Choose a sequence $0 = β_{0} < β_{1} < \dots < γ$ such that $r ([ω^{m} β_{i}, ω^{m} β_{i + 1})) = S^{-}$ for all $i \in N$ . Since ${lim}_{ω^{m} β_{i + 1}} r ⊊ S^{-} = S_{lim}$ , we can apply case 1. to each $r ↾_{[ω^{m} β_{i}, ω^{m} β_{i + 1}]}$ and obtain a run ${\hat{r}}_{i} : ω^{m} + 1 \to S$ with image $S^{-}$ such that ${\hat{r}}_{i} (ω^{m}) = {\hat{r}}_{i + 1} (0)$ . Choose $j < k \in N$ such that ${\hat{r}}_{j} (ω^{m} j) = {\hat{r}}_{k} (ω^{m} k)$ . Let $f : ω^{m + 1} \to {0, 1, \dots, k - 1}$ given by $f (δ) = i$ if there are $i_{0}, k_{0} \in N$ such that $ω^{m} i_{0} ⩽ δ < ω^{m} (i_{0} + 1)$ and $i = i_{0} < k$ or $i_{0} = k + k_{0} (k - j) + i$ , and $g : ω^{m + 1} \to ω^{m}$ given by $g (δ) = δ^{'}$ such that there is a $δ^{″}$ with $δ = ω^{m} \cdot δ^{″} + δ^{'}$ . Now define $\hat{r} : ω^{m} ω + 1 \to S$ given by $\begin{matrix} \hat{r} (δ) = \{\begin{matrix} {\hat{r}}_{f (δ)} (g (δ)) & if δ < ω^{m} ω, \\ r (ω^{m} γ) & if δ = ω^{m} ω . \end{matrix} \end{matrix}$ Now we can apply the induction hypothesis to $\hat{r}$ for $(m, S^{-}, ω)$ . □

Finally, we prove the Second Pumping Proposition. Proof of Proposition 3.7.

Let $r : α + 1 \to S$ be a run on empty input and set $S_{lim} : = {lim}_{α} r$ . Suppose that $\begin{matrix} S_{lim} = {q_{1}, q_{2}, \dots, q_{n}} . \end{matrix}$ Let β be minimal such that $r ([β, α)) = S_{lim}$ . By induction on pairs $(i, j)$ (ordered lexicographically) we can choose a sequence ${(α_{j}^{i})}_{i, j \in ω}$ such that
$α_{j}^{i} < α$ ,

$α_{0}^{0} > β$ ,

$r ([α_{j}^{i}, α_{j + 1}^{i})) = S_{lim}$ for all $i, j \in ω$ ,

$α_{0}^{i + 1} = sup {(α_{j}^{i})}_{j \in ω}$ , and

$α_{j}^{i}$ is of the form $ω^{m} \cdot γ$ for some ordinal γ.
Let $k < j$ be numbers such that $r (α_{0}^{k}) = r (α_{0}^{j}) = s^{'} \in S$ . By Lemma 3.9, we can shrink $r ↾_{[0, α_{0}^{k}]}$ to a run $r_{1} : ω^{m} + 1 \to S$ with
$r_{1} (0) = s_{0}$ ,

$r_{1} (ω^{m}) = s^{'}$ and

${lim}_{ω^{m}} r_{1} = S_{lim}$ ,
and $r ↾_{[α_{0}^{k}, α_{0}^{j}]}$ to a run $r_{2} : ω^{m} + 1 \to S$ with

$r_{2} (0) = s^{'}$ ,

$r_{2} (ω^{m}) = s^{'}$ and

${lim}_{ω^{m}} r_{2} = im (r_{2}) = S_{lim}$ .

Composing $r_{1}$ with ω many copies of $r_{2}$ extended with $s_{1}$ as final state yields the desired run.

Let $r : s_{0} \overset{◇^{ω^{m + 1}}}{\underset{A_{α}}{⟶}} s_{1}$ be a run such that ${lim}_{ω^{m} i} r = {lim}_{ω^{m + 1}} r$ for all $1 ⩽ i < ω$ . Let $k \in ω$ be such that $r ([ω^{m} k, ω^{m + 1})) = {lim}_{ω^{m + 1}} r$ . Let $k < k_{1} < k_{2}$ be numbers such that $r (ω^{m} k_{1}) = r (ω^{m} k_{2})$ . Application of Lemma 3.9, gives a run $\bar{r} : ω^{m} + 1 \to S$ such that $\bar{r} (0) = \bar{r} (ω^{m})$ and $im (\bar{r}) = {lim}_{ω^{m}} r = S_{lim}$ .

Define $r^{'} : α + 1 \to S$ by $\begin{matrix} r^{'} (β) = \{\begin{matrix} r (β) & if β < ω^{m} k_{2}, \\ \bar{r} (β^{'}) & if α > β ⩾ ω^{m} k_{2} and β = ω^{m} β^{″} + β^{'} for some β^{'} < ω^{m}, \\ r (ω^{m + 1}) & if β = α . \end{matrix} \end{matrix}$
□

3.3. Emptiness problem for ordinal-automata

Ordinal automata possess many properties known from the setting of finite word automata (cf. [21] for details on the latter). In particular, the usual constructions for union, intersection and projection carry over to our setting. Thanks to our pumping lemma, we can also show that emptiness of ordinal automata is decidable. Note that our setting is slightly different to the one considered by Wojciechowski [30] and Carton [6] because we consider only words of a fixed length α. This makes a difference since for instance the results in Section 3.4 depend on α.

Lemma 3.10.
Let α be an ordinal. Emptiness of $(α)$ -automata is decidable in polynomial time, i.e., there is an algorithm that, given an $(α)$ -automaton $A$ decides whether $L (A) = \emptyset$ .
Proof.
Fix an $(α)$ -automaton $A$ . Let n be a strict bound on the number of states of $A$ . Using closure under projection, we can assume that $A$ uses alphabet ${◇}$ . Recall that $α_{\sim n}$ denotes the unique multiple of $ω^{n + 1}$ such that $\begin{matrix} α = α_{\sim n} + ω^{n} m_{n} + ω^{n - 1} m_{n - 1} + \dots + m_{0} \end{matrix}$ for certain finite number $m_{0}, \dots, m_{n}$ . We first reduce the emptiness problem to finitely many emptiness problems for $ω^{i}$ -automata where i ranges over $0, 1, \dots, n$ . This reduction distinguishes whether $α_{\sim n}$ has countable cofinality.
First assume that $α_{\sim n} = 0$ . $L (A) \neq \emptyset$ if and only if there are states $\begin{matrix} q_{n}^{0}, q_{n}^{1}, \dots, q_{n}^{m_{n}}, q_{n - 1}^{0}, q_{n - 1}^{1}, \dots, q_{n - 1}^{m_{n - 1}}, \dots, q_{0}^{m_{0} - 1}, q_{0}^{m_{0}} \end{matrix}$ such that

$q_{n}^{0}$ is an initial state and $q_{0}^{m_{0}}$ is a final state,

$q_{i}^{m_{i}} = q_{i - 1}^{0}$ for all $1 ⩽ i ⩽ n$ , and

for all $0 ⩽ i ⩽ n$ and $0 ⩽ j < m_{i}$ , there is a run $q_{i}^{j} \overset{◇^{ω^{i}}}{\underset{A}{⟶}} q_{i}^{j + 1}$ .

Next assume that $α_{\sim n} \neq 0$ has countable confinality. Pumping with Proposition 3.6 (applied to words of length $α_{\sim n}$ ) shows that $L (A)$ is nonempty if and only if there are states $\begin{matrix} s, q_{n}^{0}, q_{n}^{1}, \dots, q_{n}^{m_{n}}, q_{n - 1}^{0}, q_{n - 1}^{1}, \dots, q_{n - 1}^{m_{n - 1}}, \dots, q_{0}^{m_{0} - 1}, q_{0}^{m_{0}} \end{matrix}$ such that

s is an initial state and $q_{0}^{m_{0}}$ is a final state,

$q_{i}^{m_{i}} = q_{i - 1}^{0}$ for all $1 ⩽ i ⩽ n$ ,

there is a run $s \overset{◇^{ω^{n + 1}}}{\underset{A}{⟶}} q_{n}^{0}$ , and

for all $0 ⩽ i ⩽ n$ and $0 ⩽ j < m_{i}$ , there is a run $q_{i}^{j} \overset{◇^{ω^{i}}}{\underset{A}{⟶}} q_{i}^{j + 1}$ .

Finally assume that $α_{\sim n} \neq 0$ has countable confinality. Pumping with Proposition 3.7 (applied to words of length $α_{\sim n}$ ) shows that $L (A)$ is nonempty if and only if there are states $\begin{matrix} s, s^{'}, q_{n}^{0}, q_{n}^{1}, \dots, q_{n}^{m_{n}}, q_{n - 1}^{0}, q_{n - 1}^{1}, \dots, q_{n - 1}^{m_{n - 1}}, \dots, q_{0}^{m_{0} - 1}, q_{0}^{m_{0}} \end{matrix}$ such that

s is an initial state and $q_{0}^{m_{0}}$ is a final state,

$q_{i}^{m_{i}} = q_{i - 1}^{0}$ for all $1 ⩽ i ⩽ n$ ,

there are runs $s \overset{◇^{ω^{n}}}{\underset{A}{⟶}} s^{'}$ and $r : s^{'} \overset{◇^{ω^{n}}}{\underset{A}{⟶}} s^{'}$ such that there is a transition $(D, q_{n}^{0})$ for $D = im (r) = {lim}_{ω^{n}} r$ , and

for all $0 ⩽ i ⩽ n$ and $0 ⩽ j < m_{i}$ , there is a run $q_{i}^{j} \overset{◇^{ω^{i}}}{\underset{A}{⟶}} q_{i}^{j + 1}$ .
Using this case distinction, we can decide emptiness of $A$ , if we can decide whether there is a run $r : q \overset{◇^{ω^{i}}}{\underset{A}{⟶}} q^{'}$ for given states q, $q^{'}$ and an $i \in ω$ and if we can determine the possible image and the possible set of cofinal states of such runs. But this is decidable due to a result of Wojciechowski [30]. Moreover, Carton [6] even showed how to decide such problems in polynomial time. □

3.4. Determinisation of ordinal automata

Another important result for finite automata is the fact that finite automata can be determinised whence we can construct an automaton accepting the complement of the language of a given automaton. This result carries only partly over in the sense that the closure under determinisation (and complementation as well) of $(α)$ -automata depends on α. Büchi [4,5] provided a determinisation procedure for α-automata for all countable α (we write α-automaton instead of $(α)$ -automaton because in this setting also words with infinite support are allowed as inputs). For the setting where words with infinite support are allowed, this is optimal as we show by an example in the Appendix.

Interestingly, the picture changes in our setting because we consider automata that only accept $(α)$ -words with finite support. We prove below that an $(α)$ -automaton $A$ can be determinised if $L (A)$ only contains finite $(α)$ -words and $α < ω_{1} + ω^{ω}$ . On the other hand there is an $(ω_{1} + ω^{ω})$ -automaton $A$ such that the complement of $L (A)$ is not the language of any $(ω_{1} + ω^{ω})$ -automaton.

Definition 3.11.
An $(α)$ -automaton $A = (Q, Σ, I, F, Δ)$ is deterministic if I is a singleton, for each pair $(q, σ) \in Q \times Σ$ there is at most one $p \in Q$ such that $(q, σ, p) \in Δ$ and for each subset $P \subseteq Q$ , there is at most one $q \in Q$ such that $(P, q) \in Δ$ .

Recall that complementation for deterministic $(α)$ -automata is trivial: exchanging the final and the nonfinal states of a deterministic automaton $A$ yields an deterministic automaton $B$ such that $L (B) = Σ^{α} ∖ L (A)$ . Since the set of finite $(α)$ -words is recognised by an automaton as well, we can easily derive an automaton $C$ such that $L (C) = Σ^{(α)} ∖ L (A)$ .

We first give a simple example that shows that complementation of $(ω_{1} + ω^{ω})$ -automata is in general not possible even if the automaton only accepts finite $(ω_{1} + ω^{ω})$ -words.
Example 3.2.
Let $\begin{matrix} L = {w \in {◇, a}^{(ω_{1} + ω^{ω})} ∣ supp (w) = {β}, β is a limit ordinal and β \neq ω_{1}} . \end{matrix}$ L is accepted by the automaton $\begin{matrix} A = ({s_{1}, s_{2}, s_{3}, s_{4}}, {◇, a}, {s_{1}}, {s_{4}}, Δ), \end{matrix}$ where Δ consists of
$(s_{i}, ◇, s_{j})$ for all $i, j \in {1, 2}$ ,

$({s_{1}}, s_{1})$ ,

$({s_{2}}, s_{3})$ , $({s_{1}, s_{2}}, s_{3})$ ,

$(s_{3}, a, s_{4})$ , $(s_{4}, ◇, s_{4})$ , and

$({s_{4}}, s_{4})$ .
This is an extension of the automaton from Example 3.1 that may read one letter a at those positions where the original automaton enters state $s_{3}$ .

Heading for a contradiction assume that $B$ is an automaton that accepts the complement of $L (A)$ (with respect to ${◇, a}^{(α)}$ or ${◇, a}^{α}$ ). Let r be an accepting run of $B$ on the word w defined by $\begin{matrix} w (β) = \{\begin{matrix} a & if β = ω_{1}, \\ ◇ & otherwise . \end{matrix} \end{matrix}$ Using Propositions 3.6 and 3.7, we can shrink $r ↾_{[0, ω_{1})}$ to a run on empty input of length $ω^{ω}$ and we can pump using Proposition 3.6 $r ↾_{[ω_{1} + 1, ω_{1} + ω^{ω}]}$ to a run with domain $[ω^{ω}, ω_{1} + ω^{ω}]$ . Concatenation of these two runs yields an accepting run of $B$ on v defined by $\begin{matrix} v (β) = \{\begin{matrix} a & if β = ω^{ω}, \\ ◇ & otherwise, \end{matrix} \end{matrix}$ which contradicts the assumption that $B$ accepts the complement of $L (A)$ .

Note that the same example works for all ordinals $α ⩾ ω_{1} + ω^{ω}$ . In case that α has uncountable cofinality, we only have to replace the second application of Proposition 3.6 by a use of Proposition 3.7.

Now we turn to the proof of the rather surprising fact that for all $α < ω_{1} + ω^{ω}$ we can determinise $(α)$ -automata whose language consists of finite $(α)$ -words only. This result relies on three facts.

The determinisation procedure of $(γ)$ -automata for countable ordinals γ is independent of the choice of γ.

We can compute all the possible pairs of initial and final states of runs on empty input of length $ω_{1}$ (using decidability of emptiness), and the interval $[β, ω_{1})$ is isomorphic to $ω_{1}$ for all ordinals $β < ω_{1}$ .

For ordinals $α < ω_{1} + ω^{ω}$ a deterministic automaton can detect position $ω_{1}$ in an $(α)$ -word.
Proposition 3.12.
Let $α < ω_{1} + ω^{ω}$ be some ordinal and $A$ some $(α)$ -automaton such that $L (A) \subseteq Σ^{(α)}$ (for some alphabet Σ). There is a deterministic $(α)$ -automaton $B$ such that $L (B) = L (A)$ .

Before we come to the proof, we collect some results from the literature that we exhibit in our construction of $B$ . Lemma 3.13 ([5]).

Let $A$ be some ordinal automaton with state set S. From $A$ one can compute a deterministic automaton $B$ with state set Q and initial state i, and a function $f : Q \to 2^{S \times S}$ such that for all countable ordinals γ and all $(γ)$ -words w, all $q \in Q$ and all $s, s^{'} \in S$ the following are equivalent:

there is a run $i \overset{w}{\underset{B}{⟶}} q$ and $(s, s^{'}) \in f (q)$ , and

there is a run $s \overset{w}{\underset{A}{⟶}} s^{'}$ .

Lemma 3.14 (cf. [30]).

For each $α < ω^{ω}$ , there is a deterministic ordinal automaton $A$ that marks α in the sense that there is a special state s of $A$ such that on every input w (of length at least α) the run of $A$ on w is in state s exactly at position α. Similarly, for every number $m \in N$ there is a deterministic automaton $A_{m}$ with a special state $s_{m}$ such that on input any $(γ)$ -word w the run of $A_{m}$ reaches state $s_{m}$ exactly at all positions of the form $ω^{m} \cdot β ⩽ γ$ for $β ⩾ 1$ some ordinal.

Proof.
$A_{m}$ has states ${s_{1}, \dots, s_{m}}$ . At successor steps $A_{m}$ always switches to state $s_{1}$ . At a limit step where states $s_{1}, s_{2}, \dots, s_{i - 1}$ appear cofinally, $A_{m}$ switches to state $max {s_{m}, s_{i}}$ .

The construction of $A$ uses similar ideas and is left to the reader. An optimal construction minimizing the number of states can be found in [30]. □
Proof of Proposition 3.12.
If $α < ω_{1}$ , just apply Lemma 3.13. Now assume that $ω_{1} ⩽ α < ω_{1} + ω^{ω}$ and let $A$ be an $(α)$ -automaton. The basic idea of our determinisation procedure is to compute a deterministic automaton $B$ that consists of three components $B_{1}$ , $B_{2}$ and $B_{3}$ with the following behaviour:
$B_{1}$ is the deterministic variant of $A$ obtained from Lemma 3.13. Given a position $β < ω_{1}$ , the state of $B_{1}$ at β on input w reports via the function f those pairs $(q, q^{'})$ such that there is a run $q \overset{w ↾_{[0, β)}}{\underset{A}{⟶}} q^{'}$ .

Using the information from $B_{1}$ , $B_{2}$ reports at all positions $β ⩽ ω_{1}$ the possible pairs $(q, q^{'})$ such that there is a run $q \overset{w ↾_{[0, β^{'}]} ◇^{ω_{1}}}{\underset{A}{⟶}} q^{'}$ where $β^{'} = max ({0} \cup (supp (w) \cap β))$ . This component only changes its state at positions β with $β \in supp (w)$ . At such a position, it adds a pair $(q, q^{'})$ to its state if there is a state $q^{″}$ such that $(q, q^{″}) \in f (s)$ for s the state of $B_{1}$ and such that there is a run $q^{″} \overset{◇^{ω_{1}}}{\underset{A}{⟶}} q^{'}$ (since emptiness is decidable, those pairs $(q^{″}, q^{'})$ are effectively computable).

$B_{3}$ behaves like the deterministic variant of some $A_{I^{'}}$ on the countable tail of α, i.e., on $[ω_{1}, α]$ where $A_{I^{'}}$ denotes the automaton obtained from $A$ by replacing the initial states with some set $I^{'}$ that we describe below. Assume that $α = ω_{1} + α^{'}$ and assume that $α^{'} < ω^{m}$ . At each position $ω^{m} \cdot β$ with $1 ⩽ β ⩽ ω_{1}$ , $B_{3}$ starts the computation of the deterministic version of $A_{I^{'}}$ from Lemma 3.13 where $I^{'}$ contains all those states q such that the state of $B_{2}$ at $ω^{m} \cdot β$ contains a pair $(i, q)$ where i is some initial state of $A$ . $B_{3}$ then simulates the deterministic version of $A_{I^{'}}$ up to $ω^{m} \cdot β + α^{'}$ and then stops its computation.
$B$ now accepts input w if and only if $B_{3}$ simulates some $A_{I^{'}}$ on $[ω_{1}, α]$ and reaches a state q at α such that $f (q)$ contains a pair $(i, q)$ such that $i \in I^{'}$ and q is a final state of $A$ .

Using the previous lemmas it is clear that the automaton $B$ with the described behaviour can be computed from $A$ . We finally prove that $L (B) = L (A)$ . First assume that $w \in L (A)$ . Fix a run $r : q_{i} \overset{w}{\underset{A}{⟶}} q_{f}$ for an initial state $q_{i}$ and a final state $q_{f}$ of $A$ . Let $β = max {{0} \cup (supp (w) \cap ω_{1})}$ and $q_{1} = r (β + 1)$ . By definition the state of $B_{1}$ at $β + 1$ is some state s such that $(q_{i}, q_{1}) \in f (s)$ . Since $r ↾_{[β + 1, ω_{1}]}$ witnesses $q_{1} \overset{◇^{ω_{1}}}{\underset{A}{⟶}} r (ω_{1})$ , the state of $B_{2}$ on $[β + 1, ω_{1}]$ is constant and contains the pair $(q_{i}, r (ω_{1}))$ . We conclude that $B_{3}$ simulates the deterministic variant of $A_{I^{'}}$ on $[ω_{1}, α]$ for some $I^{'}$ that contains $r (ω_{1})$ . Now $r ↾_{[ω_{1}, α]}$ witnesses $r (ω_{1}) \overset{w ↾_{[ω_{1}, α)}}{\underset{A}{⟶}} q_{f}$ whence $B_{3}$ ’s state reports (via function f) the pair $(r (ω_{1}), q_{f})$ of an initial state of $A_{I^{'}}$ and a final state. Thus, $B$ accepts on input w.

Similarly, if $B$ accepts on input w, we can reconstruct an accepting run r of $A$ on w. □

3.5. Ordinal automatic structures

Automata on words (or infinite words or (infinite) trees) have been applied fruitfully for representing structures. This can be lifted to the setting of $(α)$ -words and leads to the notion of $(α)$ -automatic structures. In order to use $(α)$ -automata to recognize relations of $(α)$ -words, we need to encode tuples of $(α)$ -words by one $(α)$ -word:

Definition 3.15.
Let Σ be an alphabet and $r \in N$ .
We regard any tuple $\bar{w} = (w_{1}, \dots, w_{r}) \in {(Σ^{(α)})}^{r}$ of $(α)$ -words over some alphabet Σ as an $(α)$ -word $\bar{w} \in {(Σ^{r})}^{(α)}$ over the alphabet $Σ^{r}$ by defining $\begin{matrix} \bar{w} (β) = (w_{1} (β), \dots, w_{r} (β)) \end{matrix}$ for each $β < α$ .

An r-dimensional $(α)$ -automaton (over Σ) is an $(α)$ -automaton $A$ (over $Σ^{r}$ ). The r-ary relation on $Σ^{(α)}$ recognized by $A$ is denoted by $\begin{matrix} R (A) = {\bar{w} \in {(Σ^{(α)})}^{r} ∣ \bar{w} \in L (A)} . \end{matrix}$

Remark 3.1.

Recall that we declared $(◇, \dots, ◇)$ to be the blank symbol of $Σ^{r}$ . Thus, $supp (\bar{w}) = supp (w_{1}) \cup \dots \cup supp (w_{r})$ is indeed a finite set.

Usually, this interpretation of $\bar{w}$ as an $(α)$ -word is called convolution of $\bar{w}$ and denoted $\otimes \bar{w}$ . For the sake of convenience, we just omit the ⊗-symbol.

Definition 3.16.
Let $τ = {R_{1}, R_{2}, \dots, R_{m}}$ be a finite relational signature and let relation symbol $R_{i}$ be of arity $r_{i}$ . A structure $A = (A, R_{1}^{A}, R_{2}^{A}, \dots, R_{m}^{A})$ is $(α)$ -automatic if there are an alphabet Σ and $(α)$ -automata $A, A_{\approx}, A_{1}, \dots, A_{m}$ such that
$A$ is an $(α)$ -automaton over Σ,

for each $R_{i} \in τ$ , $A_{i}$ is an $r_{i}$ -dimensional $(α)$ -automaton over Σ recognizing an $r_{i}$ -ary relation $R (A_{i})$ on $L (A)$ ,

$A_{\approx}$ is a 2-dimensional $(α)$ -automaton over Σ recognizing a congruence relation $R (A_{\approx})$ on the structure $A^{'} = (L (A), L (A_{1}), \dots, L (A_{m}))$ , and

the quotient structure $A^{'} / R (A_{\approx})$ is isomorphic to $A$ , i.e., $A^{'} / R (A_{\approx}) ≅ A$ .
In this situation, we call the tuple $(A, A_{\approx}, A_{1}, \dots, A_{m})$ an $(α)$ -automatic presentation of $A$ . This presentation is said to be injective if $L (A_{\approx})$ is the identity relation on $L (A)$ . In this case, we usually omit $A_{\approx}$ from the tuple of automata forming the presentation.

As in the case of classical automatic structures, for ordinals $α < ω_{1} + ω^{ω}$ , the class of $(α)$ -automatic structures behaves well with respect to first-order logic extended by $\exists^{\infty}$ , i.e., the $FO (\exists^{\infty})$ -theory of every $(α)$ -automatic structure is uniformly decidable. Our proof for the $\exists^{\infty}$ -quantifier is inspired by the analogous result for tree-automatic structures. For the tree-automatic result one uses the fact that a set of finite trees is finite if and only if the union of the domains of all trees from this set forms the domain of some finite tree. Analogously, we use the fact that a set of finite sets of ordinals is finite if and only if the union of all these sets is a finite set.
Proposition 3.17.
For each $α < ω_{1} + ω^{ω}$ , the class of $(α)$ -automatic structures is effectively closed under expansion by $FO (\exists^{\infty})$ definable relations.

For each ordinal β, the class of $(β)$ -automatic structures is effectively closed under expansion by $\exists^{} Pos$ definable relations.*
Proof.
The proof relies on the closure of recognizable $(α)$ -languages under projection (for ∃), union (for ∨), intersection (for ∧) and complementation (for ¬) and is by induction on the structure of first-order formulas. It is completely analogous to the case of automatic structures whence we omit it. For the $\exists^{\infty}$ quantifier, we use a reduction to first-order logic over some expansion. This technique is known from the setting of tree-automatic structures.

Note that for every α the relation $\begin{matrix} ⊑ = {(w, v) \in {(Σ^{(α)})}^{2} ∣ supp (w) \subseteq supp (v)} \end{matrix}$ is recognizable by an $(α)$ -automaton. Given an $(α)$ -automatic structure $A$ , elements $a_{1}, \dots, a_{n}$ of $A$ and an $FO (\exists^{\infty})$ formula $\exists^{\infty} x φ (z_{1}, \dots, z_{n}, x)$ , we have $\begin{matrix} A ⊧ \exists^{\infty} x φ (a_{1}, \dots, a_{n}, x) \end{matrix}$ if and only if $\begin{matrix} A_{⊑} ⊧ ψ : = \neg (\exists z \in Σ^{(α)} \forall x \exists x^{'} (φ (a_{1}, \dots, a_{n}, x) \to (x \approx x^{'} \land x^{'} ⊑ z))), \end{matrix}$ where $A_{⊑}$ denotes the expansion of $A$ by the relation ⊑ and ≈ denotes the congruence from the presentation of $A$ .

The proof of the equivalence of the two formulas can be sketched as follows. If there are only finitely many $b_{1}, \dots, b_{m} \in A$ such that $A ⊧ φ (a_{1}, \dots, a_{n}, b_{i})$ then we can pick one representative $c_{i}$ from the ≈-class representing $b_{i}$ . Now let d be a word such that $supp (d) = ⋃_{i = 1}^{m} supp (c_{i})$ . Any witness for φ is equivalent to one of the $c_{i}$ and $supp (c_{i}) \subseteq supp (d)$ . Thus, $A$ does not satisfy ψ.

On the other hand, if there are infinitely many pairwise inequivalent elements $b_{i}$ satisfying ϕ, then the union of their supports forms an infinite set. Thus, for any given finite $(α)$ -word c we find an $b_{i}$ that satisfies ϕ and is not equivalent to any word whose support is contained in the support of c because there are only finitely many words whose support is contained in $supp (c)$ . Thus, $A$ satisfies ψ. □
Corollary 3.18.
Let $α < ω_{1} + ω^{ω}$ be some ordinal. The $FO (\exists^{\infty})$ -theory of every $(α)$ -automatic structure is decidable.

For $β ⩾ ω_{1} + ω^{ω}$ the $\exists^{} Pos$ -theory of every* $(β)$ -automatic structure is decidable.
Proof.
Fix an $(α)$ -automatic structure $A$ . Given an $FO$ -sentence φ we construct (using the previous lemma) the automaton $A_{φ}$ corresponding to the relation defined by φ. Since φ is a sentence, $A_{φ}$ is inputless. By construction $A ⊧ φ$ if and only if $A_{φ}$ accepts on empty input. The latter is decidable by Lemma 3.10. □

This result shows that the class of $(α)$ -automatic structures for $α < ω_{1} + ω^{ω}$ is a useful tool for proving decidability of first-order logic on some structures.

In the case of an $(α)$ -automatic structure $A$ where $α < ω_{1} + ω^{ω}$ , we can transform any given presentation into an injective one. This is due to the fact that there is a $(α)$ -automata recognisable well-order on $Σ^{(α)}$ , which allows to select the minimal representative of every equivalence class.
Lemma 3.19.
The set $Σ^{(α)}$ admits an $(α)$ -automatic well-order, i.e., there is a 2-dimensional $(α)$ -automaton over Σ recognizing a well-order on $Σ^{(α)}$ .
Proof.
Fix a linear order $⩽_{Σ}$ on Σ. It is well-known that the following definition yields a strict well-order < of order type $| Σ |^{α}$ on $Σ^{(α)}$ (cf. [28, Excercise 3.4.5]): $u < v$ if $u \neq v$ and $u (β) <_{Σ} v (β)$ for the maximal $β \in supp (u) \cup supp (v)$ with $u (β) \neq v (β)$ . It is easy to see that this order can be recognized by a 2-dimensional $(α)$ -automaton. Basically, such an automaton first guesses the position β, then verifies $u (β) <_{Σ} v (β)$ and finally checks that it guessed β correctly. □

Thanks to the previous lemma and closure under first-order definitions, we can apply the same construction as for automatic structures in order to translate non-injective presentations to injective ones. Proposition 3.20.
Let $γ < ω_{1} + ω^{ω}$ be an ordinal and $A$ an $(γ)$ -automatic structure. There is an injective $(γ)$ -automatic presentation of $A$ .
Proof.
Let $(A, A_{\approx}, A_{1}, \dots, A_{n})$ be a $(γ)$ -automatic presentation of $A$ . Using the automatic well-order ⩽ from the previous lemma, we can construct an automaton $A^{'}$ such that $\begin{matrix} L (A^{'}) = {w \in L (A) ∣ \forall v \in L (A) : (w, v) \notin L (A_{\approx}) or w ⩽ v} . \end{matrix}$ Apparently, $A^{'}$ accepts exactly one member of each $A_{\approx}$ -class accepted by $A$ . Intersection of $A_{i}$ with an $r_{i}$ -dimensional variant of $A^{'}$ yields an $r_{i}$ -dimensional automaton $A_{i}^{'}$ such that $\begin{matrix} L (A_{i}^{'}) = L (A_{i}) \cap L {(A^{'})}^{r_{i}} . \end{matrix}$ Thus $(A^{'}, A_{1}^{'}, \dots, A_{n}^{'})$ forms an injectively $(γ)$ -automatic presentation of $A$ . □

4. Complete structures under FO-interpretations

Blumensath [2] characterised the classes of automatic structures represented by finite (infinite, respectively) words (trees, respectively) independently from the notion of automata. These characterisations are based on first-order interpretations.2

²
Readers who are not familiar with the notion of logical interpretations can obtain the necessary basics from [2].

For instance, consider

A = (N, +, |_{p})

where

x |_{p} y

iff there is a

k \in N

such that

x = p^{k}

and x is a divisor of y (for some fixed prime number p).

A

is an automatic structure and every automatic structure

B

is first-order interpretable in

A

(cf. [2]). In this sense

A

is the most complex automatic structure. We call a structure with these properties complete for the class of automatic structures under first-order interpretations. Blumensath identified similar structures that are complete for the class of infinite word automatic structures and finite or infinite tree automatic structures.

Analogously, we call $A$ complete for the class of $(α)$ -automatic structures if $A$ is $(α)$ -automatic and any $(α)$ -automatic structure can be interpreted in $A$ via first-order interpretations.

For the rest of this section, we fix the alphabet $Σ = {0, 1, □, ◇}$ .

Definition 4.1.

Let $F_{α} = (L, {Next}_{0}, {Next}_{1}, {Next}_{◇}, ⩽, el)$ where

L is the set of all $(β)$ -words over alphabet ${0, 1, ◇}$ for all $β ⩽ α$ ,

for $i \in {0, 1, ◇}$ , $(w, v) \in {Next}_{i}$ , if w is a $(β)$ -word, v a $(β + 1)$ -word and $\begin{matrix} v (γ) = \{\begin{matrix} w (γ) & for γ < β, \\ i & for γ = β, \end{matrix} \end{matrix}$

⩽ is the prefix order on words of length up to α, i.e., $w ⩽ v$ for a $(β)$ -word w and a $(γ)$ -word v if $β ⩽ γ$ and $v ↾_{β} = w$ , and

$(x, y) \in el$ if there is a $β ⩽ α$ such that x and y are both $(β)$ -words ( $el$ stands for ‘equal length’).

For words

w \in L

, we write

| w |

for the

β ⩽ α

such that w is a

(β)

-word.

The main result of this section is the following theorem.

Theorem 4.2.

Let $α < ω_{1} + ω^{ω}$ be an ordinal. $F_{α}$ is complete for the class of $(α)$ -automatic structures.

Let us start with the easy part of the theorem:

Proposition 4.3.

For all ordinals α, $F_{α}$ is $(α)$ -automatic.

Proof.

For $β < α$ we can encode a $(β)$ -word w over ${0, 1}_{◇}$ as the $(α)$ -word $\bar{w}$ over alphabet Σ given by $\begin{array}{l} \bar{w} (γ) = \{\begin{matrix} w (γ) & for γ < β, \\ □ & for γ = β, \\ ◇ & otherwise . \end{matrix} \end{array}$ Moreover, we encode an $(α)$ -word w by $\bar{w} : = w$ . The set $\bar{L}$ of $(α)$ -words over Σ encoding $(β)$ -words for some $β ⩽ α$ is clearly $(α)$ -automatic. An automaton for $\bar{L}$ just has to check that after the occurrence of □ only label ◇ appears and that the word has finite support.

An automaton for ${Next}_{i}$ has to check, on input $(w, v)$ , that at the β with $w (β) = □$ the value of v is i, i.e., that $v (β) = i$ and that $v (β + 1) = □$ (in case that $β + 1 < α$ ).

An automaton for ⩽ has to check, on input $(w, v) \in \bar{L} \times \bar{L}$ , that the two words agree up to the occurrence of □ in w.

An automaton for $el$ only has to check that there is an occurrence of $(□, □)$ or no occurrence of symbol □ in either of the two words (in the latter case, both words are of length α). □

The proof that any $(α)$ -automatic structure is first-order definable in $F_{α}$ (for $α < ω_{1} + ω^{ω}$ ) needs a more involved argument. We basically combine Blumensath’s approach from the classical setting with a clever use of the pumping lemma. We first briefly review Blumensath’s approach and then explain how pumping allows to adapt it to our setting.

In the setting of usual (finite) words, given an automatic relation R over alphabet $Σ^{'}$ , we can first identify the alphabet $Σ^{'}$ with some subset of $Σ^{k}$ . Similarly, we can identify the state set of an automaton $A$ corresponding to R with some subset of $Σ^{l}$ . This allows to represent elements of R as well as runs of $A$ as tuples of words over Σ. Then one constructs a first-order formula (over signature ${{Next}_{0}, {Next}_{1}, {Next}_{◇}, ⩽, el}$ ) $\begin{matrix} φ_{R} (\bar{w}) = \exists \bar{r} (max (\bar{w}, \bar{r}) \land R (\bar{w}, \bar{r}) \land S (\bar{r}) \land A (\bar{r})), \end{matrix}$ where

$\bar{w}$ is a tuple of words over Σ of the right size to represent elements from R and $\bar{r}$ is a tuple of size l, i.e., of the right size to represent sequences of states of the automaton $A$ ,

max states that the elements from $\bar{r}$ are long enough to code a run on the words encoded by $\bar{w}$ ,

R states that the sequence of states encoded by $\bar{r}$ respects the transition relation of $A$ ,

S states that $\bar{r} (0)$ encodes an initial state, and

A states that the last state encoded by $\bar{r}$ is accepting.

Using these formulas

φ_{R}

, we can now give a first order formula for each automatic relation. In particular, the formulas corresponding to the relations of an automatic structure form a first-order interpretation of this structure in

F_{ω}

In order to lift Blumensath’s approach to $α < ω_{1} + ω^{ω}$ we face one problem. We can code a run of an $(α)$ -automaton $A$ (with state set $Σ^{l}$ ) as an l-tuple of infinite α-words over Σ. But more than one state might appear infinitely often whence this run cannot be encoded directly as an $(α)$ -word. Here, the pumping lemma comes to our rescue: first assume that α is countable. If a run parses an empty subword of length $ω^{m} γ$ where m is the number of states of $A$ and $γ > 0$ some countable ordinal, there is a run from state q to state $q^{'}$ on this word if and only if there is one on the empty word of length $ω^{m}$ . Thus, we can hardcode a table of the possible runs on ${(◇)}^{ω^{n}}$ for each $1 ⩽ n ⩽ m$ in our formulas. This allows to use an $(α)$ -word $\bar{r}$ to encode the states of a run r on $(α)$ -words $\bar{w}$ at the positions from $supp (w)$ and at finitely many positions in the gaps between the support such that the distance between two such positions is either $ω^{n}$ for some $n < m$ or $ω^{m} γ$ for some ordinal $γ > 0$ .

If $ω_{1} ⩽ α ⩽ ω_{1} + ω^{ω}$ , we still can apply the idea described above. We only have to take care of a possible gap in $supp (w)$ of uncountable cofinality. From our basic results on $(α)$ -automata we know that there are less possible runs on an empty input of some length $ω^{m} β$ where β has uncountable cofinality than in the case that β has countable cofinality. Fortunately, if $α < ω_{1} + ω^{j}$ for some $j \in N$ , then any gap whose right end is of uncountable cofinality ends exactly at $ω_{1}$ . Moreover, position $ω_{1}$ in an α word is characterised by the fact that it is the maximal position p that is of the form $p = ω^{j + 1} \cdot γ$ for some ordinal γ. As we show below, this position is definable in $F_{α}$ . Thus, by a special treatment of the gaps ending at $ω_{1}$ we can lift the result to all $α < ω_{1} + ω^{ω}$ .

We now provide the details of the proof. As a simplification we first show that it is sufficient to consider $(α)$ -automatic structures over the previously fixed alphabet Σ.

Lemma 4.4.

Every $(α)$ -automatic structure is first-order interpretable in an $(α)$ -automatic structure with presentation over the alphabet Σ.

Proof.

Let $(A, A_{1}, \dots, A_{k})$ be a presentation of some structure $A$ over alphabet $Σ^{'}$ . We identify $Σ^{'}$ with a subset of $Σ^{n}$ for big enough n. It is easy to construct automata $A^{'}, A_{1}^{'}, \dots, A_{k}^{'}$ such that the prime version of every automaton behaves like the original, but on inputs over $Σ^{n}$ . It is straightforward to give an n-dimensional first-order interpretation of $A$ over the structure $(Σ^{(α)}, L (A^{'}), L (A_{1}^{'}), \dots, L (A_{k}^{'}))$ . □

What is left to show is the following proposition

Proposition 4.5.

Let $α < ω_{1} + ω^{ω}$ . Let $R \subseteq {(Σ^{k})}^{(α)}$ be a relation recognisable by some $(α)$ -automaton. Then R is first-order interpretable in $F_{α}$ .

Fix an automaton $A = (Σ^{m}, Σ_{◇}^{k}, I, F, Δ)$ that recognises R. Let $Δ = Δ_{s} \cup Δ_{l}$ be the partition into the successor transitions $Δ_{s} \subseteq Q \times Σ^{k} \times Q$ and the limit transitions $Δ_{l} \subseteq 2^{Q} \times Q$ .

In order to simplify the arguments of our proof we first establish some notation for certain first-order definable relations.

We write $a ⊏ b$ if and only if $| a | < | b |$ . This is definable from $el$ and ⩽.

Set ${lim}_{⩾ 0} (p) = \exists x (x ⊏ p)$ and for all $i ⩾ 1$ $\begin{matrix} lim_{⩾ i} (p) = \exists z (z ⊏ p) \land \forall z ((z ⊏ p) \to \exists y (z ⊏ y ⊏ p \land lim_{⩾ i - 1} (y))) . \end{matrix}$ By an easy induction on $i \in N$ one shows that $F_{α} ⊧ {lim}_{⩾ i} (p)$ if and only if $| p | = ω^{i} \cdot β$ for some ordinal $β ⩾ 1$ .

We set $\begin{matrix} lim_{i} (p) = lim_{⩾ i} (p) \land \neg lim_{⩾ i + 1} (p) . \end{matrix}$ ${lim}_{i} (p)$ is satisfied in $F_{α}$ if and only if $i \in N$ is maximal such that $| p | = ω^{i} β$ for some ordinal $β ⩾ 1$ . In the following, we call such a position an i-limit.

For $\bar{σ} = (σ_{1}, \dots, σ_{n}) \in {0, 1, ◇}^{n}$ and $\bar{x} \in (x_{1}, \dots, x_{n})$ y we define $\begin{array}{l} {Sm}_{\bar{σ}} (\bar{x}, y) = ⋀_{i = 1}^{n} \exists x^{'} \exists x^{″} (el (y, x^{'}) \land {Next}_{σ_{i}} (x^{'}, x^{″}) \land x^{″} ⩽ x_{i}) . \end{array}$ $A_{α} ⊧ {Sm}_{\bar{σ}} (\bar{w}, p)$ if and only if $| p | < α$ and the symbols of $\bar{w}$ at position p are $\bar{σ}$ , i.e., $w_{i} (| p |) = σ_{i}$ for $\bar{w} = (w_{1}, \dots, w_{n})$ .

We extend the $el$ -predicate to arbitrary many variables, i.e., we write $el (x_{1}, \dots, x_{n})$ for $el (x_{1}, x_{2}) \land el (x_{2}, x_{3}) \land \dots \land el (x_{n - 1}, x_{n})$ .

For all $n \in N$ let $max (x_{1}, x_{2}, \dots, x_{n}) = \forall x (x_{1} ⩽ x \to x = x_{1}) \land el (x_{1}, x_{2}, \dots, x_{n})$ . $F_{α} ⊧ max (a_{1}, \dots, a_{n})$ if and only if $a_{1}, \dots, a_{n}$ are all $(α)$ -words (as opposed to $(β)$ -words for some $β < α$ ).

We now prove the hard direction of the main theorem for the cases where α is countable. Afterwards we discuss the other cases.

Lemma 4.6.

Let $α < ω_{1}$ . For each $(α)$ -automaton $A$ over alphabet $Σ^{k}$ , there is a formula $φ_{A} (x_{1}, \dots, x_{k})$ such that $F_{α} ⊧ φ_{A} (w_{1}, \dots, w_{k})$ if and only if $(w_{1}, \dots, w_{k}) \in L (A)$ .

Proof.

In the following we describe an encoding of a run r on an $(α)$ -word w (over alphabet $Σ^{i}$ for some $i \in N$ ) of some automaton $A = (Q, Σ^{k}, I, F, Δ)$ with $| Q | = m$ . We identify Q with a subset of $Σ^{l}$ for an appropriate l. There are an $n ⩽ | supp (w) |$ (see Definition 3.1 for the support $supp (w)$ of w) and (ordinal) positions $\begin{matrix} 0 = p_{0} ⩽ p_{1} < p_{2} < p_{3} < p_{4} < \dots < p_{2 n - 1} < p_{2 n} < p_{2 n + 1} = α \end{matrix}$ such that $\begin{matrix} supp (w) = [p_{1}, p_{2}) \cup [p_{3}, p_{4}) \cup \dots \cup [p_{2 n - 1}, p_{2 n}) \end{matrix}$ and $w ↾_{[p_{2 i}, p_{2 i + 1})}$ is an empty word for all $0 ⩽ i ⩽ n$ .

Each $p_{2 i + 1}$ decomposes as $\begin{matrix} p_{2 i + 1} = p_{2 i} + ω^{m} \cdot γ_{i} + ω^{m - 1} \cdot c_{i, m - 1} + \dots + ω \cdot c_{i, 1} + c_{i, 0}, \end{matrix}$ where $c_{i, j} \in N$ and $γ_{i}$ some ordinal. We encode a run r of $A$ on w by an $(α)$ -word $r_{f}$ such that $\begin{matrix} r ↾_{supp (r_{f})} = r_{f} ↾_{supp (r_{f})} \end{matrix}$ and $supp (r_{f})$ is given by the following rules.

For all $1 ⩽ i ⩽ n$ , $\begin{matrix} supp (r_{f}) \cap [p_{2 i - 1}, p_{2 i}) = [p_{2 i - 1}, p_{2 i}) (= supp (r) \cap [p_{2 i - 1}, p_{2 i})) \end{matrix}$

For all $0 ⩽ i ⩽ n$ , $supp (r_{f}) \cap [p_{2 i}, p_{2 i + 1})$ consists of

$p_{2 i}$ ,

$p_{2 i} + ω^{m} γ_{i}$ if there is a $0 ⩽ k ⩽ m - 1$ such that $c_{i, k} \neq 0$ (i.e., $p_{2 i} + ω^{m} γ_{i} < p_{2 i + 1}$ ),

and all $\begin{matrix} p_{2 i} + ω^{m} \cdot γ_{i} + ω^{m - 1} \cdot c_{i, m - 1} + \dots + ω^{k + 1} \cdot c_{i, k + 1} + ω^{k} j \end{matrix}$ for all $0 ⩽ k < m$ and all $0 ⩽ j < c_{i, k}$ .

We define a formula

\begin{matrix} φ (\bar{w}) = \exists \bar{q} (max (\bar{w}, \bar{q}) \land R_{supp} (\bar{w}, \bar{q}) \land R (\bar{w}, \bar{q}) \land S (\bar{q}) \land A (\bar{q})) \end{matrix}

such that

F_{α} ⊧ φ (\bar{w})

if and only if

\bar{w} \in R

. If this formula is satisfied, every witness

\bar{r}

for the quantification

\exists \bar{q}

is some word

r_{f}

corresponding to some accepting run r of

A

\bar{w}

. Let us explain S, A,

R_{supp}

and R.

S states that $\bar{q} (0)$ is an initial state of $A$ : $S (\bar{q}) = \exists p (\forall z (\neg z ⊏ p) \land ⋁_{i \in I} {Sm}_{i} (\bar{q}, p))$ .

$R_{supp}$ expresses that $supp (\bar{q}) = supp (r_{f})$ for an encoding $r_{f}$ of an arbitrary run r of $A$ on $\bar{w}$ . Note that the following set is exactly $supp (r_{f})$ and that it is easy to translate our description into a formula that defines this set: $\begin{array}{l} supp (w) \cup {p ∣ \exists p^{'} \in supp (w) p = p^{'} + 1} \\ \cup {p | \exists p^{'} \forall p^{″} (p ⊏ p^{'} \land p^{'} \in supp (\bar{w}) \land lim_{⩾ m} (p) \land (p ⊏ p^{″} ⊑ p^{'} \to \neg lim_{⩾ m} (p^{″})))} \\ \cup ⋃_{0 ⩽ i < m} {p | \exists p^{'} \forall p^{″} (p ⊏ p^{'} \land p^{'} \in supp (\bar{w}) \land lim_{i} (p) \land (p ⊏ p^{″} ⊑ p^{'} \to \neg lim_{⩾ i + 1} (p^{″})))} \\ \cup {p | \exists p^{'} \forall p^{″} (lim_{⩾ m} (p) \land (p ⊏ p^{″} \to \neg lim_{⩾ m} (p^{″})) \land (p^{'} ⊏ p^{″} \to \neg lim_{⩾ m - 1} (p^{″})))} \\ \cup ⋃_{0 ⩽ i < m} {p | \exists p^{'} \forall p^{″} (lim_{i} (p) \land (p ⊏ p^{″} \to \neg lim_{⩾ i + 1} (p^{″})) \land (p^{'} ⊏ p^{″} \to \neg lim_{⩾ i} (p^{″})))} . \end{array}$ Let us briefly sketch why this set is equal to $supp (r_{f})$ for any run r on $\bar{w}$ . The first line describes the positions in $[p_{2 i - 1}, p_{2 i}]$ for $1 ⩽ i ⩽ n$ . The second line puts $p_{2 i} + ω^{m} \cdot γ_{i}$ for each $0 ⩽ i < n$ into the set. The third line puts elements of the form $\begin{matrix} p_{2 i} + ω^{m} \cdot γ_{i} + ω^{m - 1} \cdot c_{i, m - 1} + \dots + ω^{k + 1} \cdot c_{i, k + 1} + ω^{k} j \end{matrix}$ for all $i < n$ $0 ⩽ k < m$ and all $0 ⩽ j < c_{i, k}$ . The last two lines do the same as the second and third but with respect to the position $p_{2 n}$ . The main difference is that position α is not available in $F_{α}$ . In order to understand the last two lines first note that $\exists p^{'} \forall p^{″} (p^{'} ⊏ p^{″} \to \neg {lim}_{⩾ i} (p^{″}))$ is satisfied in $F_{α}$ if and only if $α \neq ω^{i + 1} \cdot α^{'}$ for some ordinal $α^{'}$ . Thus, if $α \neq ω^{m} \cdot α^{'}$ for some $α^{'}$ , the third line collects the position $p = ω^{m} \cdot β$ for the maximal β such that $p < α$ . Otherwise this third set is empty. Analogously, the last set contains all i-limits p such that $p + ω^{i} c ⩾ α$ for some constant $c \in N$ .

R is a formula that expresses that the states of $\bar{q}$ are compatible with the transition relation. If $p, p + 1 \in supp (\bar{q})$ this requires that there is a successor transition $δ = (\bar{q} (p), \bar{w} (p), \bar{q} (p + 1))$ : $\begin{matrix} \forall y ({Next}_{0} (x, y) \to \underset{(q, σ, q^{'}) \in Δ_{s}}{⋁} {Sm}_{q} (\bar{q}, x) \land {Sm}_{σ} (\bar{w}, x) \land {Sm}_{q^{'}} (\bar{q}, y)) . \end{matrix}$ Now for each $1 ⩽ m^{'} < m$ note that for $p < α$ and $p^{'} = p + ω^{m^{'}}$ we have that $p^{'}$ is the direct successor of p in $supp (\bar{q})$ if and only if $p^{'}$ is an $m^{'}$ -limit and $\bar{w} ↾_{[p, p^{'})} = ◇^{ω^{m^{'}}}$ . Let $Q_{m} \subseteq Q \times Q$ be the list of tuples $(q_{1}, q_{2})$ such that there is a run $r^{'} : q_{1} \overset{◇^{ω^{m^{'}}}}{\underset{A}{⟶}} q_{2}$ . We say that $(\bar{q} (p), \bar{q} (p^{'}))$ are compatible with Δ if $(\bar{q} (p), \bar{q} (p^{'})) \in Q_{m}$ . For each $m^{'} < m$ there is a formula $φ_{m^{'}} (\bar{q})$ which is satisfied if all positions in $supp (\bar{q})$ of distance $ω^{m^{'}}$ are compatible with Δ. Let $\begin{array}{l} ϵ (p, p^{'}, \bar{q}) = (p ⊏ p^{'} \land \underset{σ \neq ◇}{⋁} {Sm}_{σ} (\bar{q}, p) \land \underset{σ \neq ◇}{⋁} {Sm}_{σ} (\bar{q}, p^{'}) \land (\forall p^{″} (p ⊏ p^{″} ⊏ p) \to {Sm}_{◇} (\bar{q}, p))), \\ φ_{m^{'}} = \forall p \forall p^{'} ((lim_{m^{'}} (p^{'}) \land ϵ (p, p^{'}, \bar{q})) \to \underset{(q_{1}, q_{2}) \in Q_{m^{'}}}{⋁} {Sm}_{q_{1}} (\bar{q}, p) \land {Sm}_{q_{2}} (\bar{q}, p^{'})), \end{array}$ where $ϵ (p, p^{'}, \bar{q})$ states that $\bar{q}$ is defined at p and $p^{'}$ but undefined between p and $p^{'}$ .

Finally, we have to provide a formula $φ_{m}$ dealing with the k-limits in $supp (\bar{q})$ for $k ⩾ m$ . Let $\begin{array}{l} φ_{m} = \forall p \forall p^{'} ((lim_{⩾ m} (p^{'}) \land ϵ (p, p^{'}, \bar{q})) \to \underset{(q_{1}, q_{2}) \in Q_{m}}{⋁} {Sm}_{q_{1}} (\bar{q}, p) \land {Sm}_{q_{2}} (\bar{q}, p^{'})) . \end{array}$ We claim that this formula expresses compatibility of a pair $(\bar{q} (p), \bar{q} (p^{'}))$ for p, $p^{'}$ direct successors in $supp (\bar{q})$ of distance $ω^{m} \cdot γ$ for any ordinal $γ ⩾ 1$ of countable cofinality. For $γ = 1$ the reasoning is as in the case of $φ_{m^{'}}$ . For $γ > 1$ we use Proposition 3.6: there is a run on empty input of length $ω^{m} \cdot γ$ if and only if there is a run with the same initial and final state and the same image on the empty input of length $ω^{m}$ .

The definition of A depends on α as follows

If $α = ω^{m} \cdot γ$ for some $γ > 0$ , let $A (\bar{q})$ state that $\bar{q} (max supp (\bar{q}))$ is a state $q_{1}$ such that there is a final state f such that $(q_{1}, f) \in Q_{m}$ . In this case $[max supp (\bar{q}), α)$ is isomorphic to $ω^{m} \cdot γ^{'}$ for some $γ^{'} > 0$ . Using the pumping lemma again, we conclude that $A (\bar{q})$ holds if and only if there is a run $q_{1} \overset{◇^{ω^{m} γ^{'}}}{\underset{A}{⟶}} f$ for $q_{1} = \bar{q} (max (supp (\bar{q})))$ and f some final state.

If $\begin{matrix} α = ω^{m} \cdot γ + ω^{m - 1} k_{m - 1} + \dots + ω^{j} k_{j} \end{matrix}$ with $k_{j} \neq 0$ , let $A (\bar{q})$ state that $\bar{q} (max supp (\bar{q}))$ is a state $q_{1}$ such that there is a final state f such that $(q_{1}, f) \in Q_{j}$ . Note that in this case $p^{'} : = max (supp (\bar{q}))$ satisfies $\begin{matrix} p^{'} = α = ω^{m} \cdot γ + ω^{m - 1} k_{m - 1} + \dots + ω^{j} (k_{j} - 1) \end{matrix}$ we conclude that $A (\bar{q})$ holds if and only if there is a run $q_{1} \overset{◇^{[p^{'}, α)}}{\underset{A}{⟶}} f$ for $q_{1} = \bar{q} (p^{'})$ and f some final state. □

Our proof can easily be adapted for every ordinal α with $ω_{1} ⩽ α < ω_{1} + ω^{ω}$ as follows.

If $α = ω_{1}$ everything can be done as before, except that we have to adapt A. In this case for any coding $r_{f}$ of a run, the interval $[max (supp (r_{f})), α)$ is of the form $ω_{1}$ . Since $ω_{1}$ has uncountable cofinality, not all runs on $◇^{ω^{m}}$ can be translated to runs on $◇^{ω_{1}}$ . Nevertheless we can compute all the possible pairs of initial and final states of runs on empty input of length $ω_{1}$ and hardcode these into A instead of the set $Q_{m}$ .

If $ω_{1} < α < ω_{1} + ω^{z}$ for some $z \in N$ , we can copy everything from the countable case except for one thing: given a word $r_{f}$ , it might happen that $ω_{1} \in supp (r_{f})$ . In this case, there are two positions $p_{1}, p_{2} \in supp (r_{f})$ such that they satisfy $ε (p_{1}, p_{2}, \bar{q})$ and $[p_{1}, p_{2})$ is of order type $ω_{1}$ . For this case we have to add a conjunction to R that requires that the states $q_{1} = \bar{q} (p_{1})$ and $q_{2} = \bar{q} (p_{2})$ satisfy that there is a run of the automaton from state $q_{1}$ to state $q_{2}$ on input $◇^{ω_{1}}$ . Since all those pairs are computable and the position $p_{2}$ where this happens is the maximal $(z + 1)$ -limit in α, this can easily be done. Remark 4.1.

In fact, we can also define complete structures for all $α ⩾ ω_{1} + ω^{ω}$ . Let $F_{α}^{'}$ be the expansion of $F_{α}$ by a unary predicate $CoCo$ (“countable cofinality”) such that $F_{α}^{'} ⊧ p \in CoCo$ if and only if p is a $(β)$ -word for some β of countable cofinality. Using this predicate, we can extend the definition of R to distinguish whether a gap of the form $ω^{m} \cdot α^{'}$ in $supp (r_{f})$ has countable or uncountable cofinality and require the states to correspond to a run on empty input of length $ω^{m}$ or $ω_{1}$ respectively. Moreover, if α itself has uncountable cofinality we have to adapt the definition of A as in the case of $α = ω_{1}$ . But recall that for $α ⩾ ω_{1} + ω^{ω}$ , the class of $(α)$ -automatic structures is probably not closed under first-order definable relations which turns this result less interesting.

5. Growth lemmas for ordinal-automatic structures

A relation $R \subseteq X \times Y$ is called locally finite if for every $x \in X$ , there are at most finitely many $y \in Y$ with $(x, y) \in R$ . In the following, we first characterise the branching degree of locally finite $(α)$ -automatic relations. We first define a function $U_{m}$ that computes, on input the support of (the representation) of some $x \in X$ , an upper bound on the support of (the representation of) any $y \in Y$ such that $(x, y) \in R$ for any locally finite $(α)$ -automatic relation whose automata has less than m states.

Definition 5.1.
Let $\begin{matrix} β = β_{\sim m} + ω^{m} n_{m} + ω^{m - 1} n_{m - 1} + \dots + n_{0} \end{matrix}$ be an ordinal and X a finite set of ordinals. Let us define the following sets.
Let $U_{m} (β)$ denote the set of ordinals $γ = β_{\sim m} + ω^{m} l_{m} + ω^{m - 1} l_{m - 1} + \dots + l_{0}$ such that either
$γ = β$ or

$l_{k} ⩽ n_{k} + m$ and $l_{i} ⩽ m$ for all $i < k$ ,
where k is maximal with $l_{k} \neq n_{k}$ .

Let $U_{m} (X) = ⋃_{γ \in X \cup {0}} U_{m} (γ)$ .

Let $U_{m} (X, δ) = U_{m} (X \cup {δ}) \cap δ$ be those elements of $U_{m} (X \cup {δ})$ that are strictly below δ.

Let $U_{m}^{1} (X) = U_{m} (X)$ and $U_{m}^{i + 1} (X) = U_{m} (U_{m}^{i} (X))$ for $i \in N$ , and similarly let $U_{m}^{1} (X, δ) = U_{m} (X, δ)$ and $U_{m}^{i + 1} (X, δ) = U_{m} (U_{m}^{i} (X, δ), δ)$ for $i \in N$ .

A rough upper bound for the sizes of these sets is provided in the next lemma. In this lemma, we use the following abbreviations (where as before X is a finite set of ordinals and $β = β_{\sim m} + ω^{m} n_{m} + ω^{m - 1} n_{m - 1} + \dots + n_{0}$ ).

$c_{m} (β) = {max}_{i ⩽ m} n_{i}$ ,

$c_{m} (X) = {max}_{γ \in X \cup {0}} c_{m} (γ)$ (we add 0 to be well-defined if X is empty), and

$d_{m} (X) = | {γ_{\sim m} ∣ γ \in X \cup {0}} |$ .
Lemma 5.2.
Suppose that X is a finite set of ordinals and $i, n ⩾ 1$ . Then $\begin{array}{l} | U_{m}^{i} (X) | ⩽ {(c_{m} (X) + i m)}^{m + 1} d_{m} (X), \\ | U_{m}^{i} (X, α) | ⩽ {(c_{m} (X \cup {α}) + i m)}^{m + 1} d_{m} (X \cup {α}) and \\ | U_{m}^{i} (X, ω^{n}) | ⩽ {(c_{m} (X) + i m)}^{n} . \end{array}$
Proof.
The coefficient of $ω^{j}$ of an element of $U_{m}^{i} (γ)$ can take at most $(c_{m} (w) + i m)$ many different values for any fixed $j ⩽ m$ . Hence $| U_{m}^{i} (γ) | ⩽ {(c_{m} (w) + i m)}^{m + 1}$ for all $i ⩾ 1$ . Moreover $d_{m} (U_{m}^{i} (X)) = d_{m} (X)$ for all $i ⩾ 1$ .

Finally, note that $U_{m}^{i} (X, ω^{k})$ only contains ordinals of the form $\begin{matrix} 0 + ω^{m} 0 + ω^{m - 1} 0 + \dots + ω^{k} 0 + ω^{k - 1} l_{k - 1} + ω^{k - 2} l_{k - 2} + \dots + l_{0}, \end{matrix}$ where the same restrictions on the $l_{j}$ apply as before. □

It follows that there are at most $| Σ |^{{(c_{m} (X) + i m)}^{m + 1} d_{m} (X)}$ $(α)$ -words w over alphabet Σ with $supp (w) \subseteq U_{m}^{i} (X)$ for $i ⩾ 1$ .
Lemma 5.3 (Growth lemma).

Let $R \subseteq {(Σ^{(α)})}^{k} \times {(Σ^{(α)})}^{l}$ be a locally finite relation of $(α)$ -words which is recognizable by some $(α)$ -automaton $A$ with at most m states. Then $supp (w) \subseteq U_{m + 1} (supp (v), α)$ for all $(v, w) \in R$ .

Proof.
Heading for a contradiction, fix an accepting run r of $A$ on $(v, w) \in R$ and assume that $\begin{matrix} supp (w) ∖ U_{m + 1} (supp (v), α) \neq \emptyset . \end{matrix}$ Let $β \in supp (w) ∖ U_{m + 1} (supp (v), α)$ be minimal. We aim at proving the following three claims.
There is a $γ \in supp (v) \cup {0, α}$ such that $\begin{matrix} β ⩽ γ < β + ω^{m + 1} or γ ⩽ β < γ + ω^{m + 1}, \end{matrix}$ i.e., $β_{\sim m} = γ_{\sim m}$ .

We prepare some notation for the second claim. Let $k ⩽ m$ be least such that there is some $δ \in supp (w) \cup {0, α}$ such that $\begin{matrix} β ⩽ δ < β + ω^{k + 1} or δ ⩽ β < δ + ω^{k + 1} . \end{matrix}$ For this fixed k, let γ be maximal with this property. By choice of k, $β_{\sim k} = γ_{\sim k}$ and there are natural numbers $n_{0}, n_{1}, \dots, n_{k}$ and $l_{0}, l_{1}, \dots, l_{k}$ such that $\begin{array}{l} β = β_{\sim k} + ω^{k} n_{k} + \dots + ω^{1} n_{1} + n_{0} and \\ γ = γ_{\sim k} + ω^{k} l_{k} + \dots + ω^{1} l_{1} + l_{0} . \end{array}$ We claim that either $n_{k} < l_{k}$ or $l_{k} < n_{k} ⩽ l_{k} + m$ .

$n_{0}, n_{1}, \dots, n_{k - 1}$ are all at most m.
Having proved these three claims, it follows immediately that $β \in U_{m + 1} (γ) \subseteq U_{m + 1} (supp (v), α)$ yielding the desired contradiction. We now prove the claims as follows.
Heading for a contradiction assume that $δ : = max (supp (v) \cup {0}) \cap β$ satisfies $\begin{array}{l} (1) & δ + ω^{m + 1} ⩽ β and assume that \\ (2) & [β, β + ω^{m + 1}) \cap (supp (v) \cup {0, α}) = \emptyset . \end{array}$ Note that (2) implies $β + ω^{m + 1} ⩽ α$ . Let η be minimal such that $[η, β + ω^{m + 1})$ is of order type $ω^{m + 1}$ . Since η is minimal, the order type of $[δ + 1, η)$ is $ω^{m + 1} δ^{'}$ for some ordinal $δ^{'} \neq 0$ . Recall that r is a fixed accepting run of $A$ on $(v, w)$ . Using the Shrinking Lemma 3.9 and then the Pumping Lemma 3.8 we can translate the run $r_{0} : = r ↾ [δ + 1, η)$ (on (a convolution of) empty words of length $ω^{m + 1} δ^{'}$ ) into a run $r_{i}$ on empty words of length $ω^{m} (ω δ^{'} + i)$ for each $i \in N$ . Note that replacing $r_{0}$ by $r_{i}$ in r results again in an accepting run of $A$ on some tuple of $(α)$ -words $(v_{i}, w_{i})$ because $\begin{matrix} [0, δ] + [δ + 1, η) + [η, β + ω^{m + 1}) = [0, δ] + [δ + 1, η) + ω^{m} \cdot n + [η, β + ω^{m + 1}) \end{matrix}$ For the same reason, $v_{i} = v$ for all $i \in N$ . On the other hand we show that $w_{i}$ differs from $w_{j}$ for all $i \neq j$ . Just recall that $[η, β + ω^{m + 1})$ is of order type $ω^{m + 1}$ whence there is some $n \in N$ such that $\begin{matrix} η + ω^{m} n ⩽ β < η + ω^{m} (n + 1) . \end{matrix}$ Since we obtain $w_{i}$ by inserting an empty word of length $ω^{m} \cdot i$ in w at η, it is straightforward to conclude that $β_{i} : = min (supp (w_{i}) ∖ U_{m + 1} (supp (v), α))$ satisfies $\begin{matrix} η + ω^{m} (n + i) ⩽ β_{i} < η + ω^{m} (n + i + 1) . \end{matrix}$ Note that we have constructed infinitely many $v_{i}$ such that $(w, v_{i}) \in R$ contradicting the fact that R is locally finite. Thus, we arrive at a contradiction and the first claim is proved.

Note that by minimality of k, $n_{k} = l_{k}$ is not possible. Heading for a contradiction assume that $n_{k} > l_{k} + m$ . This implies $γ \neq α$ whence we can conclude that $α ⩾ β + ω^{k + 1}$ . Thus, $(β, α)$ is isomorphic to $ω^{k + 1} \cdot δ_{1} + δ_{0}$ for ordinals $δ_{1} ⩾ 1$ and $δ_{0} ⩾ 0$ . In particular, for all $i \in N$ $\begin{matrix} [0, β_{\sim k}) + ω^{k} i + ω^{k} n_{k} + \dots + ω^{1} n_{1} + n_{0} + (β, α) \end{matrix}$ is of order type α again (the extra $ω^{k} \cdot i$ is absorbed by $(β, α)$ ). By maximality of γ, $w ↾_{(γ, β)}$ is the empty word. Moreover, there is a state s of $A$ and numbers $l_{k} < i_{0} < i_{1} ⩽ l_{k} + m + 1 ⩽ n_{k}$ such that $\begin{matrix} r (β_{\sim k} + ω^{k} i_{0}) = r (β_{\sim k} + ω^{k} i_{1}) . \end{matrix}$ Let $r_{0} = r$ and let $r_{i + 1}$ be obtained from $r_{i}$ by inserting $r ↾_{[β_{\sim k} + ω^{k} i_{0}, β_{\sim k} + ω^{k} i_{1})}$ at $β_{\sim k} + ω^{k} i_{1}$ . For each $i \in N$ , $r_{i}$ is an accepting run of $A$ on a tuple $(v_{i}, w_{i})$ of $(α)$ -words. Since γ has been chosen as the maximal element of $supp (v) \cup {0}$ in the $ω^{k + 1}$ copy of β, we immediately conclude that $v_{i} = v$ . Moreover, $w_{i} \neq w_{j}$ if $i < j$ because either $w ↾_{[β_{\sim k} + ω^{k} i_{0}, β_{\sim k} + ω^{k} i_{1})}$ is empty and $\begin{array}{l} w_{i} (γ_{\sim k} + ω^{k} (n_{k} + {(i_{1} - i_{0})}^{i}) + \dots + ω^{1} n_{1} + n_{0}) = w (β) \in supp (w) while \\ w_{j} (γ_{\sim k} + ω^{k} (n_{k} + {(i_{1} - i_{0})}^{i}) + \dots + ω^{1} n_{1} + n_{0}) = ◇, \end{array}$ or $w ↾_{[β_{\sim k} + ω^{k} i_{0}, β_{\sim k} + ω^{k} i_{1})}$ is nonempty whence $| supp (w_{j}) | > | supp (w_{i}) |$ . Note that we have constructed infinitely many $v_{i}$ such that $(w, v_{i}) \in R$ contradicting the fact that R is locally finite. Thus, we arrive at a contradiction and the second claim is proved.

Let $i \in {0, \dots, k - 1}$ . By minimality of k, $\begin{array}{l} v ↾_{[β_{\sim (i + 1)} + ω^{i + 1} n_{i + 1}, β_{\sim (i + 1)} + ω^{i + 1} (n_{i + 1} + 1))} \end{array}$ is an empty word. If $n_{i} > m$ , some state s occurs in $\begin{matrix} r ↾_{[β_{\sim (i + 1)} + ω^{i + 1} n_{i + 1}, β_{\sim (i + 1)} + ω^{i + 1} n_{i + 1} + ω^{i} n_{i})} \end{matrix}$ at two positions in different $ω^{i}$ copies. The subrun between these positions can be iterated as before and yields infinitely many $w_{i}$ such that $(v, w_{i}) \in R$ .
Putting all results together, we proved that $γ_{\sim k} = β_{\sim k}$ , $n_{k} \neq l_{k}$ , $n_{k} ⩽ l_{k} + m$ , and $n_{j} ⩽ m$ for all $0 ⩽ j < k$ . This implies $β \in U_{m + 1} (γ) \subseteq U_{m + 1} (v, α)$ contradicting the assumptions on β. Thus, $supp (w) ∖ U_{m + 1} (v, α) = \emptyset$ . □

For some real number x, let $⌈ x ⌉$ denote the least $n \in ω$ with $x ⩽ n$ , and log the logarithm with base 2.
Lemma 5.4 (Growth lemma for semigroups).

Suppose the multiplication of the semigroup $(S, \cdot)$ is recognised by an $(α)$ -automaton with at most m states. Suppose $s_{1}, \dots, s_{n} \in S$ and $supp (s_{i}) \subseteq X$ for $1 ⩽ i ⩽ n$ where $n ⩾ 2$ . Then $supp (s_{1} \dots s_{n}) \subseteq U_{m + 1}^{⌈ log n ⌉} (X, α)$ .

Proof.
We follow the proof of [22, Lemma 3.2]. The statement follows from the Growth Lemma for $n ⩽ 2$ . For $n > 2$ let $k = ⌈ \frac{n}{2} ⌉$ and $l = n - k$ . Then $⌈ log k ⌉, ⌈ log l ⌉ < ⌈ log n ⌉$ . Let $t = s_{1} \cdot \dots \cdot s_{k}$ and $u = s_{k + 1} \cdot \dots \cdot s_{n}$ . Then $supp (t) \cup supp (u) \subseteq U_{m + 1}^{⌈ log n ⌉ - 1} (X)$ by the induction hypothesis for $⌈ \frac{n}{2} ⌉$ . Thus, $supp (t \cdot u) \subseteq U_{m + 1}^{⌈ log n ⌉} (X, α)$ by the Growth Lemma applied to t and u. □

We give a variant of the growth lemma that turns out to be very useful in the setting of noninjective presentations of structures with functions, e.g. groups. Instead of using pumping to generate many words related to a fixed one, we now use shrinking in order to get a small element related to a given one. This lemma can be seen as a weak variant of Delhommé’s relative growth arguments [7] for ordinal-automatic structures. Lemma 5.5 (Inverse growth lemma).

Let $A$ be an $(α)$ -automaton with $m^{'}$ states and let w, v be finite $(α)$ -words such that $A$ accepts $(w, v)$ . Setting $m : = m^{'} + 2$ , there is a word $v^{'}$ such that $supp (v^{'}) \in U_{m} (supp (w), α)$ and $A$ accepts $(w, v^{'})$ .

Proof.
Let r be an accepting run of $A$ on $(w, v)$ .

Assume that $\begin{matrix} β = min (supp (v) ∖ U_{m} (supp (w), α)) \end{matrix}$ exists. Using pumping and shrinking inductively, we can transform v into a word $v^{'}$ such that $A$ accepts $(w, v^{'})$ and $supp (v^{'}) \subseteq U_{m} (supp (w), α)$ . For this purpose, we define $\begin{array}{l} γ = max ((supp (w) \cap β) \cup {0}) and \\ δ = min ((supp (w) \cap [β, α)) \cup {α}) . \end{array}$ We have an outer induction on the size of $supp (v) ∖ U_{m} (supp (w) \cup {α})$ and an inner (transfinite) induction on the size of $[γ, β)$ . The inductive step is a tedious case distinction on the shapes of $[γ, β)$ and $[β, δ)$ . Let us fix natural numbers $b_{i}$ , $c_{i}$ , $d_{i}$ , $0 ⩽ i ⩽ m$ such that $\begin{array}{l} β = β_{\sim m} + ω^{m} b_{m} + ω^{m - 1} b_{m - 1} + \dots + b_{0}, \\ γ = γ_{\sim m} + ω^{m} c_{m} + ω^{m - 1} c_{m - 1} + \dots + c_{0}, and \\ δ = δ_{\sim m} + ω^{m} d_{m} + ω^{m - 1} d_{m - 1} + \dots + d_{0} . \end{array}$ Since $β \notin U_{m} (γ)$ and $γ ⩽ β$ , one of the following holds.
$β_{\sim m} > γ_{\sim m}$ ,

$β_{\sim m} = γ_{\sim m}$ , $c_{m} = b_{m}$ , $\dots$ , $c_{k + 1} = b_{k + 1}$ , and $c_{k} + m < b_{k}$ , or

$β_{\sim m} = γ_{\sim m}$ , $c_{m} = b_{m}$ , $\dots$ , $c_{k + 1} = b_{k + 1}$ , and $c_{k} < b_{k} ⩽ c_{k} + m$ and there is a maximal $k^{'} < k$ such that $b_{k^{'}} > m$ .
Since $β \notin U_{m} (δ)$ and $β ⩽ δ$ , one of the following holds.
$β_{\sim m} < δ_{\sim m}$ or

$β_{\sim m} = δ_{\sim m}$ , $d_{m} = b_{m}$ , $\dots$ , $d_{i + 1} = b_{i + 1}$ , and $b_{i} < d_{i}$ and there is a maximal $i^{'} < i$ such that $b_{i^{'}} > m$ .
This leads to the following cases.
Set $\begin{array}{l} γ^{'} = max ((supp (w) \cup supp (v)) \cap β_{\sim m}) + 1 and \\ δ^{'} = max (supp (v) \cap δ_{\sim m}) + 1 . \end{array}$ By minimality of β and maximality of γ, $γ_{\sim m}^{'} = γ_{\sim m}$ . Hence $[γ^{'}, β_{\sim m})$ is of shape $ω^{m + 1} η_{1}$ for some ordinal $η_{1} ⩾ 1$ . By definition of $δ^{'}$ , $[δ^{'}, δ_{\sim m})$ is of shape $ω^{m + 1} η_{2}$ for some ordinal $η_{2} ⩾ 1$ . Choose an ordinal η such that $[β_{\sim m}, δ^{'}) + η$ is isomorphic to $[γ^{'}, δ_{\sim m})$ and define $\begin{matrix} v^{'} : = v ↾_{[0, γ^{'})} + ◇^{ω^{m^{'} + 1}} + v ↾_{[β_{\sim m}, δ^{'})} + ◇^{η} + v ↾_{[δ_{\sim m}, α)} . \end{matrix}$ We claim that $(w, v^{'})$ is accepted by $A$ . Application of the Shrinking Lemma 3.9 to $r ↾_{[γ^{'}, β_{\sim m})}$ yields a run $r_{1}$ of $A$ on $◇^{ω^{m^{'} + 1}}$ with the same initial and final states as $r ↾_{[γ^{'}, β_{\sim m})}$ . Application of Pumping (depending on whether $δ_{\sim m}$ has countable cofinality, Proposition 3.6 or Proposition 3.7) to $r ↾_{[δ^{'}, δ_{\sim m})}$ yields a run $r_{2}$ of $A$ on $◇^{η}$ with the same initial and final states as $r ↾_{[δ^{'}, δ_{\sim m})}$ . Since $w ↾_{[γ^{'}, δ_{\sim m})}$ is an empty word, the composition of $r ↾_{[0, γ^{'})}$ , $r_{1}$ , $r ↾_{[β_{\sim m}, δ^{'})}$ , $r_{2}$ , and $r ↾_{[δ_{\sim m}, α]}$ is an accepting run of $A$ on $(w, v^{'})$ .

One concludes easily that either $\begin{matrix} | supp (v^{'}) ∖ U_{m} (supp (w) \cup {α}) | < | supp (v) ∖ U_{m} (supp (w) \cup {α}) | \end{matrix}$ or $\begin{matrix} | supp (v^{'}) ∖ U_{m} (supp (w) \cup {α}) | = | supp (v) ∖ U_{m} (supp (w) \cup {α}) | \end{matrix}$ and $v^{'}$ satisfies the conditions of cases 2 + i or 3 + i.

Note that $w ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i} b_{i}, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i} (b_{i} + 1))}$ is the empty word. Since $b_{i^{'}} > m^{'}$ we can find $n_{1} < n_{2} < b_{i^{'}}$ such that $\begin{matrix} r (β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i^{'} + 1} b_{i^{'} + 1} + ω^{i^{'}} n_{1}) = r (β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i^{'} + 1} b_{i^{'} + 1} + ω^{i^{'}} n_{2}) . \end{matrix}$ Thus, the composition of $\begin{matrix} r ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i^{'} + 1} b_{i^{'} + 1} + ω^{i^{'}} n_{1})} and r ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i^{'} + 1} b_{i^{'} + 1} + ω^{i^{'}} n_{2}, α]} \end{matrix}$ is an accepting run on $\begin{matrix} (w, v ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i^{'} + 1} b_{i^{'} + 1} + ω^{i^{'}} n_{1})} + v ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{i^{'} + 1} b_{i^{'} + 1} + ω^{i^{'}} n_{2}, α)}) \end{matrix}$ and we can conclude by induction hypothesis.

In this case, there are natural numbers $c_{k} < n_{1} < n_{2} ⩽ b_{k}$ such that $\begin{matrix} r (β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k + 1} b_{k + 1} + ω^{k} n_{1}) = r (β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k + 1} b_{k + 1} + ω^{k} n_{2}) . \end{matrix}$ Thus, the composition of $\begin{matrix} r ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k + 1} b_{k + 1} + ω^{k} n_{1})} and r ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k + 1} b_{k + 1} + ω^{k} n_{2}, α]} \end{matrix}$ is an accepting run on $\begin{matrix} (w, v ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k + 1} b_{k + 1} + ω^{k} n_{1})} + v ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k + 1} b_{k + 1} + ω^{k} n_{2}, α)}) \end{matrix}$ and we can conclude by induction hypothesis.

Set $j = min (k, i^{'})$ and $\begin{matrix} e_{j} : = \{\begin{matrix} c_{k} + 1 & if j = k, \\ 0 & if j < k . \end{matrix} \end{matrix}$ Note that $b_{j} ⩾ e_{j} + m^{'}$ and that $w ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} e_{j}, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} (b_{j + 1} + 1))}$ is empty. Thus, there are $e_{j} ⩽ n_{1} < n_{2} ⩽ b_{j}$ such that the composition of $\begin{matrix} r ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{1})} and r ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{2}, α]} \end{matrix}$ is an accepting run on $\begin{matrix} (w, v ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{1})} + v ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{2}, α)}) \end{matrix}$ and we can conclude by induction hypothesis.

Note that $w ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k^{'} + 1} b_{k^{'} + 1}, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k^{'} + 1} (b_{k^{'} + 1} + 1))}$ is empty. There are $n_{1} < n_{2} ⩽ b_{k^{'}}$ such that the composition of $\begin{matrix} r ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k^{'} + 1} b_{k^{'} + 1} + ω^{k^{'}} n_{1})} and r ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k^{'} + 1} b_{k^{'} + 1} + ω^{k^{'}} n_{2}, α]} \end{matrix}$ is an accepting run on $\begin{matrix} (w, v ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k^{'} + 1} b_{k^{'} + 1} + ω^{k^{'}} n_{1})} + v ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{k^{'} + 1} b_{k^{'} + 1} + ω^{k^{'}} n_{2}, α)}) \end{matrix}$ and we can conclude by induction hypothesis.

Set $j = min (k^{'}, i^{'})$ Note that $w ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1}, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} (b_{j + 1} + 1))}$ is empty. Thus, there are $n_{1} < n_{2} ⩽ b_{j}$ such that the composition of $\begin{matrix} r ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{1})} and r ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{2}, α]} \end{matrix}$ is an accepting run on $\begin{matrix} (w, v ↾_{[0, β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{1})} + v ↾_{[β_{\sim m} + ω^{m} b_{m} + \dots + ω^{j + 1} b_{j + 1} + ω^{j} n_{2}, α)}) \end{matrix}$ and we can conclude by induction hypothesis. □

6. Ordinal automatic Boolean algebras

In this section, we classify completely the finite word $ω^{n}$ -automatic Boolean algebras. Moreover, we show that the countable atomless Boolean algebra does not have an injective finite-word ordinal-automatic presentation.

6.1. Basics on Boolean algebras

This section provides the necessary background on Boolean algebras. For more details, we refer the reader to [12,24].

Definition 6.1.
A Boolean algebra is an algebraic structure $A = (A, ⊔, ⊓, \overline{\cdot}, 0, 1)$ such that both $(A, ⊔, 0)$ and $(A, ⊓, 1)$ are idempotent commutative monoids, ⊔ and ⊓ distribute over each other, and $\overline{\cdot}$ is a unary operation satisfying the following identities for all $a, b \in A$ : $\begin{array}{l} \overline{\overline{a}} = a, a ⊓ \overline{a} = 0, a ⊔ \overline{a} = 1, \\ \overline{a ⊓ b} = \overline{a} ⊔ \overline{b}, \overline{a ⊔ b} = \overline{a} ⊓ \overline{b} . \end{array}$

The operations ⊔, ⊓ and $\overline{\cdot}$ are called union (or disjunction), intersection (or conjunction) and complement (or negation), respectively. Notice that $\overline{\cdot}$ is an involution and that the above axioms imply $\overline{0} = 1$ and $\overline{1} = 0$ .
Example 6.1.

Each Boolean algebra satisfying $0 = 1$ contains precisely one element and is called trivial. Clearly, there is – up to isomorphism – only one trivial Boolean algebra.

Let X be some arbitrary set. The power set algebra of X is the Boolean algebra $P (X) = (2^{X}, \cup, \cap,^{∁}, \emptyset, X)$ . If X is a singleton set, $P (X)$ models classical two-valued logic, where ∅ corresponds to “false” and X to “true”.

Let $L = (L, ⩽)$ be some linear ordering. The interval algebra of $L$ is the Boolean algebra $I_{L} = (I_{L}, \cup, \cap,^{∁}, \emptyset, L)$ , where $I_{L}$ is the set of all finite unions of half-open intervals of the form $[a, b) = {c \in L ∣ a ⩽ c < b}$ for $a \in L \cup {- \infty}$ and $b \in L \cup {\infty}$ , where $- \infty < a < \infty$ for each $a \in L$ .

For Boolean algebras $A$ and $B$ , their direct product $A \times B$ , whose domain is $A \times B$ and whose operations and constants are defined component-wise, is a Boolean algebra as well.

A useful technique to characterize Boolean algebras is to study the transfinite process of iteratively quotienting out their indecomposable elements. Formally, let $A = (A, ⊔, ⊓, \overline{\cdot}, 0, 1)$ be a Boolean algebra. A pair $(b, c) \in A \times A$ is a decomposition of $a \in A$ if $b ⊔ c = a$ , $b ⊓ c = 0$ and $b, c \neq 0$ . An atom of $A$ is a non-zero element which admits no decomposition.

An ideal of $A$ is a subset $I \subseteq A$ such that $0 \in I$ , $i ⊔ j \in I$ for all $i, j \in I$ , and $i ⊓ a \in I$ for all $i \in I$ and $a \in A$ . Any ideal I of $A$ induces a congruence $\equiv_{I}$ on $A$ which is defined by $a \equiv_{I} b$ if $a △ b \in I$ , where $a △ b = (a ⊓ \overline{b}) ⊔ (\overline{a} ⊓ b)$ is the symmetric difference (or exclusive disjunction) of a and b. The corresponding quotient algebra – which is again a Boolean algebra – is denoted by $A / I$ and its elements by ${[a]}_{I}$ for $a \in A$ . If I is an ideal of $A$ and J is an ideal of $A / I$ , then the set $\begin{matrix} I \circ J = {a \in A ∣ {[a]}_{I} \in J} \end{matrix}$ is an ideal of $A$ with $I \circ J \supseteq I$ and the quotient algebras $A / I \circ J$ and $(A / I) / J$ are isomorphic via mapping ${[a]}_{I \circ J}$ to ${[{[a]}_{I}]}_{J}$ .

The set $\begin{matrix} F (A) = {a_{1} ⊔ \dots ⊔ a_{n} ∣ n ⩾ 0 and a_{1}, \dots, a_{n} \in A are atoms} \end{matrix}$ is an ideal of $A$ , called the Frechét ideal of $A$ . In fact, it is the smallest ideal of $A$ containing all its atoms. For each ordinal α, the iterated Frechét ideal $F_{α} (A)$ is defined as follows, where λ is a limit ordinal: $\begin{array}{l} F_{0} (A) = {0}, F_{α + 1} (A) = F_{α} (A) \circ F (A / F_{α} (A)), F_{λ} (A) = ⋃_{α < λ} F_{α} (A) . \end{array}$ Observe that $F_{α} (A) \subseteq F_{β} (A)$ whenever $α ⩽ β$ and that there is always an ordinal α such that $F_{α} (A) = F_{β} (A)$ for all ordinals $β ⩾ α$ . The least such α is called ordinal type of $A$ and denoted by $o (A)$ . If $A$ is countable, then $o (A)$ is countable as well. The Boolean algebra $A$ is called superatomic in case that $F_{o (A)} (A) = A$ . If $A$ is non-trivial and superatomic, then $o (A)$ is a successor ordinal, say $o (A) = β + 1$ , and $A / F_{β} (A)$ is a finite Boolean algebra, say it has $m ⩾ 1$ atoms. In this situation, the pair $(β, m)$ is called (superatomicity) type of $A$ and denoted $type (A)$ . An example of a superatomic Boolean algebra of type $(β, m)$ is the interval algebra $I_{ω^{β} m}$ . Due to the following proposition, this is indeed the only countable example whenever $I_{ω^{β} m}$ is countable.
Proposition 6.2 ([12, Proposition 1.5.9]).

Two non-trivial countable superatomic Boolean algebras $A$ and $B$ are isomorphic if and only if $type (A) = type (B)$ .

If superatomic Boolean algebras are regarded as one end of the whole spectrum of Boolean algebras, the other end is populated by atomless Boolean algebras, i.e., those which do not contain any atoms at all. An example of a atomless Boolean algebra is the interval algebra $I_{(Q, ⩽)}$ of the rationals. Due to the following proposition, this is the only non-trivial countable example.

Proposition 6.3 ([12, Proposition 1.5.1]).

Any two non-trivial countable atomless Boolean algebras are isomorphic.

An alternate approach to Boolean algebras is based on partial orders. This is used in Lemma 6.8 below. In fact, every Boolean algebra $A = (A, ⊔, ⊓, \overline{\cdot}, 0, 1)$ induces a partial order ⊑ on A which is defined by $a ⊑ b$ if $a ⊔ b = b$ , or equivalently, $a ⊓ b = a$ . This partial order is compatible with ⊔ and ⊓, i.e., $a ⊔ b ⊑ a^{'} ⊔ b^{'}$ and $a ⊓ b ⊑ a^{'} ⊓ b^{'}$ whenever $a ⊑ a^{'}$ and $b ⊑ b^{'}$ . Moreover, $0$ is its least element and $1$ its greatest element. An element $a \in A$ is an atom of $A$ precisely if $a \neq 0$ and there is no $b \in A$ such that $0 ⊏ b ⊏ a$ . Finally, the last condition on ideals, namely that $i ⊓ a \in I$ for all $i \in I$ and $a \in A$ , is equivalent to the requirement that $a ⊑ b$ and $b \in I$ implies $a \in I$ for all $a, b \in A$ .

6.2. Classification of the $(ω^{n})$ -automatic Boolean algebras

The objective of this section is to characterize the class of $(ω^{n})$ -automatic Boolean algebras, see Theorem 6.4 below. To this end, we extend the proof technique used in [22] to characterize the class of automatic Boolean algebras.

Theorem 6.4.
Let $A$ be a Boolean algebra and $n \in N$ . The following are equivalent:
$A$ is $(ω^{n})$ -automatic.

$A$ is isomorphic to the interval algebra $I_{α}$ for some ordinal $α < ω^{n + 1}$ .

$A$ is isomorphic to the direct product ${(I_{ω^{k}})}^{m}$ for some $k, m \in N$ with $k ⩽ n$ .

We show the implications (1. ⇒ 2.), (2. ⇒ 3.) and (3. ⇒ 1.) seperately. Aside from the case $α = 0$ , which leads to the trivial Boolean algebra $I_{0}$ , the implication (2. ⇒ 3.) is demonstrated by the proposition below.
Proposition 6.5.
For every ordinal $α > 0$ , the interval algebra $I_{α}$ is isomorphic to the direct product ${(I_{ω^{γ}})}^{m}$ for some $m ⩾ 1$ and an ordinal γ with $ω^{γ} ⩽ α$ .
Proof.
Using the Cantor normal form, we obtain a number $m ⩾ 1$ and two ordinals β, γ such that $α = ω^{γ} m + β$ and $β < ω^{γ}$ . Notice that for any two linear orderings $L_{1}$ and $L_{2}$ , the interval algebra $I_{L_{1} + L_{2}}$ is isomorphic to the direct product $I_{L_{1}} \times I_{L_{2}}$ via mapping M to $(M \cap L_{1}, M \cap L_{2})$ . Thus, $\begin{matrix} I_{α} ≅ I_{ω^{γ} m} \times I_{β} ≅ I_{β} \times I_{ω^{γ} m} ≅ I_{β + ω^{γ} m} = I_{ω^{γ} m} ≅ {(I_{ω^{γ}})}^{m} . \end{matrix}$ This proves the claim. □

Since the class of $(ω^{n})$ -automatic structures is closed under direct products, the implication (3. ⇒ 1.) of Theorem 6.4 is established by the following proposition.
Proposition 6.6.
Let $k \in N$ . The interval algebra $I_{ω^{k}}$ is $(α)$ -automatic for each ordinal $α ⩾ ω^{k}$ .
Proof.
We show that $I_{ω^{k}}$ is $(α)$ -automatic over the alphabet $Σ = {a, b, ◇}$ . Every set $M \in I_{α^{k}}$ can be uniquely written as $M = [a_{1}, b_{1}) \cup \dots \cup [a_{r}, b_{r})$ with $r ⩾ 0$ and $0 ⩽ a_{1} < b_{1} < a_{2} < b_{2} < \dots < a_{r} < b_{r} ⩽ ω^{k}$ . We encode this set M by the $(α)$ -word $u_{M} \in Σ^{(α)}$ defined by $u_{M} (β) = a$ if $β \in {a_{1}, \dots, a_{r}}$ , $u_{M} (β) = b$ if $β \in {b_{1}, \dots, b_{r}}$ , and $u_{M} (β) = ◇$ for all other β. Using the fact that an $(α)$ -automaton can identify the $(ω^{k})$ th position in any $(α)$ -word (cf. Lemma 3.14), it is a matter of routine to check that this encoding of $I_{α}$ induces an injectively $(α)$ -automatic presentation of $I_{α}$ . □

Finally, we turn to the implication (1. ⇒ 2.) of Theorem 6.4, whose proof needs some preparation. Basically, we have to investigate the connection between decompositions and iterated Frechét ideals as well as the $FO (\exists^{\infty})$ -definability of the latter.
Lemma 6.7.
Let $A$ be a Boolean algebra and α an ordinal. Any $a \in A ∖ F_{α + 1} (A)$ admits a decomposition $(b, c)$ such that $b \notin F_{α + 1} (A)$ and $c \notin F_{α} (A)$ .
Proof.
Let $I = F_{α} (A)$ and $B = A / I$ . Then $a \notin F_{α + 1} (A)$ can be rephrased as ${[a]}_{I} \notin F (B)$ . In particular, ${[a]}_{I}$ is neither zero nor an atom in $B$ . Thus, there is a decomposition $({[b^{'}]}_{I}, {[c^{'}]}_{I})$ of ${[a]}_{I}$ . We cannot have both ${[b^{'}]}_{I} \in F (B)$ and ${[c^{'}]}_{I} \in F (B)$ because that would imply ${[a]}_{I} = {[b^{'}]}_{I} ⊔ {[c^{'}]}_{I} \in F (B)$ . Without loss of generality, we assume ${[b^{'}]}_{I} \notin F (B)$ . The remainder of this proof is to show that putting $b = a ⊓ b^{'}$ and $c = a ⊓ \overline{b^{'}}$ yields the desired decomposition $(b, c)$ .

Obviously, $a = b ⊔ c$ and $b ⊓ c = 0$ . If we had $b = 0$ , then we would obtain $\begin{matrix} b^{'} = (a ⊓ b^{'}) ⊔ (\overline{a} ⊓ b^{'}) = \overline{a} ⊓ b^{'} ⊑ \overline{a} ⊓ (b^{'} ⊔ c^{'}) ⊑ a △ (b^{'} ⊔ c^{'}) . \end{matrix}$ Since ${[a]}_{I} = {[b^{'}]}_{I} ⊔ {[c^{'}]}_{I}$ , i.e. $a △ (b^{'} ⊔ c^{'}) \in I$ , this would imply $b^{'} \in I$ and hence ${[b^{'}]}_{I} = 0$ . However, this contradicts the fact that $({[b^{'}]}_{I}, {[c^{'}]}_{I})$ decomposes ${[a]}_{I}$ . Consequently, $b \neq 0$ . For the sake of another contradiction, suppose that $c = 0$ . Then $a ⊓ \overline{b^{'}} ⊓ c^{'} = 0$ and hence $\begin{array}{l} c^{'} & = (\overline{a} ⊓ c^{'}) ⊔ (a ⊓ b^{'} ⊓ c^{'}) ⊔ (a ⊓ \overline{b^{'}} ⊓ c^{'}) = (\overline{a} ⊓ c^{'}) ⊔ (a ⊓ b^{'} ⊓ c^{'}) \\ ⊑ (\overline{a} ⊓ (b^{'} ⊔ c^{'})) ⊔ (b^{'} ⊓ c^{'}) ⊑ (a △ (b^{'} ⊔ c^{'})) ⊔ (b^{'} ⊓ c^{'}) . \end{array}$ Since ${[b^{'}]}_{I} ⊓ {[c^{'}]}_{I} = 0$ , i.e. $b^{'} ⊓ c^{'} \in I$ , and $a △ (b^{'} ⊔ c^{'}) \in I$ , this implies $c^{'} \in I$ , i.e. ${[c^{'}]}_{I} = 0$ . Again, this is not possible and hence $c \neq 0$ . So far, we have shown that $(b, c)$ decomposes a. It remains to show that $b \notin F_{α + 1} (A)$ and $c \notin F_{α} (A)$ .

Concerning the first claim, observe that $b △ b^{'} = \overline{a} ⊓ b^{'} ⊑ a △ (b^{'} ⊔ c^{'}) \in I$ and hence ${[b]}_{I} = {[b^{'}]}_{I} \notin F (B)$ . The latter can be rephrased as $b \notin F_{α + 1} (A)$ . Regarding the second claim, we have $\begin{matrix} c △ c^{'} = (a ⊓ \overline{b^{'} ⊔ c^{'}}) ⊔ (\overline{a} ⊓ c^{'}) ⊑ a △ (b^{'} ⊔ c^{'}) \in I, \end{matrix}$ i.e. ${[c]}_{I} = {[c^{'}]}_{I} \neq 0$ . Since $I = F_{α} (A)$ , we obtain $c \notin F_{α} (A)$ . □
Lemma 6.8.
For every $n \in N$ , the iterated Frechét ideal $F_{n} (A)$ is uniformly $FO (\exists^{\infty})$ -definable in any Boolean algebra $A$ augmented by some well-order ⩽ on A.
Proof.
First, we prove the following characterization of $F (A)$ , which is obviously expressible in $FO (\exists^{\infty})$ : $\begin{matrix} F (A) = {a \in A ∣ there are only finitely many b \in A with b ⊑ a} . \end{matrix}$

First, consider $a \in F (A)$ . There are atoms $a_{1}, \dots, a_{n}$ such that $a = a_{1} ⊔ \dots ⊔ a_{n}$ . For each $b ⊑ a$ and $i = 1, \dots, n$ , we have $0 ⊑ a_{i} ⊓ b ⊑ a_{i}$ and hence either $a_{i} ⊓ b = 0$ or $a_{i} ⊓ b = a_{i}$ . Let $I_{b} \subseteq {1, \dots, n}$ be the set of those i with $a_{i} ⊓ b = a_{i}$ . Then $\begin{matrix} b = a ⊓ b = (a_{1} ⊔ \dots ⊔ a_{n}) ⊓ b = ⨆_{1 ⩽ i ⩽ n} (a_{i} ⊓ b) = ⨆_{i \in I_{b}} a_{i}, \end{matrix}$ i.e., b is determined by the set $I_{b}$ . In particular, there are at most $2^{n}$ many $b ⊑ a$ .

Second, consider some $a \in A ∖ F (A)$ . If there are infinitely many atoms below a, then there is nothing to show, so let us assume that $a_{1}, \dots, a_{n}$ be all atoms below a. Put $c = a_{1} ⊔ \dots ⊔ a_{n} \in F (A)$ . It suffices to show that there are infinitely many $b ⊑ a ⊓ \overline{c}$ . Clearly, $a ⊑ c$ as well as $a \neq c$ and hence $a ⊓ \overline{c} \neq 0$ . Since all atoms below a are also below c and $c ⊓ (a ⊓ \overline{c}) = 0$ , there is no atom below $a ⊓ \overline{c}$ . Due to this fact, there is an infinite sequence $c_{0}, c_{1}, c_{2}, \dots$ such that $a ⊓ \overline{c} = c_{0} ⊐ c_{1} ⊐ c_{2} ⊐ \dots ⊐ 0$ . This completes the characterization of $F (A)$ .

Now, we show the actual claim of the lemma by induction on n. Since $F_{0} (A) = {0}$ , the claim is trivial for $n = 0$ . Henceforth, suppose $n > 0$ . By the induction hypothesis, the iterated Frechét ideal $F_{n - 1} (A)$ is definable in $A$ . Applying the same idea as in the proof of Proposition 3.20, namely using the well-order ⩽ to select representatives, we can define the whole quotient algebra $A / F_{n - 1} (A)$ in $A$ . Thus, we can also define the Frechét ideal $F (A / F_{n - 1} (A))$ and hence the iterated Frechét ideal $F_{n} (A) = F_{n - 1} (A) \circ F (A / F_{n - 1} (A))$ in $A$ . □

Since Proposition 6.2 ensures that the interval algebra $I_{ω^{β} m}$ is the only countable superatomic Boolean algebra of type $(β, m)$ for countable β, the following proposition demonstrates the implication (1. ⇒ 2.) of Theorem 6.4. Proposition 6.9.
Let $n \in N$ . Every $(ω^{n})$ -automatic Boolean algebra $A$ is superatomic and its type $type (A) = (β, m)$ satisfies $β ⩽ n$ .
Proof.
If $A$ is finite, the claim is trivial. Henceforth, suppose that $A$ is infinite and therefore $n ⩾ 1$ . By Proposition 3.20, there is an injective $(ω^{n})$ -automatic presentation $(A, A_{⊔}, \dots)$ of $A$ over some alphabet Σ. Without loss of generality, we further assume that $L (A) = A \subseteq Σ^{(ω^{n})}$ . We denote the automatic well-order on $Σ^{(ω^{n})}$ defined in Lemma 3.19 by ⩽.

Aiming for a contradiction, suppose that the claim of the proposition is wrong. This would particularly imply $F_{n + 1} (A) \neq A$ and hence $1 \notin F_{n + 1} (A)$ . We consider the minimal relation $R \subseteq A \times A$ satisfying the following conditions.
For $a \in F (A)$ , $(a, a) \in R$ .

For $a \in A ∖ F (A)$ , we consider the greatest $r \in {1, \dots, n + 1}$ such that $a \notin F_{r} (A)$ . By Lemma 6.7, there is a decomposition $(b, c)$ of a such that $b \notin F_{r} (A)$ and $c \notin F_{r - 1} (A)$ . Among all these decompositions, for the one with the least b with respect to ⩽ we have $(a, b) \in R$ and $(a, c) \in R$ .
Moreover, we inductively define for each $k \in N$ a finite subset $H_{k} \subseteq A$ as follows: $\begin{array}{l} H_{0} & = {1}, H_{k + 1} = R (H_{k}) = {b \in A ∣ \exists a \in H_{k} : (a, b) \in R} . \end{array}$ Intuitively, one can visualize $H_{k}$ as the kth level of a finitely branching tree with root $1$ and successor relation R. Finally, we consider for every $k \in N$ the set $\begin{matrix} D_{k} = {⨆_{a \in M} a | M \subseteq H_{k}} . \end{matrix}$ In the remainder of this proof, we provide contradictory asymptotic lower and upper bounds on the size of $D_{k}$ . Claim.
We have the following lower bound on the size of $D_{k}$ : $\begin{matrix} | D_{k} | \in 2^{Ω (k^{n + 1})} . \end{matrix}$
Proof.
Two elements $a, a^{'} \in A$ are called disjoint if $a ⊓ a^{'} = 0$ . For disjoint $a, a^{'} \in A$ and a decomposition $(b, c)$ of a, the elements $a^{'}$ , b, c are mutually disjoint as well. Using this fact in an induction on k yields that the elements of $H_{k}$ are mutually disjoint. Moreover, the definition of decompositions implies $0 \notin H_{k}$ . In this situation, every element of $D_{k}$ is generated by a unique subset $M \subseteq H_{k}$ and hence $| D_{k} | = 2^{| H_{k} |}$ . Thus, it suffices to show $| H_{k} | \in Ω (k^{n + 1})$ .

To this end, we show by induction on k that $\begin{matrix} (3) & | H_{k} ∖ F_{r} (A) | ⩾ \sum_{i = 0}^{n + 1 - r} (\binom{k}{i}) \end{matrix}$ for $0 ⩽ r ⩽ n + 1$ , where $(\binom{k}{i}) = 0$ whenever $k < i$ . Since $1 \notin F_{r} (A)$ , the base case $k = 0$ is trivial. Henceforth, assume $k > 0$ . Every element of $H_{k - 1} ∖ F_{n + 1} (A)$ induces at least one element in $H_{k} ∖ F_{n + 1} (A)$ . In combination with the induction hypothesis, we obtain the inequation for $r = n + 1$ : $\begin{matrix} | H_{k} ∖ F_{n + 1} (A) | ⩾ | H_{k - 1} ∖ F_{n + 1} (A) | ⩾ (\binom{k - 1}{0}) = (\binom{k}{0}) . \end{matrix}$ For $0 ⩽ r ⩽ n$ , every element of $H_{k - 1} ∖ F_{r + 1} (A)$ induces two elements in $H_{k} ∖ F_{r} (A)$ and every element of $H_{k - 1} \cap (F_{r + 1} (A) ∖ F_{r} (A))$ induces at least one element in $H_{k} ∖ F_{r} (A)$ . In combination with the induction hypothesis, we obtain: $\begin{array}{l} | H_{k} ∖ F_{r} (A) | ⩾ & | H_{k - 1} ∖ F_{r + 1} (A) | \\ + | H_{k - 1} ∖ F_{r + 1} (A) | + | H_{k - 1} \cap (F_{r + 1} (A) ∖ F_{r} (A)) | \\ = & | H_{k - 1} ∖ F_{r + 1} (A) | + | H_{k - 1} ∖ F_{r} (A) | \\ ⩾ & \sum_{i = 0}^{n - r} (\binom{k - 1}{i}) + \sum_{i = 0}^{n + 1 - r} (\binom{k - 1}{i}) = \sum_{i = 0}^{n + 1 - r} (\binom{k}{i}) . \end{array}$ This completes the inductive proof of Eq. (3). The case $r = 0$ immediately implies $| H_{k} | ⩾ (\binom{k}{n + 1}) \in Ω (k^{n + 1})$ – the claimed lower bound. □
Claim.
We have the following upper bound on the size of $D_{k}$ : $\begin{matrix} | D_{k} | \in 2^{O (k^{n})} . \end{matrix}$
Proof.
According to Lemma 6.8, the relation R is $FO (\exists^{\infty})$ -definable in $A$ augmented by ⩽. By Proposition 3.17, there is an $ω^{n}$ -automaton $A_{R}$ recognizing R. Let $m \in N$ be such that both $A_{R}$ and $A_{⊔}$ have less than m states and put $X = supp (1)$ . By the growth lemma (Lemma 5.3), every $a \in H_{k}$ satisfies $supp (a) \subseteq U_{m}^{k} (X, ω^{n})$ . From the definitions of R and $H_{k}$ , we conclude $| H_{k} | ⩽ 2^{k}$ . Due to the growth lemma for semigroups (Lemma 5.4), every $d \in D_{k}$ satisfies $supp (d) \subseteq U_{m}^{k} (U_{m}^{k} (X, ω^{n}), ω^{n}) = U_{m}^{2 k} (X, ω^{n})$ and hence $\begin{matrix} | D_{k} | ⩽ | Σ |^{| U_{m}^{2 k} (X, ω^{n}) |} . \end{matrix}$ By Lemma 5.2, we further obtain $\begin{matrix} | U_{m}^{2 k} (X, ω^{n}) | ⩽ {(c_{m} (X) + 2 k m)}^{n} \in O (k^{n}) . \end{matrix}$ Combining the last two inequations yields $| D_{k} | \in 2^{O (k^{n})}$ – the claimed upper bound. □

Clearly, the provided lower and upper bound on the size of $D_{k}$ asymptotically contradict one another. □

6.3. Atomless Boolean algebras are not injectively $(α)$ -automatic

We prove that any atomless Boolean algebra is not $(α)$ -automatic. For this purpose, we first show by pumping that every $(α)$ -automatic $A$ possesses some nonempty $(ω^{ω})$ -automatic substructure $A^{'}$ such that, if $A ⊧ φ (\bar{a})$ , then $A^{'} ⊧ φ (\bar{a})$ , for all $φ \in \forall^{*} \exists^{*} Pos$ and $\bar{a} \in A^{'}$ . If the structure is injectively $(α)$ -automatic, then φ may even come from $\forall^{*} \exists^{*} {Pos}_{\neq}$ .

With this result it is easy to conclude that the existence of an injective presentation of some atomless Boolean algebra implies the existence of a $(ω^{ω})$ -automatic presentation of the countable atomless Boolean algebra. Given such a presentation, it could be turned into an injective one. We then use the growth lemma to show that such a presentation cannot exist.

Lemma 6.10.
Let $α ⩾ ω^{ω}$ be some ordinal and $A$ be a nonempty $(α)$ -automatic structure. There is a nonempty $(ω^{ω})$ -automatic substructure $A^{'}$ with the following property. For all formulas $φ (\bar{x}) \in \forall^{} \exists^{} Pos$ and all tuples $\bar{a} \in A^{'}$ , if $A ⊧ φ (\bar{a})$ , then $A^{'} ⊧ φ (\bar{a})$ . If $A$ is injectively $(α)$ -automatic, this result extends to all formulas in $\forall^{} \exists^{} {Pos}_{\neq}$ .
Proof.
Note that the second part follows from the first part because for all injectively $(α)$ -automatic presentations the expansion by the relation ≠ is also injectively $(α)$ -automatic.

Let $α^{'}$ be the ordinal such that $ω^{ω} + α^{'} = α$ and let f denote the embedding $f : Σ^{(ω^{ω})} \to Σ^{(α)}$ given by $f (w) = w ◇^{α^{'}}$ . Let $A$ be represented by the $(α)$ -automata $(A, A_{\approx}, A_{R_{1}}, \dots, A_{R_{n}})$ .

For any $(α)$ -automaton $B$ let $B^{ω^{ω}}$ denote the automaton which accepts any $w \in Σ^{(ω^{ω})}$ if and only if $B$ accepts $f (w)$ . Note that the construction of $B^{ω^{ω}}$ commutes with the automata constructions for Boolean connectives, i.e., if $B$ , $B_{1}$ , and $B_{2}$ are $(α)$ -automata such that $L (B) = L (B_{1}) * L (B_{2})$ for $* \in {\cup, \cap}$ , then $\begin{matrix} L (B^{ω^{ω}}) = L (B_{1}^{ω^{ω}}) * L (B_{2}^{ω^{ω}}) . \end{matrix}$

Let $A^{'}$ be the structure represented by $(A^{ω^{ω}}, A_{\approx}^{ω^{ω}}, A_{R_{1}}^{ω^{ω}}, \dots, A_{R_{n}}^{ω^{ω}})$ . Via f we can identify it with a substructure of $A$ . Note that $A^{'}$ is nonempty: let w be some $(α)$ -word accepted by $A$ . We can write w as $\begin{matrix} w = ◇^{α_{0}} σ_{1} ◇^{α_{1}} σ_{2} \dots ◇_{n - 1}^{α} σ_{n} ◇^{α_{n}} \end{matrix}$ with $σ_{i} \in Σ$ . Note that $α_{n}$ has countable cofinality if and only if α has. Thus, using the Pumping Lemmas 3.6 and 3.7, we can find for each $α_{i}$ an empty word of length $β_{i} < ω^{m + 1} \cdot 2$ where m is the number of states of $A$ such that $A$ has also an accepting run on $f (w^{'})$ where $\begin{matrix} w^{'} = ◇^{β_{0}} σ_{1} ◇^{β_{1}} σ_{2} \dots ◇_{n - 1}^{β} σ_{n} ◇^{ω^{ω}} . \end{matrix}$ Thus, $w^{'}$ represents some element of $A^{'}$ .

Now assume that $w_{1}, \dots, w_{n} \in Σ^{(ω^{ω})}$ represent elements $a_{1}, \dots, a_{n} \in A^{'}$ such that $\begin{matrix} A ⊧ \forall x_{1} \dots \forall x_{m} \exists y_{1} \exists \dots y_{ℓ} φ (a_{1}, \dots, a_{n}, x_{1}, \dots, x_{m}, y_{1}, \dots, y_{ℓ}) \end{matrix}$ for φ a Boolean combination of the relations of $A$ . Let $A_{φ}$ be an $(α)$ -automaton corresponding to φ on $A$ . Now we conclude that for all $v_{1}, \dots, v_{m} \in Σ^{(ω^{ω})}$ representing elements $b_{1}, \dots, b_{m} \in A^{'}$ there are words $u_{1}, \dots, u_{ℓ} \in Σ^{(α)}$ representing elements $c_{1}, \dots, c_{ℓ} \in A$ such that $A_{φ}$ accepts $\begin{matrix} (f (w_{1}), \dots, f (w_{n}), f (v_{1}), \dots, f (v_{m}), u_{1}, \dots, u_{ℓ}) . \end{matrix}$ Applying pumping (Propositions 3.6 and 3.7) to $\begin{matrix} (u_{1}, \dots, u_{ℓ}) ↾_{[max (⋃_{i = 1^{n}} supp (w_{i}) \cup ⋃_{i = 1}^{m} supp (v_{i})) + 1, α)}, \end{matrix}$ we can shrink the gaps in the support of $u_{1}, \dots, u_{ℓ}$ below $ω^{k}$ for some $k \in N$ . Thus results in $(ω^{ω})$ -words $u_{1}^{'}, \dots, u_{ℓ}^{'}$ such that $A_{φ}$ accepts $\begin{matrix} (f (w_{1}), \dots, f (w_{n}), f (v_{1}), \dots, f (v_{m}), f (u_{1}^{'}), \dots, f (u_{ℓ}^{'})) . \end{matrix}$ Recall that ${(A_{φ})}^{ω^{ω}}$ corresponds to φ on $A^{'}$ . By definition, ${(A_{φ})}^{ω^{ω}}$ accepts $\begin{matrix} (w_{1}, \dots, w_{n}, v_{1}, \dots, v_{m}, u_{1}^{'}, \dots, u_{ℓ}^{'}), \end{matrix}$ whence $A^{'} ⊧ φ (a_{1}, \dots, a_{n}, b_{1}, \dots, b_{m}, c_{1}^{'}, \dots, c_{ℓ}^{'})$ for $c_{i}^{'} \in A^{'}$ represented by $u_{i}^{'}$ . Since this argument is independent of the choice of $b_{1}, \dots, b_{m}$ , we conclude that $\begin{matrix} A^{'} ⊧ \forall x_{1} \dots \forall x_{m} \exists y_{1} \exists \dots y_{ℓ} φ (a_{1}, \dots, a_{n}, x_{1}, \dots, x_{m}, y_{1}, \dots, y_{ℓ}) . \end{matrix}$ □
Corollary 6.11.
Let $α ⩾ ω^{ω}$ be some ordinal. Every $(α)$ -automatic Boolean algebra has an $(ω^{ω})$ -automatic subalgebra. In particular, if there is an injectively $(α)$ -automatic atomless Boolean algebra, then the countable atomless Boolean algebra is $(ω^{ω})$ -automatic.
Proof.
Note that the axioms of Boolean Algebras are $\forall^{} \exists^{} Pos$ formulas. Moreover, an algebra is atomless if and only if it satisfies $\begin{matrix} \forall x \exists y \exists z (x = 0 \lor (x = y ⊔ z \land y ⊓ z = 0 \land y \neq 0 \land z \neq 0)) . \end{matrix}$ □
Theorem 6.12.
There is no non-trivial atomless Boolean algebra which is injectively $(α)$ -automatic for some ordinal α. Thus, there is no non-trivial atomless Boolean algebra which is $(β)$ -automatic for some ordinal $β < ω_{1} + ω^{ω}$ .
Proof.
Due to Corollary 6.11, it suffices to show that the non-trivial countable atomless Boolean algebra $A$ is not $(ω^{ω})$ -automatic. For this purpose, we use the same proof technique as in the proof of Proposition 6.9.

Aiming for a contradiction, assume that the non-trivial countable atomless Boolean algebra is $(ω^{ω})$ -automatic. This time, we define the relation $R \subseteq A \times A$ as follows: For every $a \in A ∖ {0}$ , we choose among all decompositions $(b, c)$ of a the one with the least b with respect to ⩽ and put $(a, b) \in R$ and $(a, c) \in R$ . Such a decomposition always exists because $A$ is atomless. We retain the definitions of $H_{k}$ and $D_{k}$ for $k \in N$ , but use the new relation R instead of the old one. The intuition about the tree remains the same as before, save that we now obtain the full binary tree. Along the lines of the old proof, one easily shows that the elements of $H_{k}$ are mutually disjoint and hence $| H_{k} | = 2^{k}$ as well as $| D_{k} | = 2^{2^{k}}$ . In the remainder of this proof, we establish an upper bound on the size of $D_{k}$ which asymptotically contradicts this observation.

Again, there is a $(ω^{ω})$ -automaton recognizing R. Let $m \in N$ be such that $A_{R}$ has less than m states and put $X = supp (1)$ . Using the two growth lemmas, we obtain $\begin{matrix} | D_{k} | ⩽ | Σ |^{| U_{m}^{2 k} (X, ω^{ω}) |} . \end{matrix}$ By Lemma 5.2, we have $\begin{matrix} | U_{m}^{2 k} (X, ω^{ω}) | ⩽ {(c_{m} (X \cup {ω^{ω}}) + 2 k m)}^{m + 1} d_{m} (X \cup {ω^{ω}}) \in O (k^{m + 1}) . \end{matrix}$ Combining the last two inequations yields $| D_{k} | \in 2^{O (k^{m + 1})}$ . Clearly, this asymptotically contradicts $| D_{k} | = 2^{2^{k}}$ . □

7. Groups and term algebras

The following result generalized the case of automatic structures (cf. [3]), since every automatic structure is equal to an $(ω)$ -automatic structure. For the definitions and basic properties of term algebras see [1,13].

Lemma 7.1.
For all cardinalities $κ ⩾ 2$ and all ordinals α, the free term algebra with one function f of arity 2 and κ many generators is not contained in any $(α)$ -automatic structure.

The same statement holds for the free semigroup and the free group with κ many generators.
Proof.
We do the proof only for the free term algebra. The other proofs are completely analogous using the product instead of the function f.

Heading for a contradiction, assume that $(A, A_{≃}, A_{G})$ is a (noninjective) $(α)$ -automatic presentation of the free term algebra $T$ with κ generators. In the following, we write ${[w]}_{\approx}$ for the element of A represented by w. Let u, v be $(α)$ -words such that ${[u]}_{\approx}$ and ${[v]}_{\approx}$ are two generators of $T$ . Define $T_{0} = {{[u]}_{\approx}, {[v]}_{\approx}}$ and $T_{i + 1} = {f (t_{1}, t_{2}) ∣ t_{1}, t_{2} \in T_{i}}$ . Note that $| T_{0} | = 2^{2^{0}}$ and, inductively, $\begin{matrix} | T_{i} | = | T_{i - 1} |^{2} = {(2^{2^{i - 1}})}^{2} = 2^{2^{i - 1} \cdot 2} = 2^{2^{i}} . \end{matrix}$ Using Lemma 5.5 we obtain a constant m such that each of the elements of $T_{n}$ has a representative w such that $\begin{matrix} (4) & supp (w) \subseteq U_{m}^{n} (supp (u) \cup supp (v), α) . \end{matrix}$ Let $w_{1}, w_{2}, \dots, w_{2^{2^{n}}}$ be representatives of the $2^{2^{n}}$ many pairwise distinct elements of $T_{n}$ satisfying (4). But by Lemma 5.2, there are constants c, d and e such that $2^{c + {(d n)}^{e}}$ is a bound on the number of words with support in $U_{m}^{n} (supp (u) \cup supp (v), α)$ . This is clearly a contradiction for large n. □

The free term algebra with countable infinitely many generators separates the class of tree-automatic structures from the class of ordinal-automatic structures. Damian Niwinski introduced a tree-automatic presentation of this algebra to us. Since we are not aware of a citable reference for this result, we sketch it in the next example. Readers that are not familiar to the notion of tree-automatic structures can safely continue reading in Section 8. Example 7.1.
Let T be the set of all finite subsets of ${0, 1}^{}$ . We define a function $f : T^{2} \to T$ by $\begin{matrix} \begin{matrix} f (t_{1}, t_{2}) = & {w \in {0, 1}^{} 0 ∣ w = w^{'} 0 with w^{'} \in t_{1}} \\ \cup {w \in {0, 1}^{} 1 ∣ w = w^{'} 1 with w^{'} \in t_{2}} \\ \cup {ε} . \end{matrix} \end{matrix}$ Note that $(T, f)$ is isomorphic to the free term algebra with countable infinitely many generators: the generators are the elements of the set G of all finite subsets $t \subseteq {0, 1}^{}$ such that $ε \notin t$ and f is a injective function such that $im (f) = T ∖ G$ .

Now we construct a tree-automatic presentation of $(T, f)$ . For $t \subseteq {0, 1}^{*}$ denote by $↓ (t)$ the set of all prefixes of the elements of t. We encode an element $t \in T$ as the tree $\begin{matrix} [t] : ↓ (t) \to {a, b}, where [t] (x) = \{\begin{matrix} a & x \in t, \\ b & x \in ↓ (t) ∖ t . \end{matrix} \end{matrix}$ The set ${[t] ∣ t \in T}$ is tree-automatic. It contains all finite trees where all leaves are labelled a. In this presentation, the function f is also trivially automatic because the representation of $f (t_{1}, t_{2})$ is obtained from the presentations $[t_{1}]$ and $[t_{2}]$ by shifting all occurrences of a in $[t_{1}]$ to the position at the left successor and all occurrences of a in $[t_{2}]$ to the position at the right successor.

8. Order forests

Definition 8.1.
An (order) forest is a partial order $A = (A, ⩽)$ such that for each $a \in A$ , the set ${a^{'} \in A ∣ a ⩽ a^{'}}$ is a finite linear order.

We want to study the rank (also called ordinal height) of $(α)$ -automatic well-founded forests. For this purpose we recall the definition of the height of a well-founded partial order. Afterwards, we introduce a variant of the height called infinity rank or $\infty - rank$ .
Definition 8.2.
Let $A = (A, ⩽)$ be a well-founded partial order. Setting $sup (\emptyset) = 0$ we define the height of $A$ by $\begin{array}{l} height (a, A) = sup {height (a^{'}, A) + 1 ∣ a^{'} < a \in A} and \\ height (A) = sup {height (a, A) + 1 ∣ a \in A} . \end{array}$
Definition 8.3.
Let $P = (P, ⩽)$ be a well-founded partial order. We define the ordinal valued $\infty - rank$ of a node $p \in P$ inductively by $\begin{array}{l} \infty - rank (p, P) = sup {α + 1 ∣ \exists^{\infty} p^{'} (p^{'} < p and \infty - rank (p^{'}, P) ⩾ α)} . \end{array}$ The $\infty - rank$ of $P$ is then $\begin{array}{l} \infty - rank (P) = sup {α + 1 ∣ \exists^{\infty} p \in P \infty - rank (p, P) ⩾ α} . \end{array}$

The two notions of height have a close connection. Due to this connection, proving bounds on the height of $(α)$ -automatic well-founded forests reduces to proving bounds on the infinity rank. We first state this connection and then announce our main result. Lemma 8.4 (Kartzow, Liu, and Lohrey [15]).

For $P$ a well-founded partial order, we have $\begin{matrix} \infty - rank (P) ⩽ height (P) < ω \cdot (\infty - rank (P) + 1) . \end{matrix}$

8.1. Upper bounds on the height of order forests

The following result generalizes the case of automatic structures (cf. [16,25]), since every automatic structure is equal to an $(ω)$ -automatic structure.

Theorem 8.5.
Let $α = ω^{1 + γ} < ω_{1} + ω^{ω}$ be some ordinal. Every $(α)$ -automatic well-founded order forest $F = (F, ⩽)$ has $\infty - rank$ strictly below $ω^{γ + 1}$ and rank strictly below $ω^{1 + γ + 1}$ .

This theorem is our main result on $(α)$ -automatic well-founded order forests. We prove this theorem as follows. Since the set of $(α)$ -words allows an $(α)$ -automatic well-order, we can associate with every $(α)$ -automatic well-founded order forest $F$ an $(α)$ -automatic ordinal (the Kleene–Brouwer ordinal with respect to $F$ and the $(α)$ -automatic well-order). Extending a result of Kuske et al. [25], we provide a connection between this ordinal and the infinity rank of the forest (which has already been used in [17]). Since Schlicht and Stephan [29] provided upper bounds on the $(α)$ -automatic ordinals, this connection implies bounds on the infinity ranks and height of $(α)$ -automatic forests.

Let $T = (T, ⊑)$ be a tree and let $L = (T, ⪯)$ be a linear order. Then we define the Kleene–Brouwer order (also called Lusin–Sierpiński order) $KB (T, L) : = (T, ⋖)$ given by $t ⋖ t^{'}$ if either $t^{'} ⊑ t$ or there are $s ⊑ t$ , $s^{'} ⊑ t^{'}$ such that ${r \in T ∣ r ⊏ s} = {r \in T ∣ r^{'} ⊏ s}$ and $s ≺ s^{'}$ . This generalises the order induced by postorder traversal to infinitely branching trees where the children of each node are ordered corresponding to the linear order ⪯. It is well-known that $KB (T, L)$ is a well-order if there are no infinite branches in $T$ and $L$ is a well-order. Since $(α)$ -automatic structures are closed under first-order definitions, the following observation is immediate.
Proposition 8.6.
Let $α < ω_{1} + ω^{ω}$ . If $T$ is an tree and $L$ a linear order such that both are $(α)$ -automatic with domain T, then $KB (T, L)$ is $(α)$ -automatic.
Lemma 8.7 (cf. [17]).

Let $T = (T, ⩽)$ be a nonempty well-founded order tree and $L$ a well-order with domain T. For all ordinals β, if $\infty - rank (T) ⩾ β$ . then $KB (T, L) ⩾ ω^{β}$ ,

Proof.
The proof is by induction on β.
If $β = 0$ , For nonempty $T$ we conclude that $KB (T, L)$ is nonempty whence it is at least $1 = ω^{β}$ .

Assume that $\infty - rank (T) = β = β^{'} + 1$ and that $KB (T^{'}, L) ⩾ ω^{β^{'}}$ for each tree $T^{'}$ with $\infty - rank (T^{'}) = β^{'}$ .

Since $T$ is well-founded, there is some node d such that $\infty - rank (d, T) = β$ and there is an infinite list $d_{1}, d_{2}, d_{3}, \dots$ of successors of d such that the subtree $T (d_{i})$ rooted at $d_{i}$ satisfies $\infty - rank (T (d_{i})) = β^{'}$ . By induction hypothesis, $KB (T (d_{i}), L) ⩾ ω^{β^{'}}$ . Without loss of generality we can assume that the order type of ${d_{i} ∣ i \in N}$ with respect to $L$ is ω (otherwise, take a subsequence). We conclude that $\begin{array}{l} KB (T, L) ⩾ \sum_{i \in ω} KB (T (d_{i}), L) = ω^{β^{'}} \cdot ω = ω^{β} . \end{array}$

Assume that $\infty - rank (T) = β$ is a limit ordinal. By definition for each $β^{'} < β$ there is $d \in T$ such that $\infty - rank (T (d)) ⩾ β^{'}$ whence $KB (T (d), L) ⩾ ω^{β^{'}}$ by induction hypothesis. Thus, $\begin{matrix} KB (T, L) ⩾ sup {ω^{β^{'}} ∣ β^{'} < β} = ω^{β} . \end{matrix}$
□

We prove Theorem 8.5 by a combination of this result with the following characterisation of the $(α)$ -automatic ordinals.
Theorem 8.8 (Schlicht and Stephan [29]).

For $γ = ω^{1 + γ^{'}}$ , and δ some ordinal, $(δ, <)$ is injectively $(γ)$ -automatic if and only if $δ < ω^{ω^{γ^{'} + 1}}$ .

In fact, the result carries over to noninjective presentations:

Corollary 8.9.
For $γ = ω^{1 + γ^{'}}$ , and δ some ordinal, $(δ, <)$ $(γ)$ -automatic if and only if $δ < ω^{ω^{γ^{'} + 1}}$ .
Proof.
Let $(A, A_{\approx}, A_{<})$ be an $(α)$ -automatic presentation of $(δ, <)$ . Denoting by ≺ the well-order from Lemma 3.19 we construct the automaton $A_{<^{'}}$ corresponding to the quantifier-free positive formula $x < y \lor (x \approx y \land x ≺ y)$ (recall that $(α)$ -automatic structures are closed under quantifier-free positive definable relations). $(A, A_{<^{'}})$ clearly represents some ordinal $(η, <)$ such that δ injectively embeds into η. Now Schlicht and Stephan’s theorem gives an upper bound on η which is also a bound on δ. □
Proof of Theorem 8.5.
Assume that $T = (T, ⩽)$ is an $(α)$ -automatic order tree (where $α < ω_{1} + ω^{ω}$ ). Without loss of generality we may assume that its presentation is injective. Let $L$ be the $(α)$ -automatic well-order obtained by restriction of the well-order from Lemma 3.19 to the representatives of T. Since $KB (T, L)$ is an $(α)$ -automatic ordinal, $KB (T, L) < ω^{ω^{γ + 1}}$ due to Theorem 8.8. Due to Lemma 8.7, $\infty - rank (T) < ω^{γ + 1}$ . By application of Lemma 8.4 we finally obtain $height (T) < ω^{1 + γ + 1}$ .

Note that this result easily extends to forests because for each $(α)$ -automatic forest, we can turn it into an $(α)$ -automatic tree by adding a new root. This tree has the same $\infty - rank$ as the forest we started with. □
Remark 8.1.
Theorem 8.5 also holds in the setting where α is an arbitrary ordinal and $F = (F, ⩽, succ)$ is an injective $(α)$ -automatic well-founded order forest with automatic successor-relation, i.e., if $(F, ⩽)$ is a well-founded order forest and $succ$ defines the relation $\begin{matrix} succ = {(f, g) \in F ∣ f ⩽ g \land \forall h \neg (f < h < g)} . \end{matrix}$ In this setting, note that the strict order relation of $KB (T, L)$ can be defined by $t ⋖ t^{'}$ if $t^{'} ⊏ t$ or there are r, s, $s^{'}$ such that $s ⊑ t$ , $s^{'} ⊑ t^{'}$ , $succ (r, s)$ , $succ (r, s^{'})$ , $s \neq s^{'}$ and $s ≺ s^{'}$ which is definable in $\exists^{*} {Pos}_{\neq}$ . Thus, $KB (T, L)$ is $(α)$ -automatic and we can proceed as before.

8.2. Optimality of the bounds on forests

The upper bounds from Theorem 8.5 are optimal in the sense that we can reach all lower ranks as stated in the following theorem.

Theorem 8.10.

For all $i, c \in N$ there is an $(ω^{i})$ -automatic tree $T_{i, c}$ with $\infty - rank (T_{i, c}) = ω^{i - 1} \cdot c$ and $height (T_{i, c}) = ω^{i} \cdot c$ .

For all ordinals $γ ⩾ ω$ and all $c \in N$ , there is an $(ω^{γ})$ -automatic tree $T_{γ, c}$ with $height (T_{γ, c}) = ω^{γ} \cdot c$ .

In order to prove the first part of Theorem 8.10, we want to construct for all $i \in N$ and $c \in N$ an $(ω^{i})$ -automatic tree of $\infty - rank$ $ω^{i - 1} \cdot c$ and rank $ω^{i} \cdot c$ .

We define an $(ω)$ -automatic tree as follows. Let $T = ({ε} \cup {(n, m) ∣ n ⩽ m})$ and $T_{0} = (T, ⩽)$ where $\begin{array}{l} ε ⩽ t for all t \in T, \\ (n, m) ⩽ (n^{'}, m^{'}) if m = m^{'} and n ⩽ n^{'} . \end{array}$ $T_{0}$ is clearly well-founded, $(ω)$ -automatic, and satisfies $\infty - rank (T_{0}) = 1$ and $height (T_{0}) = ω$ .

Next, we show that for any $i, c \in N$ and any given $(ω^{i})$ -automatic tree $T$ there is also an $(ω^{i})$ -automatic tree $T^{'}$ such that $\infty - rank (T^{'}) = \infty - rank (T) \cdot c$ and $height (T) = height (T) \cdot c$ .

Lemma 8.11.

Let $c \in N$ and $T$ an $(α)$ -automatic tree. Then there is an $(α)$ -automatic tree $T_{c}$ such that $\infty - rank (T_{c}) = \infty - rank (T) \cdot c$ and $height (T) = height (T) \cdot c$ .

Proof.

Let $T = (T, ⩽)$ . Set $T_{c} = ⋃_{i = 1}^{c} T^{i}$ . The order of $T_{c}$ is given by $\begin{matrix} (t_{1}, t_{2}, \dots, t_{i}) ⩽_{c} (t_{1}^{'}, t_{2}^{'}, \dots, t_{j}^{'}) \end{matrix}$ iff $i ⩽ j$ , $t_{1} = t_{1}^{'}$ , $\dots$ , $t_{i - 1} = t_{i - 1}^{'}$ and $t_{i} ⩽ t_{i}^{'}$ .

Note that $T_{1} = T$ and $T_{c + 1}$ is obtained from $T_{c}$ by attaching a copy of $T$ to each node of $T_{c}$ . Thus, an easy induction on c proves the claim on the height and the $\infty - rank$ . Moreover, $T_{c}$ is first-order interpretable in $T$ extended by one element using a c-dimensional interpretation whose formulas are all quantifier free and positive. □

By replacing the convolution by composition of $ω^{i}$ -words, we construct an $(ω^{i + 1})$ -automatic representation of the forest $⨆_{c \in N} T_{c}$ for any $(ω^{i})$ -automatic tree $T$ .

Lemma 8.12.

For $T$ an $(ω^{i})$ -automatic tree, the forest $F : = ⨆_{c \in N} T_{c}$ is $(ω^{i + 1})$ -automatic.

Proof.

Let T be the set of $ω^{i}$ -words representing the elements of $T = (T, ⩽)$ (over alphabet Σ). Without loss of generality, we assume that $◇^{ω^{i}} \notin T$ . Let F be the set of $ω^{i + 1}$ -words of the form $\begin{matrix} {t_{n} + t_{n - 1} + \dots + t_{1} + ◇^{ω^{i + 1}} ∣ n \in N, t_{i} \in T \cup {◇^{ω^{i}}} for 1 < i ⩽ n, t_{1} \in T} . \end{matrix}$ We equip F with an order ⊑ by setting $\begin{matrix} t_{n} + t_{n - 1} + \dots + t_{1} + ◇^{ω^{i + 1}} ⊑ t_{n^{'}}^{'} + t_{n^{'} - 1}^{'} + \dots + t_{1}^{'} + ◇^{ω^{i + 1}} \end{matrix}$ if and only if $n = n^{'}$ , there is a $k ⩽ n$ such that $t_{i}^{'} = t_{i}$ for all $i < k$ , $t_{k} ⩽ t_{k}^{'}$ , and $t_{i} = ◇^{ω^{i}}$ for all $k < i ⩽ n$ .

It is straightforward to construct an automaton for ⊑ from automata for T and ⩽.

It is easy to see that $(F, ⊑)$ is a presentation of the forest $F$ : those nodes with support contained in $ω^{i} \cdot c$ but not in $ω^{i} \cdot (c - 1)$ are exactly those elements representing $T_{c}$ . □

Of course, we can add a new root to $F$ and obtain an $(ω^{i + 1})$ -automatic tree $T^{'}$ with $\infty - rank (T^{'}) = sup {\infty - rank (T) \cdot c ∣ c \in N}$ and $height (T^{'}) = sup {height (T) \cdot c ∣ c \in N}$ .

Iterated application of this lemma to the tree $T_{1}$ shows that for each $i \in N$ there is an $(ω^{i})$ -automatic tree of rank $ω^{i + 1}$ (and $\infty - rank$ $ω^{i}$ ). Application of Lemma 8.11 then proves the first part of Theorem 8.10.

We now use a variant of the previous construction in order to prove the second part of Theorem 8.10, i.e., we construct $(α)$ -automatic trees of high ranks for ordinals $α ⩾ ω^{ω}$ .

Definition 8.13.

Let α be an ordinal. Let $D_{α}$ be the set of finite $(α)$ -words w over ${◇, 1}$ such that for all limit ordinals $β < α$ and all $c \in ω$ the implication $\begin{array}{l} w (β + c) = 1 \Rightarrow w (β) = w (β + 1) = \dots = w (β + c) = 1 \end{array}$ holds. We define a partial order on $D_{α}$ via the suffix relation: for $w_{1}, w_{2} \in D_{α}$ let $w_{1} {\vec{⊒}}_{α} w_{2}$ if and only if for $β ⩽ α$ maximal such that for all $0 ⩽ γ < β w_{2} (γ) = ◇$ we have that $\forall β ⩽ δ < α w_{1} (δ) = w_{2} (δ)$ , i.e., $supp (w_{2})$ is an upwards closed subset of $supp (w_{1})$ and both agree on $supp (w_{2})$ .

Note that $T_{α} : = (D_{α}, {\vec{⊒}}_{α})$ is $(α)$ -automatic. We can even add the successor relation to $T_{α}$ .

Lemma 8.14.

$T_{α} : = (D_{α}, {\vec{⊒}}_{α})$ is a tree.

Proof.

Since $D_{α}$ contains $(α)$ -words w there are only finitely many positions $β < γ$ with $w (β) = 1$ . Thus, there are also only finitely many suffixes of w that are undefined up to some position in $supp (w)$ . This implies that all ascending chains are finite. Moreover, the suffix relation is a linear order when restricted to the suffixes of a fixed word w. □

The following lemma combined with Lemma 8.11 proves the second part of Theorem 8.10.

Lemma 8.15.

For all ordinals α, $α^{'}$ such that $α = ω \cdot α^{'} ⩾ ω$ , $height (T_{α}) = α^{'}$ .

Proof.

The proof is by induction on $α^{'}$ . For $α = ω \cdot 1 = ω$ note that $D_{α}$ consists of all words $1^{m} ◇^{ω}$ , $m \in N$ where the word $◇^{ω}$ is suffix of all other elements. Moreover, these others are pairwise incomparable. Thus, $T_{ω}$ is the infinite tree of depth 1 which has rank 1 as desired. We now proceed by induction.

Assume that $α^{'}$ is a successor ordinal, i.e., there is some $β^{'}$ such that $α = ω \cdot α^{'} = ω \cdot β^{'} + ω$ . Note that the words directly below $◇^{α}$ are those of the form $w = ◇^{γ} 1^{m} ◇^{δ}$ such that $γ + δ = α$ and γ is some limit ordinal and $m < ω$ . Fix such a word and note that $D_{α} \cap {w^{'} ∣ w^{'} {\vec{⊒}}_{α} w}$ induces a suborder isomorphic to $(D_{γ}, {\vec{⊒}}_{γ})$ which by induction hypothesis has rank $γ^{'}$ for $γ^{'}$ such that $γ = ω \cdot γ^{'}$ . Thus, the suborders of maximal rank $β^{'}$ are induced by the elements $w_{m} = ◇^{ω \cdot β^{'}} 1^{m} ◇^{ω}$ for each $m < ω$ . Since these are infinitely many nodes of $\infty - rank$ $β^{'}$ , the rank of $T_{α}$ is $β^{'} + 1 = α^{'}$ .

Assume that $α^{'}$ is a limit ordinal and ${(β_{i})}_{i \in ω}$ converges to $α^{'}$ and $β_{i} < α$ for each $i \in ω$ . Then each $w_{i}^{m} : = ◇^{β_{i}} 1^{m} ◇^{α}$ for $m, i \in ω$ is directly below $◇^{α}$ and induces a suborder isomorphic to $(D_{β_{i}}, {\vec{⊒}}_{β_{i}})$ of $\infty - rank$ $β_{i}$ . Thus, $\infty - rank (T_{α}) ⩾ α^{'}$ . But as in the previous case we see that all proper suborders have $\infty - rank < α$ whence $\infty - rank (T_{α}) ⩽ α^{'}$ . Thus, its $\infty - rank$ is exactly $α^{'}$ . □

Footnotes

Determinisation fails at ω 1

References

Baader and

Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.

Blumensath, Automatic structures, Diploma thesis, RWTH Aachen, 1999.

Blumensath and

Grädel, Automatic structures, in: Proc. 15th IEEE Symp. on Logic in Computer Science, 2000, pp. 51–62.

J.R.

Büchi, Decision methods in the theory of ordinals, Bull. Amer. Math. Soc. 71 (1965), 767–770.

J.R.

Büchi, The monadic second order theory of ω₁, in: Decidable Theories II,

G.H.

Müller and

Siefkes, eds, Lecture Notes in Mathematics, Vol. 328, Springer, Berlin, Heidelberg, 1973, pp. 1–127.

Carton, Accessibility in automata on scattered linear orderings, in: MFCS,

Diks and

Rytter , eds, Lecture Notes in Computer Science, Vol. 2420, Springer, 2002, pp. 155–164.

Delhommé, Automaticité des ordinaux et des graphes homogènes, C.R. Acad. Sci. Paris Ser. I 339 (2004), 5–10.

Finkel and

Todorčević, A hierarchy of tree-automatic structures, CoRR, 2011, http://arxiv.org/abs/1111.1504.

Finkel and

Todorčević, Automatic ordinals, CoRR, 2012, http://arxiv.org/abs/1205.1775.

10.

Finkel and

Todorčević, A hierarchy of tree-automatic structures, J. Symb. Log. 77(1) (2012), 350–368.

11.

Finkel and

Todorčević, Automatic ordinals, IJUC 9(1,2) (2013), 61–70.

12.

S.S.

Goncharov, Countable Boolean Algebras and Decidability, Siberian School of Algebra and Logic, Springer, 1997.

13.

Hodges, A Shorter Model Theory, Cambridge University Press, 1997.

14.

Huschenbett, The rank of tree-automatic linear orderings, in: STACS,

Portier and

Wilke, eds, LIPIcs, Vol. 20, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013, pp. 586–597.

15.

Kartzow,

Liu and

Lohrey, Tree-automatic well-founded trees, in: Proc. CIE 2012, Lecture Notes in Computer Science, Springer-Verlag, 2012.

16.

Kartzow,

Liu and

Lohrey, Tree-automatic well-founded trees, in: How the World Computes – Turing Centenary Conference and 8th Conference on Computability in Europe, CiE 2012, Cambridge, UK, June 18–23, 2012. Proceedings,

S.B.

Cooper,

Dawar and

Löwe, eds, Lecture Notes in Computer Science, Vol. 7318, Springer, pp. 363–373.

17.

Kartzow,

Liu and

Lohrey, Tree-automatic well-founded trees, CoRR, http://arxiv.org/abs/1201.5495, 2012, Version 1.

18.

Kartzow and

Schlicht, Structures without scattered-automatic presentation, in: The Nature of Computation. Logic, Algorithms, Applications – 9th Conference on Computability in Europe, CiE 2013, Milan, Italy, July 1–5, 2013. Proceedings,

Bonizzoni,

Brattka and

Löwe, eds, Lecture Notes in Computer Science, Vol. 7921, Springer, 2013, pp. 273–283.

19.

Khoussainov and

Minnes, Model-theoretic complexity of automatic structures, Ann. Pure Appl. Logic 161(3) (2009), 416–426.

20.

Khoussainov and

Nerode, Automatic presentations of structures, in: LCC, 1994, pp. 367–392.

21.

Khoussainov and

Nerode, Automata Theory and Its Applications, Progress in Computer Science and Applied Logic, Vol. 21, Birkhäuser, 2001.

22.

Khoussainov,

Nies,

Rubin and

Stephan, Automatic structures: Richness and limitations, Logical Methods in Computer Science 3(2) (2007), 1–18.

23.

Khoussainov,

Rubin and

Stephan, Automatic linear orders and trees, ACM Trans. Comput. Log. 6(4) (2005), 675–700.

24.

Koppelberg, Handbook of Boolean Algebras, Vol. 1, North Holland, 1989.

25.

Kuske,

Liu and

Lohrey, The isomorphism problem on classes of automatic structures with transitive relations, Transactions of the American Mathematical Society 365 (2013), 5103–5151.

26.

Neeman, Finite state automata and monadic definability of singular cardinals, J. Symb. Log. 73(2) (2008), 412–438.

27.

Neeman, Monadic definability of welders, in: Logic, Methodology and Philosophy of Science. Proceedings of the Thirteenth International Congress,

W.G.

Wei, ed., College Publications, 2009, pp. 108–121.

28.

J.G.

Rosenstein, Linear Orderings, Academic Press, 1982.

29.

Schlicht and

Stephan, Automata on ordinals and automaticity of linear orders, Ann. Pure Appl. Logic 164(5) (2013), 523–527.

30.

Wojciechowski, Classes of transfinite sequences accepted by finite automata, Fundamenta Informaticae 7(2) (1984), 191–223.

Pumping for ordinal-automatic structures 1

Abstract

Keywords

1. Introduction

1.1. Outline of the paper

2. Preliminaries

2.1. Ordinals

2.2. Logics

3. Ordinal-automatic structures

Proposition 3.6 (First pumping).

Proposition 3.7 (Second pumping).

Lemma 3.14 (cf. [30]).

2 Readers who are not familiar with the notion of logical interpretations can obtain the necessary basics from [2].

6.1. Basics on Boolean algebras

Proposition 6.3 ([12, Proposition 1.5.1]).

6.2. Classification of the ( ω n ) -automatic Boolean algebras

8.1. Upper bounds on the height of order forests

Footnotes

Determinisation fails at ω 1

References

²
Readers who are not familiar with the notion of logical interpretations can obtain the necessary basics from [2].

6.2. Classification of the $(ω^{n})$ -automatic Boolean algebras