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

HAL
open science

# On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates

Thomas Colcombet, Alexander Rabinovich

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

## To cite this version:

Thomas Colcombet, Alexander Rabinovich. On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates. Computer Science Logic (CSL), Jan 2025, Amsterdam, Netherlands. 10.4230/LIPIcs.CSL.2025.11 . hal-05413474

HAL Id: hal-05413474

https://hal.science/hal-05413474v1

Submitted on 12 Dec 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates

Thomas Colcombet

Université Paris Cité, CNRS, IRIF, France

Alexander Rabinovich

The Blavatnik School of Computer Science, Tel-Aviv University, Israel

## Abstract

In this work, we consider two extensions of monadic second-order logic, and study in what cases the classical decidability results are preserved.

The first extension, MSO[$\mathrm{CBrank}_\beta$], is MSO (over the signature of the binary tree) augmented with the extra ability to express that the subtree over a set $X$ has Cantor-Bendixson rank $\beta$, for some fixed countable ordinal $\beta$. We show that this extension is decidable over the binary tree if and only if $\beta$ is finite, which means that it is decidable if and only if it is equivalent in expressiveness to MSO.

The second extension, MSO[$\mathrm{otp}_\alpha$], is MSO (over the signature of order) augmented with the extra ability to express that the suborder induced by a set $X$ has order type $\alpha$ for some fixed countable ordinal $\alpha$. We show that this extension is decidable over countable ordinals if and only if $\alpha < \omega^\omega$, which means that it is decidable if and only if it is equivalent in expressiveness to MSO.

The first result can be established as a consequence of the second. The second result relies on the undecidability results of the logic BMSO (itself relying on the undecidability of MSO+U) in the case of $\omega^\beta$ for $\beta$ a limit ordinal, and on entirely new techniques when $\beta$ is a successor ordinal. We also have some partial extensions of the second result to some uncountable cases.

**2012 ACM Subject Classification** Theory of computation → Tree languages; Theory of computation → Logic and verification

**Keywords and phrases** Logic, Algorithmic model theory, Monadic second-order logic, Ordinals, Binary tree

**Digital Object Identifier** 10.4230/LIPIcs.CSL.2025.11

**Funding** Alexander Rabinovich: Visits to IRIF were supported by the Fondation Sciences Mathématiques de Paris (FSMP) and Université Paris Cité.

## 1 Introduction

This work studies extensions of monadic second-order logic for which the decidability status was not known before.

Monadic second-order logic (MSO) is the extension of first-order logic with set quantifiers. It plays a key role in the context of automata and verification. The central decidability results in this context are (1) the seminal paper of Büchi [10] that proves the decidability of MSO($\mathbb{N},<$) using automata, (2) the breakthrough [24] where Rabin establishes that MSO is decidable on infinite trees of height $\omega$, again using automata, and from which the decidability of MSO over countable chains can be deduced, and finally (3) the introduction by Shelah [31] of model-theoretic techniques for showing the decidability of the MSO-theory of countable linear orderings, traditionally referred to as the “composition method.”

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

© Thomas Colcombet and Alexander Rabinovich;
licensed under Creative Commons License CC-BY 4.0

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025).

Editors: Jörg Endrullis and Sylvain Schmitz; Article No. 11; pp. 11:1–11:26

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

LIPICS

Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 11:2 On the Expansion of MSO with Cantor-Bendixson Rank and Order Type Predicates

These historical contributions show the extremely strong decidability properties that enjoy MSO. Their extension beyond MSO and beyond linear orderings and trees has been and still is a strong motivation for new research in the field (see more in Section 1.3). The present work pursues this quest by considering two natural extensions of monadic second-order logic (MSO for short).

### 1.1 Contributions

Our two contributions, Theorems 1 and 2 share a similar form. We consider in both cases a natural notion of measure of the “complexity” of a set, namely, the Cantor-Bendixson rank in the theory of infinite trees for the first one, and the order type in the theory of well-founded linear orders for the second. We then study the decidability status of MSO extended with a construction of the form:

> “the complexity of the set X is $\alpha$”

for a unique fixed value of $\alpha$. Our results show that either this new construction was already expressible in MSO, or decidability is lost.

#### First extension: Cantor-Bendixson rank of trees

We consider here an extension of the monadic theory of trees.

The Cantor-Bendixson rank of a tree is an ordinal that measures its branching complexity (see Section 3 for more on trees and the Cantor-Bendixson rank), and is undefined if the tree contains an induced full binary tree. A subset $X$ of a tree is downward closed if whenever $v \in X$, then all the nodes on the path from the root of $T$ to $v$ are in $X$. Given an ordinal $\alpha$, for $X$ some downward closed subset of an infinite tree, let $\mathbf{CBrank}_{\alpha}(X)$ express that “the tree restricted to universe $X$ has Cantor-Bendixson rank $\alpha$”. We denote by $\mathbf{MSO[\mathbf{CBrank}_{\alpha}]}$ monadic second-order logic extended with the new predicate $\mathbf{CBrank}_{\alpha}(-)$. We prove:

* **Theorem 1.** For all countable ordinals $\alpha$, the following properties are equivalent:

* the MSO[$\mathbf{CBrank}_{\alpha}$]-theory of the full binary tree is decidable,

* $\alpha$ is finite,

* $\mathbf{CBrank}_{\alpha}$ is MSO-definable.

It can be summarised as the impossibility to extend the main theorem of Rabin of decidability of MSO over the full binary tree with the ability to express the Cantor-Bendixson rank of trees.

#### Second extension: the order type of an ordinal

We consider here an extension of the monadic theory of linear orders.

Büchi [11] proved a kind of “a small model property”: if an MSO-formula is satisfiable in any countable ordinal, then it is satisfiable in an ordinal $< \omega^\omega$. Hence, $\omega^\omega$ is MSO-undefinable. On the other hand, for every ordinal $\alpha < \omega^\omega$ one can express “the order type of $X$ is $\alpha$.” A natural question follows: is the extension of MSO by the ability to express “the order type of $X$ is $\omega^\omega$” still decidable? We provide a negative answer to this question.

Given an ordinal $\alpha$, we consider the predicate $otp_{\alpha}(X)$ which holds if the order type of the set $X$ is the ordinal $\alpha$, i.e., if the linear order restricted to universe $X$ is isomorphic to $\alpha$. We denote by $\mathbf{MSO[otp}_{\alpha}]$ the monadic second-order logic of order extended with the new predicate $otp_{\alpha}(-)$. Our main result reads as follows.
**► Theorem 2.** For all countable ordinals $\alpha$ (and more generally for all $\alpha \le \omega_1^{\omega_1}$, where $\omega_1$ is the first uncountable ordinal), the following properties are equivalent:

- the MSO-$[otp_\alpha]$-theory of $\alpha$ is decidable,

- $\alpha < \omega^\omega$,

- $otp_\alpha(-)$ is MSO-definable.

Let us recall that the MSO-theory is known to be decidable for the class of ordinals smaller than $\omega_2$, as well as separately for each ordinal smaller than $\omega_2$ (see [12] for the countable case, [31] for ordinals up to $\omega_2$, and [21] for showing that this question is independent of ZFC at $\omega_2$, where $\omega_2$ is the first ordinal of the cardinality greater than the cardinality of $\omega_1$). It is clear that if $\alpha$ is an MSO-definable ordinal, then MSO-$[otp_\alpha]$ and MSO are effectively expressively equivalent, and thus MSO-$[otp_\alpha]$ is decidable. Our result shows that if $\alpha$ is not MSO-definable and smaller than or equals to $\omega_1^{\omega_1}$, then, the logic is strictly more expressive than MSO; however, decidability is lost.

Note that we do not rule out the possibility that there exists some uncountable ordinal $\alpha$ larger or equal to $\omega_1^{\omega_1}$ such that the MSO-$[otp_\alpha]$-theory of $\alpha$ is still decidable.

## 1.2 Overview of the proofs

For both theorems, the difficult part is to prove the undecidability of the theory.

The undecidability part of the first theorem, Theorem 1, is obtained from Theorem 2. The main observation is that when the lexicographically order over the leaves of a binary tree $T$ of Cantor-Bendixson rank $\alpha$, is an ordinal, then its order type is in the interval $[\omega^\alpha, \omega^{\alpha+1})$. This is the crux of the reduction of the undecidability.

The undecidability part of the second theorem, Theorem 2, amounts to prove the undecidability of the MSO-$[otp_\alpha]$-theory for all non MSO-definable ordinals $\alpha$ up to $\omega_1^{\omega_1}$. In fact, it boils down to treat three different cases.

- In Theorem 24, we prove that the MSO-$[otp_{\omega^\beta}$]-theory of $\omega^\beta$ is undecidable for all countable limit ordinals $\beta$ (or more generally for $\beta$ of cofinality $\omega$). This covers, in particular, the important case of $\omega^\omega$ which is the first non MSO-definable ordinal. This proof relies on a simple reduction of the BMSO-theory of $\omega$, which is known to be undecidable (see Theorem 9).

- In Theorem 25, we establish that the MSO-$[otp_{\omega^\beta}$]-theory of $\omega^\beta$ can be reduced to the MSO-$[otp_{\omega^{\beta+1}}$]-theory of $\omega^{\beta+1}$. This is the most interesting part. It involves using the construct $otp_{\omega^{\beta+1}}$ over an input that has been decomposed into $\omega$-blocks in such a way that in almost all the blocks it faithfully simulates $otp_{\omega^\beta}$.

- The two above results treat the case of all ordinals of the form $\omega^\beta$ that are smaller than $\omega_1^{\omega_1}$ and are not MSO-definable. But some ordinals are not of the form $\omega^\beta$, such as, for instance, $\omega^\omega + 1$. Extending the result to these cases requires some extra work, but can be achieved without difficulty.

Another argument in the proof is a characterization of MSO-definable ordinals. This is well known in the countable case: a countable ordinal $\alpha$ is MSO-definable if and only if it is smaller than $\omega^\omega$. For proving Theorem 2, there is also a need to characterize the MSO-definable ordinals smaller than $\omega_2$. We provide such a result in Theorem 45. This statement is not deep but, as far as we know, had not been mentioned before.

## 1.3 Historical Background

It was known in the 50s from Robinson that the extensions of MSO with a plus function, MSO($\mathbb{N}$, +), or even the doubling function MSO($\mathbb{N}$, <, $x \mapsto 2x$) were undecidable [27]. Elgot and Rabin studied in [17] the MSO theory of structures of the form $(\mathbb{N}, <, P)$, where $P$ is
11:4 On the Expansion of MSO with Cantor-Bendixson Rank and Order Type Predicates

some unary predicate. They give a sufficient condition on $P$ which ensures decidability of the MSO theory of $(\mathbb{N}, <, P)$. In particular, it holds when $P$ denotes the set of factorials, or the set of powers of some integer. The frontier between decidability and undecidability of related theories was explored in numerous later papers [14, 18, 30, 29, 26, 25, 33, 34, 1].

The Büchi decidability theorem result (and the automata method) was extended to the MSO theory of any countable ordinal [11], to $\omega_1$ - the first uncountable ordinal, and to any ordinal less than $\omega_2$ - the first ordinal of the cardinality greater than $\omega_1$, [13]. Gurevich, Magidor and Shelah [21] proved that the decidability status of the MSO theory of $\omega_2$ depends on set-theoretical assumptions. What can be said about MSO theories for linear orderings beyond ordinals? Using automata, Rabin [24] proved decidability of the MSO theory of the binary tree, from which he deduces decidability of the MSO theory of $\mathbb{Q}$, which in turn implies decidability of the MSO theory of the class of countable linear orderings. Shelah [31] improved model-theoretical techniques yielding new decidability proofs over linear orderings, and proved that the MSO theory of the real line $(\mathbb{R}, <)$ is undecidable. The frontier between decidable and undecidable cases was specified in later papers by Gurevich and Shelah [20, 22, 23]); we refer the reader to the survey [19].

A logic that was much studied in recent years, introduced in [4], is MSO+U. The logic MSO+U extends MSO with a new quantifier-like construct $UX.\varphi(X)$ expressing that there are sets of arbitrary large cardinality for which $\varphi(X)$ holds. Some non-trivial fragments of MSO+U are known to be decidable over $\omega$ (if this new construct is not allowed to appear negatively inside itesIf). [5]. It took more than ten years before it was shown undecidable over $\omega$ [8]. Works concerned with weak variants of this logic have also been pursued, yielding decidability results, such as in [9], but these cannot be considered as syntactic extensions of MSO.

The logic BMSO is a logic expressing properties of infinite sequences of numbers. It was designed in order to retain the quantitative aspects of MSO+U, while removing the ability to measure the cardinality of sets [2]. It turns out that its theory is intereducible to the one of MSO+U (see [2]), and thus it is also undecidable by [8]. The decidability of some important fragments of this logic still remain open. The undecidability result concerning MSO+U has been extended in [6], and then eventually, the existence of (almost) any significative extension of MSO that would retain decidability over $\omega$ has been ruled out in [7]: as soon as any non-regular property is expressible (with some mild closure assumption), then theory is undecidable. All these undecidability results boil down to reductions to the work [8].

The logic cost-MSO is another logic inspired by MSO+U, this time exhibiting the ability to express bound properties on the cardinality of sets, but removing the ability to quantify express asymptotic properties on these quantities. This logic is known to be decidable over finite words [15] and trees [16] over infinite words and partially over infinite trees [3]. The decidability status of cost-MSO over the full binary tree is a difficult open problem in the area.

1.4 Structure of the paper

Some definitions and results concerning MSO and BMSO are recalled in Section 2. Section 3 establishes our result over infinite trees, namely Theorem 1. Section 4 presents the proof of Theorem 24 stating that the MSO[$otp_{\omega^\beta}$]-theory of $\omega^\beta$ is undecidable for all countable limit ordinals $\beta$ (or more generally $\beta$ of cofinality $\omega$). In Section 5, we prove that the MSO[$otp_{\omega^\beta}$]-theory of $\omega^\beta$ can be reduced to the MSO[$otp_{\omega^{\beta+1}}$] of $\omega^{\beta+1}$ (Theorem 25). In Section 6, we combine the results of the two previous sections for proving our main result, Theorem 2, for all countable ordinals. Section 7 concludes the paper.
For space considerations all the results beyond the countable case, i.e., for ordinals up to $\omega_1^{\omega_1}$, do not appear in the main body of the submission, and are found in Appendix B.

## 2 Preliminaries

In this section we recall standard definitions and notions about ordinals (Section 2.1), monadic second-order logic (Section 2.2) and definability (Section 2.3). In Section 2.4, we introduce BMSO, and the undecidability Theorem 9 for it, which is crucial in our proof.

### 2.1 Ordinals

We shall use the standard terminology over ordinals. Here, an ordinal is seen, up to isomorphism, as a set equipped with a well-founded total order $<$. We use the classical notations over ordinals (order, sum, product, exponentiation). A limit ordinal is a non-empty ordinal that has no maximal element. A successor ordinal is an ordinal that has a maximum.

Given a subset $X$ of an ordinal $\alpha$, we denote $\alpha|_X$ its restriction to $X$. The order type of $X$ is the ordinal $\alpha|_X$. We shall denote $[x, y)$ the set of $\{z \in \alpha: x \le z < y\}$, and $[x, \infty)$ for the set $\{z \in \alpha: x \le z\}$. An interval of the form $[x, \infty)$ is called a final non-empty segment. Given an ordinal $\alpha$, a set $X$ is cofinal (in $\alpha$) if for all $x \in \alpha$, there is $y \in X$ with $y \ge x$. The cofinality of $\alpha$ is the least order type of $X$ for $X$ cofinal subset of $\alpha$. Let us recall that all countable limit ordinals have cofinality $\omega$.

### 2.2 Monadic second-order logic of order

We use standard notations and terminology about monadic second-order logic of order.

The monadic second-order logic of order (or monadic logic of order or simply monadic logic, abbreviated as MSO) is the extension of first-order logic over the signature $\{<\}$, where $<$ is a binary relational symbol interpreted as a total order, with (a) monadic (second-order) variables interpreted as subsets of the universe (usually denoted by uppercase letters $X, Y, Z$), (b) existential and universal quantifiers over monadic variables $\exists X.\psi$ and $\forall X.\psi$, and (c) atomic formulas $y \in X$ expressing that $y$ belongs to $X$.

In this paper, we shall always interpret this logic over partial orders or ordinals. Given a structure $M := (M, <)$, which is a model over the signature $\{<\}$, a monadic formula $\varphi(X_1, \dots, X_k, y_1, \dots, y_\ell)$, sets $U_1, \dots, U_k \subseteq M$, and elements $v_1, \dots, v_\ell \in M$, we denote the fact that the formula holds on the model $M$ with valuations $U_i$ for $X_i$, and $v_j$ for $y_j$ as

$$M \models \varphi(U_1, \dots, U_k, v_1, \dots, v_\ell).$$

We shall use the classical technique of relativization of formulas. The next lemma is obtained easily by a syntactic transformation of the formula.

**► Lemma 3 (Relativization).** Let $\varphi(Y_1, \dots, Y_l)$ be a formula, $U$ a variable not appearing in $\varphi$. We can compute a formula $\varphi^U(Y_1, \dots, Y_l, U)$ such that for every structure $M$ and every non-empty $D \subseteq M$ and every $l$-tuple $\bar{P}$ of subsets of $D$:

$$M \models \varphi^U(\bar{P}, D) \text{ if and only if } M|_D \models \varphi(\bar{P}),$$

where $M|_D$ is the substructure of $M$ over $D$.

When this is the case, we say that $\varphi$ holds in $(M, \bar{P})$ relativized to $D$.
11:6 On the Expansion of MSO with Cantor-Bendixson Rank and Order Type Predicates

To ease the notation, we shall use some shorthands such as overlined variables $\bar{X}, \bar{Y}$ to denote tuples of monadic variables. We allow ourselves to write $X \subseteq Y$ to denote the inclusion of sets, and we use more generally any abbreviation if it is clear that it can be translated into MSO syntax. For instance, we shall use formulas such as (“X is cofinal” $\wedge$ “X has order type $\omega$”).

The main results concerning the MSO-theory of ordinals are the following:

► **Theorem 4** ([12]). *The MSO-theory of the class of countable ordinals is decidable. The MSO-theory of every countable ordinal is decidable.*

► **Theorem 5** ([31]). *The MSO-theory of the class of ordinals smaller than $\omega_2$ is decidable. The MSO-theory of every ordinal smaller than $\omega_2$ is decidable.*

► **Theorem 6** ([21]). *The MSO-theory of $\omega_2$ is independent of ZFC.*

Given an ordinal $\beta$, we consider the extension of monadic logic in which the extra atomic formula $otp_\beta(X)$ for $X$ a monadic variable can be used, and is interpreted in an ordinal $\alpha$ as “the order type of $X$ is $\beta$”. It is denoted $\text{MSO}[otp_\beta]$.

2.3 Definability

We say that a sentence $\psi$ *defines the ordinal* $\alpha$ if $\alpha$ is the unique ordinal such that $\alpha \models \psi$. An ordinal $\alpha$ is *definable in logic L*, or simply (*L-definable*) if there is a sentence of L that defines $\alpha$. The following important lemma is well known.

► **Lemma 7.** For all countable ordinals $\alpha$, $\alpha$ is MSO-definable if and only if $\alpha < \omega^\omega$.

Definability of ordinals below $\omega^\omega$ is fairly straightforward, by an inductive definition. The undefinability above $\omega^\omega$, follows from the small model property for MSO over the countable ordinals.

We say that a formula $\psi(x)$ *defines $\alpha$ inside the ordinal* $\beta$ if there is a unique $b \in \beta$ such that $\beta \models \psi(b)$ and the $[0, b)$ has order type $\alpha$. For a logic L, $\alpha$ is L-definable inside $\beta$ if there is a formula $\psi(x) \in L$ that defines $\alpha$ in $\beta$.

It is clear that if $\alpha$ is MSO or $\text{MSO}[otp_\alpha]$-definable by some sentence, then, by relativization of the sentence to $[0, b)$ it is definable inside $\beta$ with the same logic for every $\beta > \alpha$. However, the other direction fails, as witnessed by the next lemma, to be put in contrast with Theorem 7.

► **Lemma 8.** $\omega^\omega$ is MSO-definable inside $\beta := \omega^\omega + \gamma$ for every $0 < \gamma < \omega^\omega$.

*Proof.* By Theorem 7, there exists an MSO-sentence $\psi_\gamma$ that defines $\gamma$. The formula that says that $x$ is the minimal element such that $\psi_\gamma$ holds when relativized to $[x, \infty)$. $\quad \blacksquare$

2.4 BMSO

The BMSO-logic is an extension of MSO that can express the existence of a bound on numerical quantity. Formally, the syntax of BMSO is the same as the one of MSO, extended with a new construct $B(X)$, for $X$ a monadic variable. These formulas are interpreted on *ω-sequences of natural numbers*, that we see as the ordinal $\omega$ extended with a map $f$ from $\omega$ to $\mathbb{N}$. The construct $B(X)$ is interpreted as “there exists $n \in \mathbb{N}$ such that $f(x) \le n$ for all $x \in X$”.

For instance, the formula $u \models \forall X.B(X)$ for an *ω*-sequence of natural numbers $u$ if and only if $u$ is bounded. The formula $\forall X.(\forall x \in X.\exists y \in X.(x < y)) \rightarrow \neg B(X)$ expresses the non-existence of an infinite set which is bounded: in other words, it expresses that $f$ tends to infinity.
**► Theorem 9 (consequence of [2, 8]).** *Satisfiability of BMSO is undecidable over ω-sequences of natural numbers.*

*Proof.* Theorem 2 in [2] states that BMSO is equivalent to another logic, AMSO. Theorem 13 states that the satisfiability of AMSO is equivalent to the one of MSO+U. Finally, Theorem 1.1 in [8] establishes the undecidability of MSO+U. ◀

### 3 The tree case

In this section we derive Theorem 1 from Theorem 2. This section is organized as follows. First, we recall some standard definitions and results about trees. Then, we recall a definition of Cantor-Bendixson rank of trees and state some well-known facts. Finally, we prove Theorem 1.

#### 3.1 Trees

A tree $(T, <)$ is a structure over a signature with a unique binary relation $< $ such that (1) there is a minimal element (called the *root*), and (2) for every $b \in T$ the set $\{a \mid a < b\}$ is finite and linearly ordered by $<$. Elements of the tree are called *nodes*. A node $u$ is *parent* of a node $v$ (and $v$ is a *child* of $u$) if $u < v$ and there is no $w$ such that $u < w < v$. A tree is *binary* if every node has at most two *children*. Nodes $u$ and $v$ are *incomparable* if neither $u \le v$ nor $v \le u$. An *antichain* is a subset of a tree such that all pairs of distinct nodes are *incomparable*. For a subset $A$ of a tree we denote by $A\downarrow$ the downward closure of $A$, i.e., the set $\{b \mid \exists a \in A(b < a)\}$. For a node $u$, denote $T^{u\uparrow}$ the tree $T$ restricted to nodes that are above or equal to $u$. $T^{u\uparrow}$ is itself a tree, and is called the *subtree at u*. Note that if $T$ is a *binary tree*, then $T^{u\uparrow}$ also is. A tree is *regular* if it has finitely-many subtrees up to isomorphism.

The *full binary tree* is a tree for which (a) there is a partition of the children into *left* and *right children* and (b) all nodes have exactly two children, one being *left*, and the other *right*. The full binary tree is considered as a structure for the signature $\{<, \text{Left}(\AA), \text{Right}(\AA)\}$. The *standard representation* of the full binary tree has as the domain the finite strings over $\{L, R\}$; the relation $<$ is interpreted as the prefix relation, and a node is *left* (respectively, *right*) if its last letter is $L$ (respectively, $R$).

The major decidability result is *Rabin's theorem* [24]:

**► Theorem 10.** *The MSO-theory of the full binary tree is decidable.*

We shall also use the so-called *Rabin's Basis Theorem* [24]:

**► Theorem 11.** *If an MSO-sentence has a [binary] tree model, it has a [binary] regular tree model.*

We use $<_{lex}$ for the lexicographical (linear) order on the nodes of the full binary tree. It is definable in the standard way. Rabin proved [24] that there is a definable antichain $Q$ such that $(Q, <_{lex})$ is order isomorphic to the rationals. As a consequence, he obtained that the MSO-theory of the rationals is decidable. Moreover, since every countable ordinal is embedable into the rationals, and “$(A, <)$ is an ordinal” is MSO-definable, he derived that the MSO-theory of the class of countable ordinals is decidable.

We will use the fact that $<_{lex}$ is MSO-definable, “$A$ is an antichain” and “$A\downarrow$” are MSO-definable.
11:8 On the Expansion of MSO with Cantor-Bendixson Rank and Order Type Predicates

3.2 Cantor-Bendixson rank

We are going to define the Cantor-Bendixson rank (or CB rank) of a binary tree. There are
several equivalent definitions. The only properties of Cantor-Bendixson rank that we need
are stated in Theorem 16 and Theorem 17. The reader might skip the definition and use
these lemmas as black-boxes.

► **Definition 12 (Sum of trees).** Let $T_i = (|T_i|, <_i)$ for $i \in \{0,1\}$ be trees over disjoint universes. their sum is the tree $T_0 + T_1$ with universe $|T_0| \cup |T_1|$ and its order relation defined as $n_1 \le n_2$ if there is $i \in \{0,1\}$ such that $n_1, n_2 \in |T_i|$ and $n_1 \le_i n_2$, or $n_1$ is the root of $T_0$.

The $\omega$-sum of trees is defined as follows.

► **Definition 13** (*ω*-sum of trees). Let $T_i = (|T_i|, <_i)$ for $i \in \omega$ be trees over disjoint universes.
We define the tree

$$
\sum_{i \in \omega} T_i
$$

as having universe $\bigcup_{i \in \omega} |T_i|$ and its order relation is defined as $n_1 \le n_2$ if there is $i$ such that $n_1, n_2 \in |T_i|$ and $n_1 \le_i n_2$ or $n_1$ is the root of $T_i$ and $n_2 \in |T_j|$ for $j \ge i$.

If the disjointness assumption does not hold, we replace $T_i$ by disjoint isomorphic copies
and proceed as above.

In order to simplify notations, we will consider only finitely branching trees. The sets of
trees of Cantor-Bendixson rank $\le \alpha$ can be defined by transfinite induction.

► **Definition 14 (Cantor-Bendixson rank of a tree).** Define two families of trees CBrank<sub>α</sub> and CBrank<sub>α</sub><sup>+</sup>, where α is a countable ordinal.

1. CBrank<sub>0</sub> contains only one element trees.

2. CBrank<sub>α</sub> is the closure of ⋃<sub>β≤α</sub> CBrank<sub>β</sub> under +, i.e. T ∈ CBrank<sub>α</sub><sup>+</sup> if T = T<sub>0</sub> + T<sub>1</sub> + ... + T<sub>k</sub> for T<sub>i</sub> ∈ ⋃<sub>β≤α</sub> CBrank<sub>β</sub>.

3. CBrank<sub>α</sub> := Σ<sub>i∈ω</sub> T<sub>i</sub>, where T<sub>i</sub> ∈ CBrank<sub>β</sub><sup>+</sup> for β < α.

If there is no α such that T ∈ CBrank<sub>α</sub><sup>+</sup>, then the Cantor-Bendixson rank is undefined;
otherwise we set CBrank(T) of T to be inf{α | T ∈ CBrank<sub>α</sub><sup>+</sup>}, and the tree is called tame.

It is well known that a tree *T* has a CB rank if there is no embedding of the full binary
tree in *T*, equivalently, *T* has only countably many branches. We are not going to use this
fact.

► **Example 15.** Let $S_1$ be the subtree of the full binary tree $T_2$ over $R^*$, $S_2$ the subtree of $T_2$ over $R^*L^*$. Let $S_{2i}$ (respectively, $S_{2i+1}$) be the subtree of $T_2$ over $(R^*L^*)^i$ (respectively, over and $(R^*L^*)^i R^*$). Then CBrank($S_i$) = $i$ for $i \ge 1$. Let $S'_1$ be the subtree of $T_2$ over $R^*L$; then CBrank($S'_1$) = 1.

The following lemma is well-known and is easily proved by induction.

**► Lemma 16.** For every $n \in \mathbb{N}$, the set of binary trees of Cantor-Bendixson rank $n$ is definable, i.e., there is an MSO sentence $\phi_n$ such that $(T, <) \models \phi_n$ if $(T, <)$ is a binary tree of Cantor-Bendixson rank $n$.

The next lemma is proved in the Appendix.

**► Lemma 17.** Let $X$ be an antichain in the full binary tree such that $(X, <_{lex})$ is isomorphic to an ordinal. Then, $(X \downarrow, <)$ has Cantor-Bendixson rank $\alpha$ if and only if the order type of $(X, <_{lex})$ belongs to $[\omega^{\alpha}, \omega^{\alpha+1})$.
### 3.3 Theorem 2 implies Theorem 1

Now, relying on Lemma 17, we can express in $MSO[CBrank_\alpha]$ that the order type of $(X, <_{lex})$ is $\omega^\alpha$ for an antichain $X$ of the full binary tree. The conjunction $\varphi_{\omega^\alpha}(X)$ of (1)-(5) below expresses this property.

1. $X$ is an antichain:

$$ \forall y \in X \forall x \in X (y \le x) \rightarrow (x = y) $$

2. $(X, <_{lex})$ is isomorphic to an ordinal, i.e., every non-empty subset has a minimum element:

$$ \forall Y \subseteq X ((Y \neq \emptyset) \rightarrow \exists y \in Y (\forall z \in Y (y \le z_{lex} z))) $$

3. The downward closure of $X$ has the $CB$ rank $\alpha$:

$$ CBrank_\alpha(X \downarrow), \text{ and} $$

4. For every final non-empty segment $Y$ of $(X, <_{lex})$ the $CB$ rank of the downward closure of $Y$ is $\alpha$:

$$ \forall y \in X (CBrank_\alpha(\{z \in X | z \ge y\} \downarrow)). $$

5. For no proper prefix $(Y, <_{lex})$ of $(X, <_{lex})$ the $CB$ rank of the downward closure of $Y$ is $\alpha$.

(1)-(5) are not $MSO[CBrank_\alpha]$ formulas; however, they can be easily translated into (less readable) $MSO[CBrank_\alpha]$ formulas.

Next, let $\psi$ be an $MSO[otp_{\omega^\alpha}]$ sentence. Let $\psi^X$ be the relativization of $\psi$ to a fresh variable $X$. Let $\Psi^X \in MSO[CBrank_\alpha]$ be obtained from $\psi^X$ when all the occurrences of $otp_{\omega^\alpha}(Y)$ are replaced by $\varphi_{\omega^\alpha}(Y)$. Finally, let $\Psi$ be $\exists X (\varphi_{\omega^\alpha}(X) \wedge \Psi^X)$. Then, $\omega^\alpha \models \psi$ if and only if $\Psi$ holds in the full binary tree. Hence, we have:

**Lemma 18.** There is an algorithm that for every $MSO[otp_{\omega^\alpha}]$ sentence $\psi$ constructs an $MSO[CBrank_\alpha]$ sentence $\Psi$ such that $\omega^\alpha \models \psi$ if and only if $\Psi$ holds in the full binary tree.

Moreover, in Theorem 18, the algorithm treats $\alpha$ symbolically, i.e., if $\varphi$ is obtained from $\psi$ when $\alpha$ is replaced by $\beta$, then the corresponding translation of $\varphi$ replaces in $\Psi$ everywhere $\alpha$ by $\beta$.

As a corollary of Theorem 18, Theorem 7 and Theorem 2, we obtain:

**Corollary 19.** $MSO[CBrank_\alpha]$ is undecidable for every $\alpha \ge \omega$.

And as a corollary of Rabin's theorem, Theorem 10, we obtain:

**Corollary 20.** For all $\alpha \ge \omega$, the property "the $CB$ rank of a binary tree is $\alpha$" is not $MSO$-definable.

Theorem 1 follows from Theorem 10, Theorem 16, Theorem 19 and Theorem 20.
4 The $\omega^\beta$ case for $\beta$ an ordinal of cofinality $\omega$

The goal of this section is to establish Theorem 24, stating that the MSO[$otp_\alpha$]-theory of $\alpha$ is undecidable for $\alpha$ of the form $\omega^\beta$ where $\beta$ is a countable limit ordinal<fnref n="1" />. This covers in particular the case of $\omega^\omega$ which is the first non-definable ordinal. Theorem 24 is obtained by reduction from the undecidability of BMSO (Theorem 9).

For the rest of the section, we fix an ordinal $\beta$ which is limit of an $\omega$-sequence $\hat{\beta} := 0 = \beta_0 < \beta_1 < \dots$. This is possible for all countable limit ordinals, and more generally for ordinals that have cofinality $\omega$.

Given an ordinal $0 < \alpha < \omega^\beta$, it is said to be of $\hat{\beta}$-rank $k$ if $\omega^{\beta_k} \le \alpha < \omega^{\beta_{k+1}}$. Let us denote $\hat{\beta}$-rank($\alpha$) the $\hat{\beta}$-rank of $\alpha$. Recall that $\alpha|_X$ is the substructure of $\alpha$ over $X$. If $X$ is some subset of an ordinal $\alpha$, we also denote $\hat{\beta}$-rank($X$) for the $\hat{\beta}$-rank($\alpha|_X$).

The key argument used in this section is that we can relate the order type of some infinite sums of ordinals to the boundedness of sequences of $\hat{\beta}$-ranks. This is formalized in the following lemma.

**Lemma 21.** *Given an $\omega$-sequence $(\alpha_i)_{i \in \omega}$ of ordinals smaller than $\omega^\beta$, then the following properties are equivalent:*

$$ \text{■} \sum_{i \in \omega} \alpha_i = \omega^\beta, $$

*The $\omega$-sequence of natural numbers defined for all $i \in \omega$ as $u_i := \hat{\beta}$-rank($\alpha_i$) is unbounded.*

**Proof.** Assume the ranks of the $\alpha_i$ are unbounded, then there exists an increasing $\omega$-sequence $0 = i_0 < i_1 < \dots$ such that $j \le \hat{\beta}$-rank($\alpha_{i_j}$) for all $j$. As a consequence, we have $\omega^{\beta_j} \le \alpha_{i_j} \le \sum_{i=i_j}^{i_j+1} \alpha_i$ for all $j$. We obtain

$$ \omega^{\beta} = \sum_{j \in \omega} \omega^{\beta_j} \le \sum_{j \in \omega} \sum_{i=i_j}^{i_j+1} \alpha_i = \sum_{i \in \omega} \alpha_i . $$

Conversely, assume the $\hat{\beta}$-ranks of the $\alpha_i$'s would be bounded by some $N$; this means that $\alpha_i \le \omega^{\beta_{N+1}}$ for all $i$. We get $\sum_{i \in \omega} \alpha_i \le \omega^{\beta_{N+1}} \times \omega < \omega^\beta$. $\quad \blacksquare$

Let $S \subseteq \omega^\beta$ be of order type $\omega$. This means that there exists an increasing $\omega$-sequence $s_0 < s_1 < \dots$ with $S = \{s_i : i \in \omega\}$. We abbreviate it as $S = \{s_0 < s_1 < \dots\}$. Given a set $S = \{s_0 < s_1 < \dots\} \subseteq \omega^\beta$, it is said to *encode the sequence* $u \in \mathbb{N}^\omega$ defined as $u(i) = \hat{\beta}$-rank($[s_i, s_{i+1})$) for all $i \in \omega$. Finally, given a set $X \subseteq \omega$, the *S-code of X*, written $\overline{X}^S$, is defined as

$$ \overline{X}^S := \bigcup_{i \in X} [s_i, s_{i+1}) . $$

**Fact 22.** *The key facts concerning these definitions are the following:*

1. All $\omega$-sequences of natural numbers $u \in \mathbb{N}^\omega$ are encoded by some $\omega$-sequence $S = \{s_0 < s_1 < \dots\}$. Take, for instance, $s_i = \omega^{\beta_{u(i)}} + \omega^{\beta_{u(i+1)}} + \dots + \omega^{\beta_{u(i-1)}}$ for all $i \in \omega$.

2. Conversely, every $S \subseteq \omega^\beta$ of order type $\omega$ encodes a sequence $u \in \mathbb{N}^\omega$; namely, the one in which $u(i)$ is the $\beta$-rank of $[s_i, s_{i+1})$ for all $i \in \omega$.

3. For sets $S$ and $X$, “$S$ is of order type $\omega$”, and “$X$ is an $S$-coded set”, are properties definable in first-order logic ($X$ and $S$ are seen as unary predicates).

4. If $S$ encodes $u$, then $u \models \neg B(X)$ if and only if $\omega^\beta \models otp_{\omega^\beta}(\overline{X}^S)$. This is a direct consequence of Theorem 21 applied to the sequence of $\alpha_i$, where $X = \{x_0 < x_1 < \dots\}$ and $\alpha_i$ is the order type of $[s_{x_i}, s_{x_i+1})$.

<footnote n="1">¹ This works in the more general case of $\beta$ being a limit ordinal of cofinality $\omega$.</footnote>
**Lemma 23.** Given a formula $\varphi(X_1, \dots, X_k, x_1, \dots, x_l)$ of BMSO, there exists effectively a formula $\varphi^*(S, X_1, \dots, X_k, x_1, \dots, x_l)$ of MSO$[otp_{\omega^\beta}]$ such that whenever $S$ encodes $u$, $A_i \subseteq \omega$, and $a_j \in \omega$,

$$u \models \varphi(A_1, \dots, A_k, a_1, \dots, a_\ell)$$

if and only if

$$\omega^\beta \models \varphi^*(S, \overline{A_1}^S, \dots, \overline{A_k}^S, s_{a_1}, \dots, s_{a_\ell}).$$

**Proof.** The translation is defined by structural induction, as in the following table:

$$(x < y)^* := x < y,$$

$$(x \in X)^* := x \in X,$$

$$(B(X))^* := \negotp_{\omega^\beta}(X),$$

$$(\varphi \wedge \psi)^* := \varphi^* \wedge \psi^*,$$

$$(\forall x \psi)^* := \forall x (x \in S \rightarrow \psi^*),$$

$$(\neg \varphi)^* := \neg \varphi^*,$$

$$(\forall X \psi)^* := \forall X (\text{"X is an S-coded set"} \rightarrow \psi^*).$$

The conclusion of the lemma is obtained along the same induction, relying on Theorem 22. ◀

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

**Corollary 24.** For all countable limit ordinals $\beta$ (and more generally for all ordinals of cofinality $\omega$), the MSO$[otp_{\omega^\beta}$]-theory of $\omega^\beta$ is undecidable.

**Proof.** Consider a BMSO sentence $\varphi$, and, using the notations in Theorem 23, and the above facts, construct the sentence

$$\psi := \exists S (\text{"S has order type } \omega \text{ "} \wedge \varphi^*(S)).$$

Then, $\varphi$ has a sequence $u \in \mathbb{N}^\omega$ which models it if and only if $\omega^\beta$ models $\psi$. Indeed, if $u \models \varphi$, one can take some $S \subseteq \omega^\beta$ encoding $u$. It is of order type $\omega$ by definition, and by Theorem 23, $\omega^\omega \models \varphi^*(S)$. Conversely, if some $S$ is the witness that $\omega^\omega \models \psi$, then $S$ is of order type $\omega$. Thus $S$ encodes some sequence $u \in \mathbb{N}^\omega$, and since $\omega^\beta \models \varphi^*(S)$, by Theorem 23, $u \models \varphi$. In combination with Theorem 9, we get that the MSO$[otp_{\omega^\beta}$]-theory of $\omega^\beta$ is undecidable. ◀

# 5 Reduction of MSO$[otp_{\omega^\beta}$] to MSO$[otp_{\omega^{\beta+1}}]$

We have shown in the previous section the undecidability of MSO$[otp_{\omega^\beta}$] for $\beta$ an ordinal of cofinality $\omega$. In this section, we show that if MSO$[otp_{\omega^{\beta+1}}]$ is decidable for some $\beta$, then the same goes for MSO$[otp_{\omega^\beta}$]. This case requires more work.

We aim at proving the following:

**Lemma 25.** For all ordinals $\beta$, the MSO$[otp_{\omega^\beta}$]-theory of $\omega^\beta$ is reducible to the MSO$[otp_{\omega^{\beta+1}}]$-theory of $\omega^{\beta+1}$.

In other words, given an MSO$[otp_{\omega^\beta}$]-sentence $\varphi$, our goal is to construct an MSO$[otp_{\omega^{\beta+1}}]$-sentence $\psi$ such that

$$\omega^\beta \models \varphi \quad \text{if and only if} \quad \omega^{\beta+1} \models \psi.$$

The principle of this construction is that formula $\psi$ will guess a decomposition of $\omega^{\beta+1}$ into $\omega$ intervals, such that almost all of them have order type $\omega^\beta$. The intuition is then that formula $\psi$ will “simulate” $\varphi$ independently in each of these blocks. The construction is done in such a way that this “simulation” is “faithful” on almost all the blocks. There, we say that a unary property $P$ holds for almost all elements of a set $D$ if $P$ holds on all, but finitely many elements of $D$.
11:12 On the Expansion of MSO with Cantor-Bendixson Rank and Order Type Predicates

The first key ingredient for achieving this is Theorem 27. It provides an MSO[$otp_{\omega^{\beta+1}}$]-
formula that allows to chop $\omega^{\beta+1}$ into $\omega$ pieces while guaranteeing that almost all of them
are of order type $\omega^{\beta}$.

We first state some elementary facts about ordinals that will prove useful in the construc-
tion.

► **Fact 26.** *The following standard facts hold:*

1. The order type of every final non-empty segment of $\omega^\beta$ has order type $\omega^\beta$.

2. Let $(\alpha_i)_{i \in \omega}$ be an $\omega$-sequences of ordinals smaller than $\omega^{\beta+1}$. Then $\sum_{i \in \omega} \alpha_i = \omega^{\beta+1}$ if and only if $\alpha_j \ge \omega^\beta$ for infinitely many $j$.

3. For all ordinals $\alpha < \omega^{\beta+1}$, either $\alpha = \omega^{\beta} \times k$ for some natural $k > 0$, or $\alpha$ has some final non-empty segment of order type smaller than $\omega^{\beta}$.

**Lemma 27.** *There is effectively an MSO[$otp_{\omega^{\beta+1}}$] formula Split<sub>ω<sup>β</sup></sub><sup>aa</sup>(X) such that for all S = {s<sub>0</sub> < s<sub>1</sub> < ...}, ω<sup>β+1</sup> |= Split<sub>ω<sup>β</sup></sub><sup>aa</sup>(S) if and only if the order type of [s<sub>i</sub>, s<sub>i+1</sub>) is ω<sup>β</sup> for almost all i ∈ ω.*

**Proof.** We proceed in three steps, in which we successively describe formulas that approximate each time better the expected behavior of Split<sub>ω<sup>β</sup></sub><sup>aa</sup>.

**Step 1.** The MSO[$otp_{\omega^{\beta+1}}$]-formula Split<sub>ω<sup>β</sup>×*</sub><sup>∞</sup>(S) expressing that

- $\bigcup_{i \in \omega} [a_i, s_{i+1})$ has order type $\omega^{\beta+1}$ for all $(a_i)_{i \in \omega}$ such that $a_i \in [s_i, s_{i+1})$ for all $i \in \omega$, which holds if and only if there exist infinitely many indices $i \in \omega$ such that $[s_i, s_{i+1})$ is of the order type $\omega^\beta \times k$ for some $k \ge 1$.

Indeed, assume that $[s_i, s_{i+1})$ is of the form $\omega^\beta \times k$ with $k \ge 1$ for infinitely many $i \in \omega$, then by the first item of Theorem 26, $[a_i, s_{i+1})$ has an order type of the form $\omega^\beta \times \ell$ with $\ell \ge 1$ for these $i$'s. Consequently, by the second item of Theorem 26, $\bigcup_{i \in \omega} [a_i, s_{i+1})$ has order type $\omega^{\beta+1}$.

Conversely, assume that $[s_i, s_{i+1})$ is not of the form $\omega^\beta \times k$ with $k \ge 1$ for almost all $i \in \omega$. This means by the third item of Theorem 26, that for these $i$'s, there exists $a_i \in [s_i, s_{i+1})$ such that the order type of $[a_i, s_i)$ is smaller than $\omega^\beta$. This can be completed, by choosing arbitrary $a_i$ in the finitely many other segments, into an $\omega$-sequence of $a_i$'s as in the formula. This time using the second item of Theorem 26, we get that $\bigcup_{i \in \omega} [a_i, s_{i+1})$ has an order type smaller than $\omega^{\beta+1}$.

**Step 2.** In a second step, we claim that the formula Split<sub>ω<sup>β</sup>×*</sub><sup>aa</sup> that expresses that

- for all infinite sets $S' \subseteq S$, $\text{Split}_{\omega^{\beta} \times *}^{\infty}(S')$ holds if and only if $[s_i, s_{i+1})$ is of the form $\omega^\beta \times k$ with $k \ge 1$ for almost all $i \in \omega$.

Indeed, if $[s_i, s_{i+1})$ is of the form $\omega^\beta \times k$ with $k \ge 1$ for almost all $i \in \omega$, this also holds for every infinite subsequence, and as a consequence, $\text{Split}_{\omega^{\beta} \times *}^{\infty}(S')$ for all infinite $S' \subseteq S$.

Conversely, assume that $[s_i, s_{i+1})$ is not of the form $\omega^\beta \times k$ with $k \ge 1$ for infinitely many $i \in \omega$. In this case, it is possible to extract a subsequence $S' = \{s'_0 < s'_1 < \dots\} \subseteq S$ such that the order type of $[s'_i, s'_{i+1})$ is not of the form $\omega^\beta \times k$ with $k \ge 1$, for all $i \in \omega$. According to the previous step, $\text{Split}_{\omega^{\beta} \times *}^{\infty}(S')$ does not hold for this choice of $S'$, and hence $\text{Split}_{\omega^{\beta} \times *}^{\infty}(S)$ does not either.

**Step 3.** Finally, we can define the formula Split<sub>ω<sup>β</sup></sub><sup>aa</sup>(S) that expresses that

- Split<sub>ω<sup>β</sup>×*</sub><sup>aa</sup>(S) holds, and

- for all $S' \supseteq S$, if Split<sub>ω<sup>β</sup>×*</sub><sup>aa</sup>(S') holds then $S' \setminus S$ is not cofinal.
We have to show that it fulfils the conclusion of the lemma, i.e., that $\text{Split}_{\omega^\beta}^{aa}(S)$ holds if and only if the order type of $[s_i, s_{i+1})$ is $\omega^\beta$ for almost all $i \in \omega$.

Indeed, assume that $[s_i, s_{i+1})$ has order type $\omega^\beta$ for almost all $i \in \omega$, and consider some $S' = \{s'_0 < s'_1 < \dots\} \supseteq S$. If $S' \setminus S$ is cofinal, then for such sufficiently large $j$, we would have that $s_i < s'_j < s_{i+1}$ for some $i$ such that $[s_i, s_{i+1})$ has order type $\omega^\beta$. But in this case, $[s_i, s'_j)$ has an order type smaller than $\omega^\beta$ and since $s'_{j-1} \ge s_i$, the interval $[s'_{j-1}, s'_j)$ also does. Overall, we have constructed infinitely many intervals $[s'_{j-1}, s'_j)$ of order type smaller than $\omega^\beta$, and thus $\text{Split}_{\omega^\beta \times *}^{aa}(S')$ does not hold. This is a contradiction, and hence $\text{Split}_{\omega^\beta}^{aa}(S)$ is satisfied.

Conversely, assume by contradiction that $\text{Split}_{\omega^\beta}^{aa}(S)$ holds, and that $[s_i, s_{i+1})$ has an order type different than $\omega^\beta$ for infinitely many $i \in \omega$. Since $\text{Split}_{\omega^\beta \times *}^{aa}(S)$ holds, this means that $[s_i, s_{i+1})$ has order type $\omega^\beta \times k$ with $k > 1$ for infinitely many $i \in \omega$. But each such interval $[s_i, s_{i+1})$ can be decomposed into $[s_i, s'_i)$ and $[s'_i, s_{i+1})$, both of them of order type $\omega^\beta \times k$ for some $k \ge 1$. Thus, the set $S'$ obtained by adding to $S$ all such elements $s'_i$ would make $\text{Split}_{\omega^\beta \times *}^{aa}(S')$ satisfied. Since $S' \setminus S$ is infinite, this contradicts the fact that $\text{Split}_{\omega^\beta}^{aa}(S)$ holds. ◀

From now on, we assume that $S = \{s_0 < s_1 < \dots\}$ is such that $\text{Split}_{\omega^\beta}^{aa}(S)$ holds. Let $\alpha_i$ be the order type of $[s_i, s_{i+1})$ be the corresponding sequence of ordinals. For the sake of simplicity, we shall not mention the first order variables in formulas in the rest of the proof, since these can be seen as a special case of monadic variables that would be interpreted as singletons (something definable).

**► Lemma 28.** There is an algorithm which given an MSO$[\text{otp}_{\omega^\beta}]$-formula

$\varphi(X_1, \dots, X_k),$

constructs an MSO$[\text{otp}_{\omega^{\beta+1}}]$-formula

$\varphi^*(S, F, X_1, \dots, X_k)$

such that for all $A_1, \dots, A_k \subseteq \omega^{\beta+1}$ and all infinite $F \subseteq \omega$,

$\omega^{\beta+1} \models \varphi^*(S, \bar{F}^S, A_1, \dots, A_k)$

if and only if

$\omega^{\beta+1}|_{[s_i, s_{i+1})} \models \varphi(A_1 \cap [s_i, s_{i+1}), \dots, A_k \cap [s_i, s_{i+1}))$

for almost all $i \in F$.

**Proof.** We shall define the formula $\varphi^*$ by structural induction on $\varphi$, and establish the conclusions of the lemma at the same time. The case of existential quantifier, the case of conjunction, and the case of MSO predicates are elementary. The crucial point is the negation.

For the sake of simplicity, we shall write $\omega^{\beta+1} \models^{S,F} \varphi(\bar{A})$ in order to express that $\omega^{\beta+1}|_{[s_i, s_{i+1})} \models \varphi(A_1 \cap [s_i, s_{i+1}), \dots, A_k \cap [s_i, s_{i+1}))$ for almost all $i$ such that $s_i \in F$.

Case of a conjunction, i.e., $\varphi(\bar{X}) = (\varphi_1(\bar{X}) \wedge \varphi_2(\bar{X}))$. We define

$\varphi^*(S, F, \bar{X}) := \varphi_1^*(S, F, \bar{X}) \wedge \varphi_2^*(S, F, \bar{X}) .$

The induction hypothesis holds: indeed, $\omega^\beta \models \varphi^*(S, F, \bar{A})$ if and only if $\omega^\beta \models \varphi_1^*(S, F, \bar{A})$ and $\omega^\beta \models \varphi_2^*(S, F, \bar{A})$, if and only if (by induction hypothesis) $\omega^{\beta+1} \models^{S,F} \varphi_1(\bar{A})$ and $\omega^{\beta+1} \models^{S,F} \varphi_2(\bar{A})$, if and only if $\omega^{\beta+1} \models^{S,F} \varphi_1(\bar{A}) \wedge \varphi_2(\bar{A})$, if and only if $\omega^{\beta+1} \models^{S,F} \varphi(\bar{A})$.
11:14 On the Expansion of MSO with Cantor-Bendixson Rank and Order Type Predicates

Case of an existential set quantifier, i.e., $\varphi(\bar{X}) = \exists Y. \varphi_1(\bar{X}, Y)$. We define

$$ \varphi^*(S, F, \bar{X}) := \exists Y. \varphi_1^*(S, F, \bar{X}, Y). $$

Correctness is also straightforward.

Case of an MSO-formula $\varphi(\bar{X})$, and in particular of the atomic formulas $x \in Y$ and $x < y$ (recall that in this case, we see first-order variable as singleton sets). In this case, we simply set $\varphi^*(S, \overline{F^S}, \bar{X})$ to express $\omega^{\beta+1} \models^{S,F} \varphi(\bar{X})$. This is easily definable using relativization and the fact that “almost all” can be expressed in MSO.

Case of an order type predicate, i.e., $\varphi(\bar{X}) := \text{otp}_{\omega^{\beta}}(X_m)$. For simplicity, we shall treat the case of $\varphi(\bar{X}) := \neg \text{otp}_{\omega^{\beta}}(X_m)$, and leave the question of removing the negation to the negation case below. We set:

$$ \varphi^*(S, F, \bar{X}) := \neg \text{otp}_{\omega^{\beta+1}}(X_m \cap \overline{F^S}). $$

The correctness of this construction relies on the second item of Theorem 26. Indeed, “otp$_{\omega^{\beta+1}}(A_m \cap \overline{F^S})$ does not hold” means that $A_m \cap [s_i, s_{i+1})$ has order type smaller than $\omega^{\beta}$ for almost all $i \in F$, which is the same as $\omega^{\beta+1} \models^{S,F} \neg \text{otp}_{\omega^{\beta}}(X_m)$.

Case of a negation, i.e., $\varphi(\bar{X}) = \neg \varphi_1(X_1, \dots, X_k)$. We set

$$ \varphi^*(S, F, \bar{X}) := \forall F' \subseteq F. (\text{"$F'$ infinite"}) \rightarrow \neg \varphi_1^*(S, F', \bar{X}). $$

Let us prove that the induction hypothesis holds. Let us assume that $\omega^{\beta+1} \models^{S,F} \neg \varphi(\bar{A})$. This is equivalent to the fact that $\neg \varphi(\bar{A} \cap [s_i, s_{i+1}))$ holds for almost all $i$ with $s_i \in F$. Hence, this is also true for almost all $i$ such that $s_i \in F'$ when $F' \subseteq F$ is infinite. Thus $\omega^{\beta+1} \models \varphi^*(S, F, \bar{A})$. Conversely, assume that $\omega^{\beta+1} \models^{S,F} \neg \varphi(\bar{A})$ does not hold. This means that there are infinitely many $i$ such that $s_i$ in $F$ and $\varphi(\bar{A} \cap [s_i, s_{i+1}))$ holds. Let us chose $F' \subseteq F$ infinite to contain these indices. Then, this $F'$ is a witness that $\omega^{\beta+1} \models \varphi^*(S, F, \bar{A})$ does not hold either. ◀

As a consequence of Theorem 28 and of Theorem 27, we obtain:

**Corollary 29.** For every MSO[$\text{otp}_{\omega^{\beta}}$]-sentence $\varphi$, there exists effectively an MSO[$\text{otp}_{\omega^{\beta+1}}$]-sentence $\psi$ such that

$$ \omega^{\beta} \models \varphi \quad \text{if and only if} \quad \omega^{\beta+1} \models \psi. $$

**Proof.** Set $\psi$ to be the formula

$$ \exists S \text{"$S$ has order type } \omega \text{"} \land \text{"$S$ is cofinal"} \land \text{Split}_{\omega^{\beta}}^{aa}(S) \land \varphi^*(S, S), $$

in which $\varphi^*$ is the formula produced by Theorem 28.

First implication. Let us assume that $\omega^{\beta} \models \varphi$. We have to prove that $\omega^{\beta+1} \models \psi$. For this, let us choose $S$ to be $\{s_i := \omega^{\beta} \times i \mid i < \omega\}$. This set $S$ is of order type $\omega$ and cofinal in $\omega^{\beta+1}$. It is also such that $[s_i, s_{i+1})$ as order type $\omega^{\beta}$ for all $i$. Hence, by Theorem 27, $\omega^{\beta+1} \models \text{Split}_{\omega^{\beta}}^{aa}(S)$. Since $\omega^{\beta} \models \varphi$, we get by Theorem 28 that $\omega^{\beta+1} \models \varphi^*(S, S)$, and hence $\omega^{\beta+1} \models \psi$.

Conversely, let us assume that $\omega^{\beta+1} \models \psi$. This means that there exists $S$ of order type $\omega$ and cofinal that satisfies $\text{Split}_{\omega^{\beta}}^{aa}(S)$. Let $S = \{s_0 < s_1 < \dots\}$. By Theorem 27, this means that $[s_i, s_{i+1})$ has order type $\omega^{\beta}$ for almost all $i$. Furthermore, $\omega^{\beta+1} \models \varphi^*(S, S)$. Hence, by Theorem 28, this means that $\omega^{\beta+1}|_{[s_i, s_{i+1})} \models \varphi$ for almost all $i \in \omega$. This means that it holds for at least one $i < \omega$ such that $\omega^{\beta+1}|_{[s_i, s_{i+1})} = \omega^{\beta}$. Hence, $\omega^{\beta} \models \varphi$. ◀
# 6 Countable ordinals

By combining Theorems 24 and 25 from the previous sections, we have proved that the MSO[otp<sub>α</sub>]-theory of α is undecidable for all countable ordinals α of the form ω<sup>β</sup>. The next step is to show it for all countable α ≥ ω<sup>ω</sup>:

► **Lemma 30.** For all countable ordinals α ≥ ω<sup>ω</sup>, the MSO[otp<sub>α</sub>]-theory of α is undecidable.

This part of the proof does not involve new interesting arguments. It is presented below for the completeness.

Recall some elementary facts about ordinal arithmetic. Cantor proved that every ordinal α can be uniquely expressed as a finite sum

$$α = ω^{β_n} + \dots + ω^{β_1} + ω^{β_0},$$

for ordinals β<sub>n</sub> ≥ ⋯ ≥ β<sub>1</sub> ≥ β<sub>0</sub>. This is called the *Cantor normal form* of α.

► **Notations.** In order to avoid multi level subscripts, we will sometimes write MSO[α] instead of MSO[otp<sub>α</sub>].

► **Lemma 31.** Let α = ω<sup>β<sub>n</sub></sup> + ⋯ + ω<sup>β<sub>1</sub></sup> + ω<sup>β<sub>0</sub></sup> where β<sub>n</sub> ≥ ⋯ ≥ β<sub>1</sub> ≥ β<sub>0</sub>. If the MSO[α]-theory of α is decidable, the MSO[ω<sup>β<sub>n</sub></sup>]-theory of ω<sup>β<sub>n</sub></sup> is also decidable.

**Proof.** First note that there is an MSO[α] formula ψ<sub>=ω<sup>β<sub>n</sub></sup></sub>(x) such that α |= ψ<sub>=ω<sup>β<sub>n</sub></sup></sub>(b) if and only if b = ω<sup>β<sub>n</sub></sup>. Indeed, this formula says that x is the minimal element such that the set {y : y ≥ x} does not have the order type α.

Now, for every MSO[ω<sup>β<sub>n</sub></sup>] sentence ϕ, we can construct an MSO[α] sentence ϕ* such that ω<sup>β<sub>n</sub></sup> |= ϕ if and only if α |= ϕ*. Indeed, it is sufficient to relativize the quantifiers to β<sub>n</sub>, and this is possible according to the above remark, and replace every occurrence of the predicate otp<sub>ω<sup>β<sub>n</sub></sup></sub>(X) by otp<sub>α</sub>(X ∪ {z | z > ω<sup>β<sub>n</sub></sup>}).

We are now ready to complete the proof of our theorem in the countable case.

**Proof of Theorem 30.** Let α ≥ ω<sup>ω</sup> be a countable ordinal. Its Cantor normal form β<sub>n</sub> ≥ ⋯ ≥ β<sub>1</sub> ≥ β<sub>0</sub> is such that β<sub>n</sub> is countable infinite. Hence, by Theorems 24 and 25, the MSO[otp<sub>ω<sup>β<sub>n</sub></sup></sub>]-theory of ω<sup>β<sub>n</sub></sup> is undecidable. By Theorem 31, this implies that the MSO[otp<sub>α</sub>]-theory of α is undecidable.

To sum up we have the following corollary:

► **Corollary 32.** Let α be a countable ordinal. TFAE

1. α ≥ ω<sup>ω</sup>.

2. α is not MSO definable.

3. The MSO[α] theory of α is undecidable.

4. The MSO[α] theory of any class of ordinals that contains an ordinal ≥ α is undecidable.

**Proof.** We have already proved the equivalence between (1)-(3). The implication (4) ⇒ (3) is immediate.

Let us proof that (3) ⇒ (4). First note that there is an MSO[α] formula Ψ<sub>α</sub>(x) which defines α inside every β > α, i.e., for every β > α there is a unique b such that β |= Ψ<sub>α</sub>(b) and the substructure of β over the prefix {a | a < b} is isomorphic to α. Now, using this formula, for every MSO[α] sentence Φ it is easy to construct an MSO[α] sentence Φ<sup>α</sup> such that α |= Φ if and only if β |= Φ<sup>α</sup> for every (equivalently some) β > α.
7 Conclusion

This paper belongs to the body of works that aims at extending the expressive power of
monadic second-order logic, while retaining decidability results. More precisely, we have
studied the question of decidability of monadic second-order logic of ordinals when extended
with predicates about the order type of sets. Since the order type of some ordinals is non
definable (in particular for all countable ordinals from ω upward), such extensions of MSO
are strictly more expressive than MSO. Our main result for ordinals, Theorem 2, shows
that up to ordinal ω₁, there is nothing to be gained: if extending MSO with an order type
predicate is decidable, then this order type was already definable in plain MSO, and thus the
obtained logic is expressively equivalent to MSO.

The proof techniques involve a reduction of non-decidability of the satisfiability BMSO,
which itself relies on the deep result of undecidability of the satisfiability of MSO+U over ω.
This has to be combined with extra involved arguments for catching all the ordinals < ω₁.
However, when reaching ω₁ all these tools seems to become useless, and the main open
question we are left with is the following:

► **Problem 33.** Is it true that $\alpha$ is MSO-definable if and only if the MSO[$otp_\alpha$]-theory of $\alpha$ is decidable for all $\alpha < \omega_2$?

Another problem is:

► **Problem 34.** What is the degree of undecidability of the MSO[$otp_\alpha$]-theory of $\alpha$?

We provided a reduction from the satisfiability of BMSO to the satisfiability problem of
MSO[$otp_\alpha$]. The satisfiability problem for BMSO is not in RE and not in Co-RE. We do not
know whether there is a reduction in the other direction. Similar problems are about the
degree of undecidability of the MSO[$CBrank_\alpha$]-theory of the full binary tree.

The Hausdorff rank (sometimes called *VD-rank* or *F-rank*) is naturally definable for linear orders [28]. In particular, a linear order (*L*, <) has a Hausdorff rank if and only if it is scattered, equivalently if and only if there is no order preserving embedding of the rationals in (*L*, <). Given an ordinal $\alpha$, let *Hrank*<sub>α</sub>(*X*) express that *X* has Hausdorff rank $\alpha$. We denote by *MSO*[*Hrank*<sub>α</sub>] the monadic second-order logic of order extended with the new predicate *Hrank*<sub>α</sub>(-).

It is well known that "a linear order has Hausdorff rank *n*" is definable for every *n* ∈ N.

► **Theorem 35.** For every countable ordinals $\alpha \ge \omega$, the MSO[$Hrank_\alpha$]-theory of the class of countable linear orders is undecidable.

The proof is a reduction of Theorem 35 to Theorem 2, and it is based on the following
observations:

1. An ordinal $\gamma$ has Hausdorff rank $\le \alpha$ if and only if $\gamma \le \omega^\alpha$.

2. Hence, for an infinite ordinal $\gamma$: $OTP(\gamma) = \omega^\alpha$ can be expressed as $Hrank(\gamma) = \alpha$ and $Hrank(\{y \mid y \ge x\}) = \alpha$ for every $x < \gamma$.

Therefore, there is an MSO[$Hrank_\alpha$] formula $\varphi_\alpha(X)$ that expresses "*X* is a well-order and the order type of *X* is $\omega^\alpha$." Hence, by Theorem 2, we obtain that the MSO[$Hrank_\alpha$]-theory of the linear orders of Hausdorff rank $\alpha$ as well as the MSO[$Hrank_\alpha$]-theory of the class of countable linear orders is undecidable.

We can prove a stronger result:

**► Theorem 36.** For every countable ordinals $\beta \ge \alpha \ge \omega$, and every countable linear order $(L, <)$ of Hausdorff rank $\beta$, the MSO[$Hrank_\alpha$]-theory of $(L, <)$ is undecidable.

Our proof of Theorem 36 is direct. The proof techniques are similar to those of Theorem 2,
however, we have not found a reduction of Theorem 36 to Theorem 2.
References

1 Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, and James Worrell. On the decidability of monadic second-order logic with arithmetic predicates. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, *Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024*, Tallinn, Estonia, July 8-11, 2024, pages 11:1–11:14. ACM, 2024. doi:10.1145/3661814.3662119.

2 Achim Blumensath, Olivier Carton, and Thomas Colcombet. Asymptotic monadic second-order logic. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, *Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014*, Budapest, Hungary, August 25-29, 2014. *Proceedings, Part I*, volume 8634 of *Lecture Notes in Computer Science*, pages 87–98. Springer, 2014. doi:10.1007/978-3-662-44522-8_8.

3 Achim Blumensath, Thomas Colcombet, Denis Kuperberg, Pawel Parys, and Michael Vanden Boom. Two-way cost automata and cost logics over infinite trees. In Thomas A. Henzinger and Dale Miller, editors, *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 16:1–16:9. ACM, 2014. doi:10.1145/2603088.2603104.

4 Mikolaj Bojanczyk. A bounding quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, *Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL*, Karpacz, Poland, September 20-24, 2004, *Proceedings*, volume 3210 of *Lecture Notes in Computer Science*, pages 41–55. Springer, 2004. doi:10.1007/978-3-540-30124-0_7.

5 Mikolaj Bojanczyk and Thomas Colcombet. Boundedness in languages of infinite words. *Log. Methods Comput. Sci.*, 13(4), 2017. doi:10.23638/LMCS-13(4:3)2017.

6 Mikolaj Bojanczyk, Laure Daviaud, Bruno Guillon, Vincent Penelle, and A. V. Sreejith. Undecidability of a weak version of MSO+U. *Log. Methods Comput. Sci.*, 16(1), 2020. doi:10.23638/LMCS-16(1:12)2020.

7 Mikolaj Bojanczyk, Edon Kelmendi, Rafal Stefanski, and Georg Zetzsche. Extensions of $\omega$-regular languages. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, *LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020*, pages 266–272. ACM, 2020. doi:10.1145/3373718.3394779.

8 Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U theory of (n, <) is undecidable. In Nicolas Ollinger and Heribert Vollmer, editors, *33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France*, volume 47 of *LIPIcs*, pages 21:1–21:8. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPICs.STACS.2016.21.

9 Mikolaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In Christoph Dürr and Thomas Wilke, editors, *29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France*, volume 14 of *LIPIcs*, pages 648–660. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPICs.STACS.2012.648.

10 J. R. Büchi. On a decision method in the restricted second-order arithmetic. In *Proc. Int. Congress Logic, Methodology and Philosophy of science, Berkeley 1960*, pages 1–11. Stanford University Press, 1962.

11 J. R. Büchi. Transfinite automata recursions and weak second order theory of ordinals. In *Proc. Int. Congress Logic, Methodology, and Philosophy of Science, Jerusalem 1964*, pages 2–23. HOLLAND, 1965.

12 J Richard Büchi and Dirk Siefkes. *Decidable Theories: Vol. 2: The Monadic Second Order Theory of All Countable Ordinals*, volume 328. Springer, 2006.

13 J.Richard Büchi and Charles Zaiontz. Deterministic automata and the monadic theory of ordinals $\omega_2$. *Z. Math. Logik Grundlagen Math.*, 29:313–336, 1983.

14 O. Carton and W. Thomas. The monadic theory of morphic infinite words and generalizations. *Inform. Comput.*, 176:51–76, 2002.
11:18 On the Expansion of MSO with Cantor-Bendixson Rank and Order Type Predicates

15 Thomas Colcombet. Regular cost functions, part I: logic and algebra over words. *Log. Methods Comput. Sci.*, 9(3), 2013. doi:10.2168/LMCS-9(3:3)2013.

16 Thomas Colcombet and Christof Löding. Regular cost functions over finite trees. In *Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom*, pages 70–79. IEEE Computer Society, 2010. doi: 10.1109/LICS.2010.36.

17 Calvin C. Elgot and Michael O. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. *J. Symb. Log.*, 31(2):169–181, 1966. doi:10.2307/2269808.

18 S. Fratani. The theory of successor extended with several predicates. *preprint*, 2009.

19 Y. Gurevich. Monadic second-order theories. In J. Barwise and S. Feferman, editors, *Model-Theoretic Logics*, pages 479–506. Springer-Verlag, Perspectives in Mathematical Logic, 1985.

20 Yuri Gurevich. Modest theory of short chains. i. *J. Symb. Log.*, 44(4):481–490, 1979. doi: 10.2307/2273287.

21 Yuri Gurevich, Menachem Magidor, and Saharon Shelah. The monadic theory of $\omega_2$. *J. Symb. Log.*, 48(2):387–398, 1983.

22 Yuri Gurevich and Saharon Shelah. Modest theory of short chains. ii. *J. Symb. Log.*, 44(4):491–502, 1979. doi:10.2307/2273288.

23 Yuri Gurevich and Saharon Shelah. Interpreting second-order logic in the monadic theory of order. *J. Symb. Log.*, 48(3):816–828, 1983. doi:10.2307/2273475.

24 M.O. Rabin. Decidability of second-order theories and automata on infinite trees. *Transactions of the American Mathematical Society*, 141:1–35, 1969.

25 A. Rabinovich. On decidability of monadic logic of order over the naturals extended by monadic predicates. *Inf. Comput.*, 205(6):870–889, 2007. doi:10.1016/J.IC.2006.12.004.

26 A. Rabinovich and W. Thomas. Decidable theories of the ordering of natural numbers with unary predicates. In Zoltán Ésik, editor, *Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings*, volume 4207 of *Lecture Notes in Computer Science*, pages 562–574. Springer, 2006. doi:10.1007/11874683_37.

27 R.M. Robinson. Restricted set-theoretical definitions in arithmetic. *Proc. Am. Math. Soc.*, 9:238–242, 1958.

28 J.G. Rosenberg. *Linear Orderings*. ISSN. Elsevier Science, 1982. URL: https://books.google.com.sg/books?id=y3YpdW-sbFsC.

29 A. L. Semenov. Decidability of monadic theories. In M. P. Chytil and V. Koubek, editors, *Proceedings of the 11th Symposium on Mathematical Foundations of Computer Science*, volume 176 of LNCS, pages 162–175, Praha, Czechoslovakia, September 1984. Springer. doi:10.1007/BFB0030296.

30 A. L. Semenov. Logical theories of one-place functions on the set of natural numbers. *Mathematics of the USSR - Izvestia*, 22:587–618, 1984.

31 S. Shelah. The monadic theory of order. *Annals of Mathematics*, 102:379–419, 1975.

32 Saharon Shelah. The monadic theory of order. *The Annals of Mathematics*, 102(3):379, November 1975. doi:10.2307/1971037.

33 D. Siefkes. Decidable extensions of monadic second order successor arithmetic. *Automatentheorie und Formale Sprachen, (Tagung, Math. Forschungsinst, Oberwolfach)*, 1969; (Bibliograph. Inst., Mannheim), pages 441–472, 1970.

34 W. Thomas. A note on undecidable extensions of monadic second order successor arithmetic. *Arch. Math. Logik Grundlagenforsch.*, 17:43–44, 1975. doi:10.1007/BF02280812.

**A Proof of Lemma 17**

Note that $T_0 + T_1$ is a binary tree only if $T_0$ has at most one child. Since we are dealing with binary trees where every child is either left or right (these trees are considered as structures for the signature $\{<, \text{Left}(\cdot), \text{Right}(\cdot)\}$) we have further refine sum and $\omega$-sum operations.
First we characterize when a tree $T$ of rank $\alpha$ is isomorphic to the downward closure of an antichain $X$ of the full binary tree such that $(X, <_{lex})$ is (isomorphic to) an ordinal. Then we state properties of these trees and finally, we prove Theorem 17.

**► Definition 37 (BWT trees).** Let BWT be the set of binary trees such that $T \in BWT$ if the children of $T$ are partitioned into the left and right children and every node has a leaf as a descendant, and the lexicographic order on the leaves is a well-order.

**► Lemma 38.** Let $X$ be an antichain in the full binary tree such that $(X, <_{lex})$ is isomorphic to an ordinal. Then $T := (X \downarrow, <)$ is in BWT.

**► Lemma 39.** Let $\pi = u_1u_1\cdots \in \{L, R\}^\omega$ be an $\omega$-branch of $T \in BWT$. Let $T_i$ (for $i \in \omega$) be the subtree of $T$ over $X_i := \{v \mid v \ge u_1\dots u_i \text{ and } \neg(v \ge u_1\dots u_{i+1})\}$. Then

1. $T_i \in BWT$.

2. Infinitely many $T_i$ have more than one element.

3. There is $i_R$ such that for every $i \ge i_R$: if $T_i$ has more than one element, then $u_{i+1} = R$.

**Proof.**

(1) $T_i \in BWT$. Indeed (a) every node in $X_i$ has a leaf descendant in $X_i$, (b) the leaves are well-ordered by $<_{lex}$ and (c) children are partitioned into left/right as in $T$.

(2) If $T_i$ is singleton for all $i > j$, then for all $i > j$ the $i$-th node on $\pi$ has no leaf as descendant. Contradiction.

(3) Let $F := \{v \mid vL \in \pi \text{ and there is a leaf above } vR\}$. We claim that $F$ is finite. Indeed if $i \in F$ and $u_i$ is a leaf above $vR$ then $vL <_{lex} u_i$ and every descendant $u$ of $vL$ is $<_{lex} u_i$. In particular, $u_{i+1} <_{lex} u_i$ for all $i \in F$. Hence, if $F$ is infinite, then $<_{lex}$ is not well-order on the leaves. Contradiction. ◀

The $+$ and $\omega$-sum operations on trees are refined by sums and infinite sums of BWT trees.

**► Definition 40 (Sums of BWT trees).** Let $T_i = (|T_i|, <_i)$ for $i \in \{0, 1\}$ be BWT trees over disjoint universes. If the root of $T_0$ does not have right (respectively left) child define $T_0 +_R T_1$ (respectively, $T_0 +_L T_1$) to be a tree with universe $|T_0| \cup |T_1|$ and its order relation defined as $n_1 \le n_2$ if there is $i \in \{0, 1\}$ such that $n_1, n_2 \in |T_i|$ and $n_1 \le_i n_2$, or $n_1$ is the root of $T_0$; the root of $T_1$ becomes right (respectively, left) child of the root of $T_0$, and for other nodes their left/right status is inherited from $T_0$ and $T_1$.

The infinite sums of BWT trees is defined as follows.

**► Definition 41 (Infinite sums of BWT trees).** Let $T_i = (|T_i|, <_i)$ for $i \in \omega$ be BWT trees over disjoint universes, and let $u_1u_2\cdots \in \{L, R\}^\omega$ be an $\omega$-string. $\sum_{i \in \omega}^u T_i$ is defined if
1. The root of $T_i$ does not have $u_{i+1}$ child ($i \in \omega$).

2. Infinitely many of $T_i$ have more than one element.

3. There is $i_R$ such that for $i \ge i_R$: if $T_i$ has more than one element, then $u_{i+1} = R$. We define the tree

$$ \sum_{i \in \omega}^{u} T_i $$

as having universe $\bigcup_{i \in \omega} |T_i|$ and its order relation is defined as $n_1 \le n_2$ if there is $i$ such that $n_1, n_2 \in |T_i|$ and $n_1 \le_i n_2$, or $n_1$ is the root of $T_i$ and $n_2 \in |T_j|$ for $j \ge i$.

The root of $T_{i+1}$ becomes the right (respectively, left) child of the root of $T_i$ if $u_{i+1} = R$ (respectively, $u_{i+1} = L$), and for other nodes of $T_i$ their left/right status is inherited from $T_i$.
Note the requirement that infinitely many of $T_i$ have more than one element ensures that every node in the $\omega$-sum has a leaf as a descendant. The third requirement ensures that the lexicographic order on the leaves of $\sum_{i \in \omega} T_i$ is well-order.

If the disjointness assumption does not hold in the above definitions, we replace $T_i$ by disjoint isomorphic copies and proceed as above.

**► Lemma 42.**

1. If $T_i$ are in BWT and $T_0 +_R T_1$ is defined, then $T_0 +_R T_1$ is in BWT.

2. If $T_i$ are in BWT and $T_0 +_L T_1$ is defined, then $T_0 +_L T_1$ is in BWT.

3. If $T_i$ are in BWT and $\sum_{i \in \omega} T_i$ is defined, then $\sum_{i \in \omega} T_i$ is in BWT.

For $T \in \text{BWT}$, we denote by $\text{OTP}(T)$ the order type of the lexicographic order on the leaves of $T$.

**► Lemma 43.**

1. $\text{OTP}(T_0 +_R T_1) = \text{OTP}(T_0) + \text{OTP}(T_1)$.

2. $\text{OTP}(T_0 +_L T_1) = \text{OTP}(T_1) + \text{OTP}(T_0)$.

3. Assume that if $T_i$ have more than one element, then $u_{i+1} = R$. Then $\text{OTP}(\sum_{i \in \omega} T_i) = \sum_{i \in \omega} \text{OTP}(T_i)$.

Define $\text{BWT}_\alpha := \text{CBrank}_\alpha \cap \text{BWT}$ and $\text{BWT}_\alpha^+ := \text{CBrank}_\alpha^+ \cap \text{BWT}$, where $\alpha$ is a countable ordinal. Note that $\text{BWT}_0$ are one element trees and $\text{BWT}_0^+$ are finite binary trees with a partition of children into left and right.

**► Lemma 44.** For $\alpha > 0$.

1. $T \in \text{BWT}_\alpha$ if and only if $T = \sum_{i \in \omega} T_i$ for $T_i \in \cup_{\beta < \alpha} \text{BWT}_\beta^+$.

2. $T \in \text{BWT}_\alpha^+$ if and only if there are $T'_0, \dots, T'_k \in \cup_{\beta \le \alpha} \text{BWT}_\beta$ and $v_1 \dots v_k \in \{L, R.\}$ such that $T = (((T'_0 + v_1 T'_1) + v_2 T'_2) \dots + v_k T'_k)$.

3. Assume that $\text{CBrank}(T) = \alpha$ and $T \in \text{BWT}_\alpha$. Let $u$ and $T_i$ be as in 1. Then

a. If $\alpha$ is limit, then for every $\beta < \alpha$ there is $T_i \notin \text{BWT}_\beta^+$.

b. If $\alpha = \gamma + 1$, then infinitely often $T_i \in \text{BWT}_\gamma^+ \setminus \cup_{\beta < \gamma} \text{BWT}_\beta^+$.

**Proof.** (1) $\Leftarrow$ direction is easily followed by the induction on $\alpha$.

$\Rightarrow$-direction. $T \in \text{CBrank}_\alpha$, therefore there is an $\omega$-branch $\pi = u_1 u_2 \dots \in \{L, R\}^\omega$ such that $T = \sum_{i \in \omega} T_i$, where $T_i \in \cup_{\beta < \alpha} \text{CBrank}_\beta^+$ is the subtree of $T$ over $X_i := \{v \mid v \ge u_1 \dots u_{i-1}$ and $\neg(v \ge u_1 \dots u_i)\}$. Since $T \in \text{BWT}$, it follows that $T_i \in \text{BWT}$ and therefore, $T_i \in \cup_{\beta < \alpha} \text{BWT}_\beta^+$. It is also clear that $T = \sum_{i \in \omega} T_i$.

(2) and (3) easily follows from the definitions.

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

**Proof Theorem 17.** Let $X$ be an antichain in the full binary tree such that $(X, <_{\text{lex}})$ is isomorphic to an ordinal. We have to prove that $T := (X \downarrow, <)$ has Cantor-Bendixson rank $\alpha$ if and only if the order type of $(X, <_{\text{lex}})$ belongs to $[\omega^\alpha, \omega^{\alpha+1})$.

Note that $T$ is a BWT by Theorem 38. The proof proceeds by induction on $\alpha$ using Theorem 43 and Theorem 44.

The base case $\alpha = 0$ is immediate.

Assume that Lemma holds for all $\beta < \alpha$.

Let $T \in \text{BWT}_\alpha$. By Theorem 44, $T = \sum_{i \in \omega} T_i$ for $T_i \in \cup_{\beta < \alpha} \text{BWT}_\beta^+$. By the inductive hypothesis $\text{OTP}(T_i) < \omega^\alpha$.

Let $u^k := u_{k+1} u_{k+2} \dots$. Then $u := u_1 \dots u_k u^k$. By Theorem 39(3), we can choose $k$ such that if $T_{k+i}$ have more than one element, then $u_{k+i+1} = R$. Hence, by Theorem 43(3), $\text{OTP}(\sum_{i \in \omega} T_{k+i}) = \sum_{i \in \omega} \text{OTP}(T_{i+k}) < \omega^\alpha \times \omega$. $T := (T_0 + u_1 + (T_1 + u_2 + u_3 + \dots + u_k T')))$, where $T' := \sum_{i \in \omega} T_{k+i}$. We proved that $\text{OTP}(T_i) < \omega^\alpha$ and $\text{OTP}(T') < \omega^\alpha \times \omega = \omega^{\alpha+1}$. Hence, by Theorem 43(1)-(2), $\text{OTP}(T) < \omega^{\alpha+1}$.
Let us show that $OTP(T) \ge \omega^\alpha$.

By Theorem 44(3), if $\alpha$ is limit then there is no $\beta < \alpha$ such that all $T_i \in BWT_\beta^+$ for $i > k$. Therefore, there is no $\beta < \alpha$ such that $OTP(T_i) < \omega^\beta$ for $i > k$. Hence $OTP(\sum_{i \in \omega}^u T_{k+i}) \ge \omega^\alpha$.

By Theorem 44(3), if $\alpha = \gamma + 1$ is a successor, then infinitely often $T_i \in BWT_\gamma^+ \setminus \cup_{\beta < \gamma} BWT_\beta^+$. Hence, by the inductive hypothesis, infinitely often $OTP(T_i) \ge \omega^\gamma$. Hence, $OTP(\sum_{i \in \omega}^u T_{k+i}) \ge \omega^\gamma \times \omega = \omega^\alpha$. Therefore, $OTP(T) \ge \omega^\alpha$. This completes the proof for the case when $T \in BWT_\alpha$.

Now assume that $T \in BWT_\alpha^+$ and $CBrank(T) = \alpha$. Then $T$ is a sum of trees in $BWT_\alpha$ where at least one of the summands has $CBrank$ equal to $\alpha$. Therefore, the $OTP$ of this summand is at least $\omega^\alpha$, and hence, the $OTP$ of the sum is at least $\omega^\alpha$. $\blacksquare$

## B Beyond countable ordinals

In this section, we consider the decidability questions concerning $MSO[otp_\alpha]$ for $\alpha$ smaller than $\omega_1^1$. It essentially relies, as for the countable case, on the techniques in Sections 4–6, but it requires a bit more care. Also, some of the arguments go beyond $\omega_1^1$, but not all.

Thus, our first task is to understand precisely what are the $MSO$-definable ordinals beyond the countable. Let $\omega_1$ be the first uncountable ordinal and $\omega_2$ be the initial ordinal of the cardinal $N_2$.

Let us first note that $\omega_1$ is $MSO$-definable, indeed, this is the least limit ordinal which is not of cofinality $\omega$. It is easy to express in an $MSO$ that an ordinal is limit and that an ordinal has a cofinal $\omega$-sequence. In the same way, $\omega_2$ is $MSO$-definable since it is the least ordinal which is not of cofinality $\omega_1$ or $\omega$.

In Section B.1 we characterize $MSO$-definable ordinals in $[\omega_1, \omega_2)$. In Section B.2 we consider ordinals of the form $\omega_1^\beta$ where $\beta$ is countable. We prove that for these ordinals $MSO[otp_{\omega_1^\beta}]$ is decidable if and only if $\omega_1^\beta$ is $MSO$ definable. In Section B.3 we extend the equivalence between decidability and definability to all ordinals $< \omega_1^1$. The ordinal $\omega_1^{\omega_1}$ is undefinable, unfortunately we do not know whether $MSO[otp_{\omega_1^{\omega_1}}]$ is decidable.

### B.1 Definable ordinals < $\omega_2$

In this subsection we characterize the $MSO$-definable ordinals $< \omega_2$. We use the following variant of the Cantor normal form: If $\alpha \in (0, \omega_2)$, then $\alpha$ has a unique decomposition of the form

$$ \alpha = \omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_0} \times \gamma_0, $$

where $\omega_2 > \beta_n > \dots > \beta_1 > \beta_0 \ge 0$ and $\gamma_i$ is a non-zero countable ordinal for all $i$. Let us call it the $\omega_1$-representation of $\alpha$.

**Proposition 45 (MSO-definable ordinals).** An ordinal $\alpha < \omega_2$ is $MSO$-definable if and only if its $\omega_1$-representation $\omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_0} \times \gamma_0$ is such that $\beta_i < \omega$ and $\gamma_i < \omega^\omega$ for all $i$.

**Proof.** $\Leftarrow$ direction.

Let us recall that $MSO$-definable ordinals are closed under sum and multiplication. Therefore, every finite power of $\omega_1$ is $MSO$-definable, and since every $\gamma < \omega^\omega$ is $MSO$-definable, we obtain that all the ordinals that have an $\omega_1$-representation as in the statement, are $MSO$-definable.

Our proof of the other direction use elements of the compositional methods [32].
For every $n \in \mathbb{N}$ we say that ordinals $\alpha$ and $\beta$ are $\equiv_n$-equivalent (notation $\alpha \equiv_n \beta$) if for every MSO sentence $\Phi$ of the quantifier depth at most $n$: $\alpha \models \Phi$ if and only if $\beta \models \Phi$. We will use the following well-known facts:

**Fact 46 (≡<sub>n</sub> is a congruence).** The relation $\equiv_n$ is an equivalence relation and it is a congruence with respect to $+$ and $\times$. If $\alpha \equiv_n \beta$ then for every $\gamma$:

1. $\alpha + \gamma \equiv_n \beta + \gamma$ and $\gamma + \alpha \equiv_n \gamma + \beta$.

2. $\alpha \times \gamma \equiv_n \beta \times \gamma$

**Fact 47.** There is a function $M: \mathbb{N} \to \mathbb{N}$ such that for every $n$ if $\alpha \equiv_{M(n)} \beta$ then $\gamma \times \alpha \equiv_n \gamma \times \beta$.

**Fact 48 (cf Theorem 3.5(B) [31]).**

1. For every $\delta < \omega_2$ there is $\delta(k) < \omega_1^\omega$ such that $\delta \equiv_k \delta(k)$.

2. For every $\delta < \omega_1$ there is $\delta(k) < \omega_1^\omega$ such that $\delta \equiv_k \delta(k)$.

Now we are ready to prove the $\Rightarrow$ direction of Theorem 45.

Assume that the $\omega_1$-representation of $\alpha$ is

$$\alpha = \omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_i} \times \gamma_i + \dots + \omega_1^{\beta_0} \times \gamma_0,$$

If $\beta_i \ge \omega$ for some $i$, then $\alpha \ge \omega_1^\omega$. Therefore, if $\alpha$ satisfies a sentence $\Phi$ of quantifier depth $k$, by Fact 48(1), there is $\alpha(k) < \omega_1^\omega$ that satisfies $\Phi$. Hence, $\alpha$ is not MSO definable.

Hence, if $\alpha$ is MSO definable then all $\beta_i < \omega$. Now assume that $\gamma_i > \omega^\omega$ for some $i$. Toward a contradiction, let $\alpha$ be definable by a sentence $\Phi$ of quantifier depth $k$. By Fact 48(2) there is $\gamma'_i < \omega^\omega$ such that $\gamma \equiv_{M(k)} \gamma'_i$, where $M$ is a function from Fact 47. Therefore, by Fact 47, $\omega_1^{\beta_i} \times \gamma_i \equiv_k \omega_1^{\beta_i} \times \gamma'_i$. Hence, by Fact 46, $\alpha$ is $\equiv_k$-equivalent to $\alpha'$ which has the following $\omega_1$-representation:

$$\alpha' = \omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_i} \times \gamma_i' + \dots + \omega_1^{\beta_0} \times \gamma_0$$

Therefore, $\alpha' \models \Phi$. But $\alpha' \neq \alpha$ (by uniqueness of $\omega_1$ representation) and this contradicts that $\alpha$ is definable by $\Phi$. $\quad \blacksquare$

## B.2 $\omega_1^\beta$ for countable $\beta$

In this subsection we consider ordinals of the form $\omega_1^\beta$ where $\beta$ is countable. We prove that for these ordinals MSO[$otp_{\omega_1^\beta}$] is decidable if and only if $\omega_1^\beta$ is MSO definable.

Theorem 24 states that if $\beta$ is of cofinality $\omega$, the MSO[$otp_{\omega^\beta}$]-theory of $\omega^\beta$ is undecidable.

Note that $\omega_1 = \omega^{\omega_1}$ and $\omega_1^\beta = \omega^{\omega_1 \times \beta}$. Observe that if $\beta$ is $\omega$-cofinal then $\omega_1 \times \beta$ is $\omega$-cofinal. Hence,

**Corollary 49.** If $\beta$ is $\omega$-cofinal, then the MSO[$otp_{\omega_1^\beta}$]-theory of $\omega_1^\beta$ is undecidable.

Now we are going to show how to reduce MSO[$\omega_1^\beta$] to MSO[$\omega_1^{\beta+1}$]. From this reduction and Theorem 49 we deduce undecidability of MSO[$\omega_1^\beta$] for all $\beta \in [\omega, \omega_1)$.

The following standard facts hold:

**Fact 50.**

1. Let $(\alpha_i)_{i \in \omega}$ be an $\omega$-sequence such that $\alpha_i < \omega^\beta$ for all $i$. Then,

$$\sum_{i \in \omega} \alpha_i \le \omega^\beta.$$
2. Let $(\alpha_i)_{i \in \omega}$ be an $\omega$-sequences of ordinals smaller than $\omega^{\beta+1}$.

$$ \sum_{i \in \omega} \alpha_i = \omega^{\beta+1} \text{ if and only if } \alpha_j \ge \omega^\beta \text{ for cofinally many } j. $$

3. Let $(\alpha_i)_{i \in \omega_1}$ be an $\omega_1$-sequences of ordinals smaller than $\omega_1^{\beta+1}$.

$$ \sum_{i \in \omega_1} \alpha_i = \omega_1^{\beta+1} \text{ if and only if } \alpha_j \ge \omega_1^\beta \text{ for cofinally many } j. $$

4. Let $(\alpha_i)_{i \in \omega_1}$ be an $\omega_1$-sequence such that $\alpha_i < \omega_1^\beta$ for all $i$. Then,

$$ \sum_{i \in \omega_1} \alpha_i \le \omega_1^\beta. $$

Theorem 50(1)-(2) was used in the reduction of $\text{MSO}[\omega^\beta]$ to $\text{MSO}[\omega^{\beta+1}]$. We will use Theorem 50(3)-(4) in our reduction of $\text{MSO}[\omega_1^\beta]$ to $\text{MSO}[\omega_1^{\beta+1}]$.

Note that for $\beta \ge \omega$, it is impossible to express in $\text{MSO}[\omega_1^{\beta+1}]$ “an interval is of length $\omega_1^\beta$.” Even there is no $\text{MSO}[\omega_1^{\beta+1}]$ formula $B(x)$ such that $\omega_1^{\beta+1} \models B(b)$ if and only if the interval $[0, b) := \{c \mid c < b\}$ has the order type $\omega^\beta$.

Our first aim is to chop $\omega_1^{\beta+1}$ into $\omega_1$ disjoint intervals all of length $\omega_1^\beta$, except a countable many.

**Lemma 51.** There is an $\text{MSO}[\omega_1^{\beta+1}]$ formula $\text{Chop}(X_B, X_E)$ such that for every $B, E \subseteq \omega_1^{\beta+1}$ we have $\omega_1^{\beta+1} \models \text{Chop}(B, E)$ if and only if

1. $B$ and $E$ have order type $\omega_1$ and $b_i < e_i < b_{i+1}$ for $i \in \omega_1$. Hence, for $i \ne j$ the intervals $(b_i, e_i)$ and $(b_j, e_j)$ are disjoint.

2. For all but countable many $i$, the order type of $[b_i, e_i)$ is $\omega_1^\beta$.

**Proof.** Let $B := (b_i)_{i \in \omega_1}$ and $E := (e_i)_{i \in \omega_1}$ be increasing $\omega_1$ sequences such that $b_i < e_i < b_{i+1}$ for all $i \in \omega_1$. (This can be formalized in $\text{MSO}$.) We want to ensure that $\text{OTP}([b_i, e_i)) = \omega_1^\beta$ for all $i \in \omega_1$, except countable many one.

Let us formalize it as follows:

**Requirements.**

(1) $\bigcup_{i \in I} [b_i, e_i)$ has order type $\omega_1^{\beta+1}$ for every cofinal subset $I$ of $\omega_1$, and

(2) for all $C := (c_i)_{i \in \omega_1}$ such that $c_i \in [b_i, e_i)$ the order type of $\bigcup [b_i, c_i)$ is not $\omega_1^{\beta+1}$ (it should be $< \omega_1^{\beta+1}$).

It is easy to formalize (1) and (2) by an $\text{MSO}[\omega_1^{\beta+1}]$ formula.

We claim that (1) and (2) hold if and only if for all, but countable many $i$: $\text{OTP}([b_i, e_i)) = \omega_1^\beta$.

Indeed, if for all $i$: $\text{OTP}([b_i, e_i)) = \omega_1^\beta$, then, by Theorem 50(4), for all $C := (c_i)_{i \in \omega_1}$ such that $c_i \in [b_i, e_i)$ we have $\text{OTP}((\bigcup [b_i, c_i)) \le \omega_1^\beta$. Therefore, if for all but countable many $i$: $\text{OTP}([b_i, e_i)) = \omega_1^\beta$, then $\text{OTP}((\bigcup [b_i, c_i)) < \omega_1^{\beta+1}$. Therefore, (1) and (2) hold.

For the other direction. If (1) holds, then by Theorem 50(4) there are at most countable many $i$ such that $\text{OTP}([b_i, e_i)) < \omega_1^\beta$. If (2) holds, then, by Theorem 50(3), there are at most countable many $i$ such that $\text{OTP}([b_i, e_i)) > \omega_1^\beta$. Hence, there are at most countable many $i$ such that $\text{OTP}([b_i, e_1)) \ne \omega_1^\beta$. We proved the Lemma $\blacksquare$

Now we will reduce $\text{MSO}[\omega_1^\beta]$ to $\text{MSO}[\omega_1^{\beta+1}]$. This is exactly like the reduction of Theorem 28, but for negation we should replace<fnref n="2" /> “infinite” by $\omega_1$.

<footnote n="2">² Instead of the filter of co-finite subset of $\omega$, we use the filter of co-countable subsets of $\omega_1$.</footnote>
**Lemma 52.** There is an algorithm which given an MSO[$\omega_1^\beta$]-formula $\varphi(X_1, \dots, X_k)$ constructs an MSO[$\omega_1^{\beta+1}$]-formula $\varphi^*(X_B, X_E, X_1, \dots, X_k)$ such that for all $A_1, \dots, A_k \subseteq \omega_1^{\beta+1}$ and all $B, E$ which satisfy $\omega_1^{\beta+1} \models \text{Chop}(B, E)$:

$$ \omega_1^{\beta+1} \models \varphi^*(B, E, A_1, \dots, A_k) $$

if and only if

$$ \omega_1^{\beta+1}|_{[b_i, e_i)} \models \varphi(A_1 \cap [b_i, e_i), \dots, A_k \cap [b_i, e_i)) $$

for all but countable many $i$.

**Proof.** We shall define the formula $\varphi^*$ by structural induction on $\varphi$, and establish the conclusions of the lemma at the same time. The case of existential quantifier, the case of conjunction, and the case of MSO predicates are elementary. The crucial point is the negation.

**Case of a conjunction, i.e.,** $\varphi(\bar{X}) = (\varphi_1(\bar{X}) \wedge \varphi_2(\bar{X}))$. We define

$$ \varphi^*(X_B, X_E, \bar{X}) := \varphi_1^*(X_B, X_E, \bar{X}) \wedge \varphi_2^*(X_B, X_E, \bar{X}). $$

Correctness follows from the fact that co-countable subsets of $\omega_1$ are closed under the intersection.

**Case of an existential set quantifier, i.e.,** $\varphi(\bar{X}) = \exists Y. \varphi_1(\bar{X}, Y)$. We define

$$ \varphi^*(X_B, X_E, \bar{X}) := \exists Y. \varphi_1^*(X_B, X_E, \bar{X}, Y). $$

Correctness is also straightforward.

Case of an MSO-formula $\varphi(\bar{X})$, and in particular of the atomic formulas $x \in Y$ and $x < y$ is easy and very similar to Theorem 28.

**Case of an order type predicate, i.e.,** $\varphi(\bar{X}) := \text{otp}_{\omega_1^\beta}(X_m)$. For simplicity, we shall treat the case of $\varphi(X) := \neg \text{otp}_{\omega_1^\beta}(X_m)$, and leave the question of removing the negation to the negation case below. We set:

$$ \varphi^*(X_B, X_E, X_m) := \text{Chop}(X_B, X_E) \wedge \neg \text{otp}_{\omega_1^{\beta+1}}(X_m \cap F), $$

where $F := \{z \mid \exists x \in X_B \exists y \in X_E (x \le z < y \wedge (x, y) \cap X_B = \emptyset \wedge (x, y) \cap X_E = \emptyset)\}$. The correctness of this construction relies on Theorem 50.

**Case of a negation, i.e.,** $\varphi(\bar{X}) := \neg \varphi_1(X_1, \dots, X_k)$. We set $\varphi^*(X_B, X_E, \bar{X})$ to be the conjunction of

A $\text{Chop}(X_B, X_E)$, and

B $\neg \varphi_1^*(X'_B, X'_E, \bar{X})$ holds for every $X'_B, X'_E$ which are cofinal subsets of $X_B$ and $X_E$ such that $\text{Chop}(X'_B, X'_E)$.

Let us assume that $\omega^{\beta+1} \models \text{Chop}(B, E)$. Then $B := \{b_i \mid i \in \omega_1\}$ and $E := \{e_i \mid i \in \omega_1\}$, where $b_i$ and $e_i$ are increasing $\omega_1$-sequences.

Condition B is equivalent to $\neg \varphi_1(\bar{A} \cap [b_i, e_i))$ holds for all but countable many $i$.

Hence, the inductive hypothesis holds.

As a consequence of Theorem 49 and Theorem 52 we obtain:

**Corollary 53.** The MSO[$\omega_1^\beta$] is undecidable on $\omega_1^\beta$ for $\beta \in [\omega, \omega_1)$.
## B.3 Definability is equivalent to Decidability for $\alpha < \omega_1^{\omega_1}$

We are ready to extend Theorem 2 up to $\omega_1^{\omega_1}$.

**▶ Theorem 54.** For all ordinals $\alpha < \omega_1^{\omega_1}$, the MSO[$otp_\alpha$]-theory of $\alpha$ is decidable if and only if $\alpha$ is MSO-definable.

*Proof.* For countable $\alpha$ it was proved in Theorem 30.

If $\alpha$ is definable, then MSO[$\alpha$] is equivalent to MSO. Since, the MSO theory of every $\alpha < \omega_2$ is decidable, we obtain that the MSO[$\alpha$] theory of $\alpha$ is decidable.

It remains to show that if an uncountable $\alpha < \omega_1^{\omega_1}$ is undefinable, then MSO[$\alpha$] is undecidable.

Let $\alpha = \omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_0} \times \gamma_0$, where $\omega_2 > \beta_n > \dots > \beta_1 > \beta_0 \ge 0$ and $\gamma_i$ is a non-zero countable ordinal for all $i$. Assume that $\alpha < \omega_1^{\omega_1}$ and $\alpha$ is undefinable.

By Proposition 45, there is $i$ such that (A) $\beta_i \ge \omega$ or (B) $\gamma_i \ge \omega^\omega$.

If (A) holds then $\beta_n \in [\omega, \omega_1)$. In this case there is an MSO[$\alpha$] formula $B(x)$ such that $\alpha \models B(b)$ if and only if the interval $[0, b)$ has the order type $\omega_1^{\beta_n}$. Indeed, let $[x, \infty)$ (respectively, $[0, x)$) be the set $\{y \mid y \le x\}$ (respectively, $\{y \mid y < x\}$) and let $B(x)$ says that $x$ is the minimal element such that $\neg\alpha([x, \infty))$. It is clear that $\alpha \models B(b)$ if the interval $[0, b)$ has the order type $\omega_1^{\beta_n}$. Now, similarly to the proof of Theorem 31, for every MSO[$\omega_1^{\beta_n}$] sentence $C$ we can (effectively) construct an MSO[$\alpha$] sentence $C^*$ such that $\omega_1^{\beta_n} \models C$ if and only if $\alpha \models C^*$. Since, MSO[$\omega_1^{\beta_n}$] is undecidable by Corollary 53, we derive that MSO[$\alpha$] is undecidable.

If (A) does not hold and (B) holds we have that all $\beta_i < \omega$ and therefore $\omega_1^{\beta_i}$ are definable for all $i \le n$, and there are $\gamma_i \ge \omega^\omega$. Let $i$ be the maximal index such that $\gamma_i \ge \omega^\omega$.

There is an MSO formula $B(x)$ such that $\alpha \models B(b)$ if and only if the order type of $[0, b)$ is $\delta := \omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_{i+1}} \times \gamma_{i+1}$ indeed $\delta$ is a definable ordinal, hence such $B$ exists. There is an MSO formula $E(y)$ such that $\alpha \models E(e)$ if the order type of $[0, e)$ is $\delta_1 := \omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_i} \times \gamma_i$. Indeed $E(x)$ states $x$ is the minimal such that the order type of $[x, \infty)$ is less than $\omega_1^{\beta_i}$. The order type of $[b, e)$ is $\mu := \omega_1^{\beta_i} \times \gamma_i$.

Now we will use two reductions. The first one reduces MSO[$\gamma_i$] to MSO[$\omega_1^{\beta_i} \times \gamma_i$]

**▷ Claim 55.** For every $k < \omega$ and an MSO[$\gamma$] sentence $A$ there is an MSO[$\omega_1^k \times \gamma$] sentence $A^*$ such that $\gamma \models A$ if and only if $\omega_1^k \times \gamma \models A^*$.

*Proof.* Since an ordinal $\omega_1^k$ is MSO definable, there is a formula $\text{Mult}(X)$ which defines the set of multiples of $\omega_1^k$, i.e., for every ordinal $\alpha$: $\alpha \models \text{Mult}(S)$ if and only if $S := \{a \in \alpha \mid [0, a) \text{ is a multiple of } \omega_1^k\}$. Let $A^*$ be defined as $\exists S(\text{Mult}(S) \wedge B)$, where $B$ is the relativisation of $A$ on $S$.

For an MSO (or MSO[$\gamma$]) sentence $A$: $\gamma \models A$ if and only if $\omega_1^k \times \gamma \models A^*$. If $A$ is an MSO[$\gamma$] sentence, then $A^*$ is an MSO[$\gamma$] sentence, and we have to express $\gamma$-order type predicates "$X \subseteq S$ has order type $\gamma$" by $\omega_1^k \times \gamma$ order type predicates.

For $x = \omega_1^k \times \beta$ (a multiple of $\omega_1^k$), we denote by $[x]$ an interval $[\omega_1^k \times \beta, \omega_1^k \times (\beta + 1))$. For a set $X$ of multiples of $\omega_1^k$, we denote by $[X]$ the set $\cup_{x \in X}[x]$. Note that $[X]$ is MSO definable from $X$.

Hence, our desired $A^*$ can be defined from $A^*$ by replacing the subformulas "$X$ has the order type $\gamma$" by $\exists Y(Y = [X] \wedge "Y$ has the order type $\omega_1^k \times \gamma$)$). $\triangleleft$

Since, $\gamma_i \ge \omega^\omega$ and it is countable, MSO[$\gamma_i$] is undecidable, hence, we obtain by Theorem 55 that MSO[$\omega_1^{\beta_i} \times \gamma_i$] is undecidable.

The second reduction reduces MSO[$\omega_1^{\beta_i} \times \gamma_i$] to MSO[$\alpha$].
▷ Claim 56. For every MSO[$\omega_1^{\beta_i} \times \gamma_i$] sentence A there is an MSO[$\alpha$] sentence $A^*$ such that $\omega_1^{\beta_i} \times \gamma_i \models A$ if and only if $\alpha \models A^*$.

Proof. Recall that there are MSO formulas $B(x)$ and $E(y)$ such that $\alpha \models B(b) \wedge E(e)$ if and only if $[0, b)$ has the order type $\omega_1^{\beta_n} \times \gamma_n + \dots + \omega_1^{\beta_{i+1}} \times \gamma_{i+1}$ and $[b, e)$ has the order type $\omega_1^{\beta_i} \times \gamma_i$.

As $A^*$ we can take $\exists xy(B(x) \wedge E(y) \wedge C)$, where $C$ is obtained from $A$ first by relativizing $A$ to the interval $[x, y)$. and then replacing atomic subformulas "$X$ has order type $\omega_1^{\beta_i} \times \gamma_i$" by "$X \cup Z$ has the order type $\alpha$," where $Z := \{z \mid z < x \lor z \ge y\}$. $\triangleleft$

Since MSO[$\omega_1^{\beta_i} \times \gamma_i$] is undecidable, we obtain by Theorem 56 that MSO[$\alpha$] is undecidable. and this completes our proof of Theorem 54. ◀