2.1 Notation and logical preliminaries

We will be working with first-order (FO) languages with signatures that contain a binary relation $<$ (possibly, in addition to constants and unary relations). Expressions such as $x> y$ , $x \leqslant y$ , and $x \not < y$ , when used in first-order formulas, are to be interpreted in the usual way, as abbreviations for the formulas $y < x$ , $x < y \vee x = y$ , and $\neg \left (x<y\right )$ respectively; similarly for other variations of the relation $<$ .

Equality will always be assumed to be included in the language. The FO signature that consists only of equality plus the relation symbol $<$ will be denoted by $L_0$ , and the signature that extends $L_0$ with unary relation symbols $\mathbf {c}_{1},\mathbf {c}_{2},\ldots ,\mathbf {c}_{k}$ (regarded as colours) will be denoted by $L_k$ . For $k \geqslant 0$ , $L_k'$ will denote the signature $L_k$ expanded with a single constant symbol, i.e., the signature of structures of the form $\left (A;<,a\right )$ when $k=0$ or $\left (A;<,a,\mathbf {c}_{1},\ldots ,\mathbf {c}_{k}\right )$ when $k>0$ .

Consider an arbitrary fixed first-order language L. The quantifier rank of a formula $\varphi $ is defined as expected and will be denoted by $\mathrm {qr}\left (\varphi \right )$ . We denote by FO $_n$ the set of first-order formulas (of the given signature L) of quantifier rank at most n and for any L-structures $\mathfrak {A}$ and $\mathfrak {B}$ , by $\mathfrak {A}\equiv _n \mathfrak {B}$ we mean equivalence of $\mathfrak {A}$ and $\mathfrak {B}$ with respect to all sentences in FO $_n$ , whereas $\mathfrak {A}\equiv \mathfrak {B}$ means, as usual, their elementary equivalence.

The domain of a structure $\mathfrak {A}$ will be denoted by $\left |\mathfrak {A}\right |$ . The cardinality of a set X will also be denoted by $\left |X\right |$ . From the context, it will always be clear which one of the two meanings applies.

Given an L-structure $\mathfrak {A}$ with domain A, the parametrically definable subsets of $\mathfrak {A}$ are those sets of the form $\left \{x \in A : \left (\mathfrak {A};\bar {a}\right ) \models \varphi \left (x,\bar {a}\right ) \right \}$ , where $\varphi \left (x,\bar {y}\right )$ is a first-order formula with $\bar {y}$ possibly empty, and $\bar {a}$ is a tuple of elements from A of the same arity as $\bar {y}$ .

Given formulas $\varphi $ and $\theta = \theta \left (x,\bar {y}\right )$ that have no variables in common, the relativisation of $\varphi $ to $\theta $ , obtained from $\varphi $ by replacing each subformula of the form $\exists u \left (\psi \left (u,\bar {w}\right )\right )$ with $\exists u \left (\theta \left (u,\bar {y}\right ) \wedge \psi \left (u,\bar {w}\right )\right )$ , and each subformula of the form $\forall u \left (\psi \left (u,\bar {w}\right )\right )$ with the formula $\forall u \left (\theta \left (u,\bar {y}\right ) \rightarrow \psi \left (u,\bar {w}\right )\right )$ , will be denoted by $\varphi ^{\theta }$ . For a detailed account of relativisations, see, e.g., [Reference Rosenstein16, p. 259]. If $\theta = \theta \left (x,y\right )$ is the formula $y \leqslant x$ , with y here playing the role of a parameter, then $\varphi ^{\theta }$ will be written simply as $\varphi ^{\geqslant y}$ . The formulas $\varphi ^{> y}$ , $\varphi ^{\leqslant y}$ , and $\varphi ^{< y}$ are interpreted similarly. If $\theta \left (x,y,z\right )$ is the formula $y \leqslant x \land x < z$ , with y and z now treated as parameters, then $\varphi ^{\theta }$ will be written as $\varphi ^{\left [y,z\right )}$ , and similarly for the other bounded intervals. Given a structure $\mathfrak {A}$ with domain A, a (possibly empty) tuple of elements $\bar {a} \in A^k$ , and a formula $\theta \left (x,\bar {y}\right )$ with $\bar {y}$ being a (possibly empty) k-tuple of variables, $\left (\mathfrak {A};\bar {a}\right )^{\theta }$ will denote the set $\left \{v \in A : \left (\mathfrak {A};\bar {a}\right ) \models \theta \left (v,\bar {a}\right ) \right \}$ .

For any natural number m, the linear order $\left (\left \{0,1,\ldots ,m-1\right \};<\right )$ , ordered in the usual way, will be denoted by $\mathbf {m}$ .

We briefly recall the definitions and main result about characteristic first-order formulas (using the notation of [Reference Doets1, Section 1.6]) that will be needed.

Given a structure $\mathfrak {A}$ with domain A, natural numbers k and n, a k-tuple of elements $\bar {a} = \left (a_0,a_1,\ldots ,a_{k-1}\right )$ from $A^k$ , and a k-tuple of variables $\bar {x} = \left (x_0,x_1,\ldots ,x_{k-1}\right )$ (where $\bar {a}$ and $\bar {x}$ are empty when $k=0$ ), the n-characteristic formula of the structure $\mathfrak {A}$ over the tuple $\bar {a}$ is denoted by $[\kern -0.15em[ \left ( \mathfrak {A}; \bar {a} \right ) ]\kern -0.15em]^n \left ( \bar {x} \right )$ and is defined as follows:

• • $[\kern -0.15em[( \mathfrak {A}; \bar {a})]\kern -0.15em]^0 ( \bar {x} ) := \bigwedge \big \{ \varphi \left ( \bar {x} \right ) : \varphi \ \text {is an atomic or negated atomic formula with}$ $\mathfrak {A} \models \varphi \left ( \bar {a} \right ) \big \}$ ;

• • $[\kern -0.15em[ ( \mathfrak {A}; \bar {a} ) ]\kern -0.15em]^{m+1} ( \bar {x} ) := \bigwedge _{a_k \in A} ( \exists x_k ( [\kern -0.15em[ ( \mathfrak {A}; \bar {a}a_k ) ]\kern -0.15em]^m ( \bar {x}x_k))) \wedge \forall x_k ( \bigvee _{a_k \in A} [\kern -0.15em[ ( \mathfrak {A}; \bar {a}a_k ) ]\kern -0.15em]^m ( \bar {x}x_k))$ .

For languages with finite relational signatures it is well known (see, e.g., [Reference Ebbinghaus, Flum and Thomas5, Theorem 3.4 of Chapter 12]) that, for all natural numbers n and k there are, up to logical equivalence, only finitely many n-characteristic formulas over the class of all structures for that signature and all k-tuples in those structures. If $\bar {a}$ is the empty tuple then $[\kern -0.15em[( \mathfrak {A};\bar {a}) ]\kern -0.15em]^n ( \bar {x} )$ is written as $[\kern -0.15em[ \mathfrak {A} ]\kern -0.15em]^n$ and is called the n-characteristic sentence of $\mathfrak {A}$ . Here are some important facts about characteristic formulas:

1. 1. The formula $[\kern -0.15em[( \mathfrak {A}; \bar {a} ) ]\kern -0.15em]^n ( \bar {x} )$ has quantifier rank n.

2. 2. $\mathfrak {A} \models [\kern -0.15em[ ( \mathfrak {A}; \bar {a} ) ]\kern -0.15em]^n ( \bar {a} )$ .

3. 3. If $\mathfrak {B}$ is a structure in the signature of $\mathfrak {A}$ and $\bar {b}$ is a k-tuple of elements from the domain of $\mathfrak {B}$ then the following three statements are equivalent for any natural number n.

   1. (a) $( \mathfrak {A}; \bar {a} ) \equiv _n ( \mathfrak {B}; \bar {b} )$ .

   2. (b) $\mathfrak {B} \models [\kern -0.15em[ ( \mathfrak {A}; \bar {a} ) ]\kern -0.15em]^n ( \bar {b} )$ .

   3. (c) $[\kern -0.15em[ ( \mathfrak {A}; \bar {a}) ]\kern -0.15em]^n ( \bar {x} ) \equiv [\kern -0.15em[ ( \mathfrak {B}; \bar {b} ) ]\kern -0.15em]^n ( \bar {x} )$ , where $\equiv $ denotes logical equivalence of formulas.

Given a finite relational FO signature L, the set

$$ \begin{align*}\sigma_n\left(L\right) := {\left\{ [\kern-0.15em[ \mathfrak{A} ]\kern-0.15em]^n : \mathfrak{A} \ \text{is any}\ L\text{-structure} \right\}} / \mathord{\equiv}\end{align*} $$

that consists of all equivalence classes of logically equivalent n-characteristic L-sentences will be called the n-spectrum of L, and its cardinality will be denoted by $f\left (L,n\right ) := \left |\sigma _n\left (L\right )\right |$ . For each finite relational signature L, natural number n, and integer i with $1 \leqslant i \leqslant f\left (L,n\right )$ , we fix a sentence $\tau _{L,n,i}$ such that

$$ \begin{align*}\tau_{L,n,1},\,\tau_{L,n,2},\,\ldots,\,\tau_{L,n,f\left(L,n\right)}\end{align*} $$

is an enumeration of all n-characteristic L-sentences, up to logical equivalence.

Given a structure $\mathfrak {A}$ , a subset $A'$ of A that has the property that, for each $a \in A$ , there exists $b \in A'$ such that $\left (\mathfrak {A};a\right ) \equiv _n \left (\mathfrak {A};b\right )$ , will be called an n-support of $\mathfrak {A}$ . It follows from the properties of characteristic formulas that if $\mathfrak {A}$ has a finite relational signature then it has a finite n-support, for each n.

The reader is referred to [Reference Doets3] for background on Ehrenfeucht–Fraïssé games; the players Di and Sy of [Reference Doets3] will be called respectively Spoiler and Duplicator here and the n-round game on structures $\mathfrak {A}$ and $\mathfrak {B}$ will be denoted by $\mathrm {EF}_{n}\!\left (\mathfrak {A},\mathfrak {B}\right )$ .

2.2 Linear orders

A k-coloured linear order, or simply a coloured linear order, is a structure of the type $\mathfrak {A} = \left (A;<,\mathbf {c}_{1},\mathbf {c}_{2},\ldots ,\mathbf {c}_{k}\right )$ where k is a positive integer, $\left (A;<\right )$ is a linear order, and each $\mathbf {c}_{i}$ is a unary predicate in A, called a colour. (Thus, an element in A may have more than one colour, or none whatsoever.) The class of all k-coloured linear orders will be denoted by $\mathcal {L}_k$ . Putting $\bar {\mathbf {c}} = \left (\mathbf {c}_{1},\mathbf {c}_{2},\ldots ,\mathbf {c}_{k}\right )$ , $\mathfrak {A}$ can also be written simply as $\mathfrak {A} = \left (A;<,\bar {\mathbf {c}}\right )$ . The k-tuple of colours $\bar {\mathbf {c}}$ will sometimes be written as $\bar {\mathbf {c}}_k$ , to emphasise that there are k colours. Given a subset B of A, we define ${\bar {\mathbf {c}}}\mathord {\upharpoonright }_{B} := \left ({\mathbf {c}_{1}}\mathord {\upharpoonright }_{B},{\mathbf {c}_{2}}\mathord {\upharpoonright }_{B},\ldots ,{\mathbf {c}_{k}}\mathord {\upharpoonright }_{B}\right )$ and $\mathfrak {A}^B := \left (B;{<}\mathord {\upharpoonright }_{B},{\bar {\mathbf {c}}}\mathord {\upharpoonright }_{B}\right )$ . To keep the notation simple, $\mathfrak {A}^B$ may sometimes also be written simply as $\mathfrak {A}^B = \left (B;<,\bar {\mathbf {c}}\right )$ , tacitly assuming that $<$ and $\bar {\mathbf {c}}$ are restricted in the obvious way. If $a \in A$ then $\mathfrak {A}^{\geqslant a}$ will mean $\mathfrak {A}^B$ where $B = \{ x \in A : a \leqslant x \}$ , and similarly for $\mathfrak {A}^{>a}$ , $\mathfrak {A}^{\leqslant a}$ , and $\mathfrak {A}^{<a}$ . A linear order $\left (A;<\right )$ that is not enriched with any colours will be called monochromatic. For technical convenience, monochromatic linear orders may also be thought of as $0$ -coloured and for which the tuple of colours $\bar {\mathbf {c}}$ is empty. Given a coloured linear order $\mathfrak {A} = \left (A;<,\bar {\mathbf {c}}\right )$ , the monochromatic reduct $\left (A;<\right )$ will be denoted by $\mathfrak {A}^-$ . Unless otherwise specified, the domains of structures $\mathfrak {A}$ , $\mathfrak {B}$ , $\mathfrak {C}_i$ , etc. will be denoted by A, B, and $C_i$ , respectively. To avoid ambiguity, when several structures are under consideration, their order relations will be denoted by $<_{\mathfrak {A}}$ , $<_{\mathfrak {B}}$ , and $<_{\mathfrak {C}_i}$ , respectively. In the interest of readability, $<_{\mathfrak {A}}$ , $<_{\mathfrak {B}}$ , and $<_{\mathfrak {C}_i}$ may sometimes all be denoted simply by $<$ , with the understanding that the relation $<$ is then to be understood as $<_{\mathfrak {A}}$ , $<_{\mathfrak {B}}$ , or $<_{\mathfrak {C}_i}$ , depending on the structure being worked in.

Given two coloured linear orders $\mathfrak {A} = \left (A;<_{\mathfrak {A}},\bar {\mathbf {c}}\right )$ and $\mathfrak {B} = \left (B;<_{\mathfrak {B}},\bar {\mathbf {d}}\right )$ , the sum $\mathfrak {A} + \mathfrak {B}$ of $\mathfrak {A}$ and $\mathfrak {B}$ is defined to be the coloured linear order $\mathfrak {A} + \mathfrak {B} := \left (A \sqcup B;<,\bar {\mathbf {e}}\right )$ , where $A \sqcup B := \left (A \times \left \{0\right \}\right ) \cup \left (B \times \left \{1\right \}\right )$ , the relation $<$ is the union of the three sets $\left \{\left (\left (x,0\right ),\left (y,0\right )\right ) : x <_{\mathfrak {A}} y \right \}$ , $\left \{\left (\left (x,1\right ),\left (y,1\right )\right ): x <_{\mathfrak {B}} y\right \}$ , and $\left \{\left (\left (x,0\right ),\left (y,1\right )\right ): x \in A \ \text {and} \ y \in B \right \}$ , and $\bar {\mathbf {e}} = \bar {\mathbf {c}}\bar {\mathbf {d}}'$ where $\bar {\mathbf {d}}'$ is the tuple that is obtained from $\bar {\mathbf {d}}$ by removing all colours that are already in $\bar {\mathbf {c}}$ , and for any colour $\mathbf {e}_{i}$ in $\bar {\mathbf {e}}$ and any $u \in A \sqcup B$ , $\mathfrak {A}+\mathfrak {B} \models \mathbf {e}_{i}\left (u\right )$ if and only if either u has the form $u = \left (a,0\right )$ and $\mathfrak {A} \models \mathbf {e}_{i}\left (a\right )$ , or u has the form $u = \left (b,1\right )$ and $\mathfrak {B} \models \mathbf {e}_{i}\left (b\right )$ . To keep the notation simple, the elements $(a,0)$ and $(b,1)$ may sometimes be identified simply with the elements $a \in A$ and $b \in B$ respectively. The following Feferman–Vaught style result (see [Reference Feferman and Vaught6]) is easily proved by a straightforward application of Ehrenfeucht–Fraïssé games.

2.3 Trees

A forest is a structure of type $\mathfrak {T} = (T; <)$ in which the relation $<$ is irreflexive, transitive, and left-linear (for each $a \in T$ , the set $\left \{x : x < a\right \}$ is linear). A tree is a forest which is left-connected: for any $a,b \in T$ there exists $c \in T$ such that $c \leqslant a$ and $c \leqslant b$ . A subset of a forest T that is maximal with respect to being connected is called a (connected) component of $\mathfrak {T}$ . The elements of T are called nodes. The least node of $\mathfrak {T}$ , if it exists, is called the root of $\mathfrak {T}$ , and a node is called a leaf when it is maximal with respect to $<$ . For a maximal linearly ordered subset $A \subseteq T$ , the linear order $\mathsf {A} = \left (A;{<}\mathord {\upharpoonright }_{A}\right )$ is called a path in $\mathfrak {T}$ . For a left-closed subset B of a path A, i.e., such that for each $b \in B$ , if $c < b$ then $c \in B$ , too, the linear order $\mathsf {B} = \left (B;{<}\mathord {\upharpoonright }_{B}\right )$ is called a stem (of $\mathsf {A}$ ) in $\mathfrak {T}$ . For ease of notation, the path $\mathsf {A}$ and the stem $\mathsf {B}$ will often be identified with their domains A and B. The set of all paths in $\mathfrak {T}$ will be denoted by $\mathcal {H}\left (\mathfrak {T}\right )$ . A set $I \subseteq T$ is called an interval when, for $a,b,c \in T$ with $a < b < c$ , if $a,c \in I$ then $b \in I$ , too.

As with linear orders, unary predicates regarded as colours may be added to the tree to obtain a coloured tree $\left (\mathfrak {T};\bar {\mathbf {c}}\right )$ .

Given a (possibly monochromatic) tree $\mathfrak {T} = \left (T;<,\bar {\mathbf {c}}\right )$ and a subset $C \subseteq T$ , the structure $\mathfrak {T}^C := \left (C;{<}\mathord {\upharpoonright }_{C},{\bar {\mathbf {c}}}\mathord {\upharpoonright }_{C}\right )$ is defined as with linear orders. In particular, for a node $a \in T$ , the trees $\mathfrak {T}^{\geqslant a}$ , $\mathfrak {T}^{>a}$ , $\mathfrak {T}^{\leqslant a}$ , and $\mathfrak {T}^{< a}$ are defined as the trees $\mathfrak {T}^C$ with C taken to be the set $T^{\geqslant a} := \left \{x \in T : a \leqslant x \right \}$ , $T^{> a} := \left \{x \in T : a < x \right \}$ , $T^{\leqslant a} := \left \{x \in T : x \leqslant a \right \}$ , and $T^{< a} := \left \{x \in T : x < a \right \}$ respectively. The tree $\mathfrak {T}^{\geqslant a}$ will be called the principal subtree generated by a and the stem $T^{<a}$ will be called the principal stem generated by a.

Now, for $\mathfrak {T} = \left (T;<_{\mathfrak {T}},\bar {\mathbf {c}}\right )$ a tree and $\mathfrak {F} = \left (F;<_{\mathfrak {F}},\bar {\mathbf {d}}\right )$ a forest (where either of $\mathfrak {T}$ and $\mathfrak {F}$ may be monochromatic), and a stem B in $\mathfrak {T}$ , we denote by $\mathfrak {T} +_B \mathfrak {F} := \left (T \sqcup F;<_{\mathfrak {T} +_B \mathfrak {F}},\bar {\mathbf {e}}\right )$ the tree with domain

$$ \begin{align*}\left|\mathfrak{T} +_B \mathfrak{F}\right| := T \sqcup F = \left(T \times \left\{0\right\}\right) \cup \left(F \times \left\{1\right\}\right),\end{align*} $$

with order relation

$$ \begin{align*} {<_{\mathfrak{T} +_B \mathfrak{F}}} & := \Big\{ \big( \left(x,0\right), \left(y,0\right) \big) : x <_{\mathfrak{T}} y \Big\} \cup \Big\{ \big( \left(x,1\right), \left(y,1\right) \big) : x <_{\mathfrak{F}} y \Big\} \\ & \;\,\quad \cup \Big\{ \big( \left(x,0\right), \left(y,1\right) \big) : x \in B \ \text{and} \ y \in F \Big\}, \end{align*} $$

and with colours $\bar {\mathbf {e}} = \bar {\mathbf {c}}\bar {\mathbf {d}}'$ , where $\bar {\mathbf {d}}'$ is the tuple that is obtained from $\bar {\mathbf {d}}$ by removing all colours that are already in $\bar {\mathbf {c}}$ , and where, for any colour $\mathbf {e}_{i}$ in $\bar {\mathbf {e}}$ and any $u \in T \sqcup F$ , $\mathfrak {T} +_B \mathfrak {F} \models \mathbf {e}_{i}\left (u\right )$ if and only if either u has the form $u = \left (a,0\right )$ and $\mathfrak {T} \models \mathbf {e}_{i}\left (a\right )$ , or u has the form $u = \left (b,1\right )$ and $\mathfrak {F} \models \mathbf {e}_{i}\left (b\right )$ . In other words, $\mathfrak {T} +_B \mathfrak {F}$ is the tree obtained from $\mathfrak {T}$ by adding the forest $\mathfrak {F}$ to the end of the stem B; a depiction of this tree is given in Figure 1. As with sums of linear orders, for nodes $a \in T$ and $b \in F$ , the nodes $\left (a,0\right )$ and $\left (b,1\right )$ in the tree $\mathfrak {T} +_B \mathfrak {F}$ will often be written simply as a and b rather than as $\left (a,0\right )$ and $\left (b,1\right )$ , to keep the notation simpler, provided that there is no danger of confusion.

Figure 1 A depiction of the tree $\mathfrak {T} +_B \mathfrak {F}$ .

The following composition result generalises Lemma 2.1 and can also be proved by a straightforward Ehrenfeucht–Fraïssé game.

Given a class of (monochromatic) linear orders $\mathcal {C}$ , a tree $\mathfrak {S}$ for which $\mathcal {H}\left (\mathfrak {S}\right ) \subseteq \mathcal {C}$ will be called a tree over $\mathcal {C}$ , or simply a $\mathcal {C}$ -tree, and the class of all k-coloured $\mathcal {C}$ -trees will be denoted by $\mathcal {T}_k\left (\mathcal {C}\right )$ (with $k=0$ in the case of monochromatic trees). If $\mathcal {C} = \left \{\alpha \right \}$ consists of just one linear order then $\mathcal {T}_k\left (\mathcal {C}\right )$ will also be denoted by $\mathcal {T}_k\left (\alpha \right )$ and the trees in $\mathcal {T}_k\left (\alpha \right )$ will be called $\alpha $ -trees.

3.1 A catalogue of properties and axioms

A (possibly coloured) tree $\mathfrak {T}$ , in particular, a linear order, is called:

• • forward discrete, if for any two elements a and b, such that $a < b$ , there exists an immediate successor c of a such that $a < c \leqslant b$ . In the case of linear orders, forward discreteness is equivalent to stating that each non-greatest element has an immediate successor.

• • backward discrete, when each element except for the least element, if there is one, has an immediate predecessor.

• • discrete, when it is both forward discrete and backward discrete.

• • definably forward well-founded, if every parametrically first-order definable non-empty set of elements contains a maximal element.Footnote ¹

• • definably backward well-founded, if every parametrically first-order definable non-empty set of elements contains a minimal (which will also be a least) element.

• • definably bounded forward well-founded, if every parametrically first-order definable non-empty set of elements X that is bounded above (i.e., for which there exists b such that $x \leqslant b$ for each $x \in X$ ) contains a maximal element.

• • definably bounded backward well-founded, if every parametrically first-order definable non-empty set of elements X that is bounded below (i.e., there exists a such that $a \leqslant x$ for each $x \in X$ ) contains a minimal element.

We define the following sentences in the first-order language $L_k$ :

1. 1. $\mathsf {LO}$ expresses that the structure is a linear order, as the conjunction of the sentences expressing irreflexivity, transitivity, and totality:

   $$ \begin{align*} \mathsf{LO} &:= \forall x \left(x \not< x\right) \wedge \forall x \forall y \forall z \big( \left(x < y \wedge y < z\right) \rightarrow x < z\big) \\ & \;\,\quad \wedge \forall x \forall y \left(x < y \vee y < x \vee x = y\right). \end{align*} $$

2. 2. $\mathsf {Tree}$ expresses that the structure is a tree, as the conjunction of sentences that express irreflexivity, transitivity, left-linearity, and left-connectedness:

   $$ \begin{align*} \mathsf{Tree} &:= \forall x \left(x \not< x\right) \wedge \forall x \forall y \forall z \big( \left(x < y \wedge y < z\right) \rightarrow x < z\big) \\ & \;\,\quad \wedge \forall x \forall y \forall z \big( \left(y < x \wedge z < x\right) \rightarrow \left( y < z \vee z < y \vee y = z \right) \big) \\ & \;\,\quad\wedge \forall x \forall y \exists z \left(z \leqslant x \wedge z \leqslant y\right). \end{align*} $$

3. 3. $\mathsf {Le}$ is a sentence that expresses the existence of a $<$ -least element:

   $$ \begin{align*}\mathsf{Le} := \exists x \forall y \left(x \leqslant y\right).\end{align*} $$

4. 4. $\mathsf {Gr}$ is a sentence that expresses the existence of a $<$ -maximal element:

   $$ \begin{align*}\mathsf{Gr} := \exists x \big(\neg \exists y \left(x < y\right) \big).\end{align*} $$

5. 5. $\mathsf {FD}$ is a sentence that expresses the property of forward discreteness:

   $$ \begin{align*}\mathsf{FD} := \forall x \forall y (x < y \rightarrow \exists z (x < z \leqslant y \wedge \neg \exists u (x < u < z))).\end{align*} $$

6. 6. $\mathsf {BD}$ is a sentence that expresses the property of backward discreteness:Footnote ²

   $$ \begin{align*}\mathsf{BD} := \forall x (\exists y (y < x) \rightarrow \exists y (y < x \wedge \neg \exists z (y < z < x))).\end{align*} $$

7. 7. $\mathsf {De}$ is a sentence that expresses the property of density:

   $$ \begin{align*}\mathsf{De} := \forall x \forall y \left(x < y \rightarrow \exists z \left(x < z < y\right)\right).\end{align*} $$

8. 8. $\mathsf {FWF}_k$ is a scheme of (infinitely many) sentences that expresses the property of definable forward well-foundedness and consists of all sentences of the form

   $$ \begin{align*} \mathsf{FWF}_k(\varphi) := \forall \bar{z} ( \exists x (\varphi(x,\bar{z})) \rightarrow \exists x ( \varphi(x,\bar{z}) \wedge \neg \exists y (\varphi(y,\bar{z}) \wedge x < y))),\end{align*} $$
   where $\bar {z} = \left (z_1,z_2,\ldots ,z_n\right )$ is any (possibly empty) tuple of variables and $\varphi \left (x,\bar {z}\right )$ is any formula in the language $L_k$ .

9. 9. $\mathsf {BWF}_k$ is an infinite scheme that expresses the property of definable backward well-foundedness and consists of all sentences of the form

   $$ \begin{align*} \mathsf{BWF}_k(\varphi) := \forall \bar{z}( \exists x(\varphi(x,\bar{z})) \rightarrow \exists x ( \varphi(x,\bar{z}) \wedge \neg \exists y (\varphi(y,\bar{z}) \wedge y < x )))\end{align*} $$
   for any formula $\varphi \left (x,\bar {z}\right )$ in the language $L_k$ .

10. 10. $\mathsf {BFWF}_k$ is an infinite scheme that expresses the property of definable bounded forward well-foundedness and consists of all sentences of the form

    $$ \begin{align*} \mathsf{BFWF}_k(\varphi) & := \forall \bar{z} (( \exists x (\varphi(x,\bar{z})) \wedge \exists y \forall x( \varphi(x,\bar{z}) \rightarrow x \leqslant y)) \\ & \;\,\quad \rightarrow \exists x( \varphi(x,\bar{z}) \wedge \neg \exists y(\varphi(y,\bar{z}) \wedge x < y))) \end{align*} $$
    for any formula $\varphi \left (x,\bar {z}\right )$ in the language $L_k$ .

11. 11. $\mathsf {BBWF}_k$ is an infinite scheme that expresses the property of definable bounded backward well-foundedness and consists of all sentences of the form

    $$ \begin{align*} \mathsf{BBWF}_k(\varphi) & := \forall \bar{z}(( \exists x(\varphi(x,\bar{z})) \wedge \exists y \forall x( \varphi(x,\bar{z}) \rightarrow y \leqslant x)) \\ & \;\,\quad \rightarrow \exists x( \varphi(x,\bar{z}) \wedge \neg \exists y(\varphi(y,\bar{z}) \wedge y < x))) \end{align*} $$
    for any formula $\varphi \left (x,\bar {z}\right )$ in the language $L_k$ .

The following facts about the first-order theory of $\omega $ will be needed later.

Fact 3.1. The first-order theory of $\omega $ can be axiomatised by the theory

$$ \begin{align*}\left\{\mathsf{LO},\mathsf{Le},\neg\mathsf{Gr},\mathsf{BD},\mathsf{FD}\right\}\end{align*} $$

(see, e.g., [Reference Rosenstein16, p. 254]). Moreover, the class of models of this first-order theory consists precisely of all linear orders of the form $\omega + \zeta \cdot \alpha $ where $\alpha $ is any linear order (see, e.g., [Reference Rosenstein16, Corollary 13.12 and Proposition 13.25]).

3.2 The first-order theory of coloured finite linear orders

We define the following first-order theory:

$$\begin{align*}\mathsf{CFLO}_k := \left\{\mathsf{LO},\mathsf{Le},\mathsf{FD}\right\} \cup \mathsf{FWF}_k.\end{align*}$$

The models of $\mathsf {CFLO}_k$ will be called coloured quasi-finite linear orders.

More generally, observe that the following implications hold in any linear order:

$$ \begin{align*} \mathsf {FWF}_k \Longrightarrow \mathsf {BFWF}_k \Longrightarrow \mathsf {BD}\ \mathrm{and}\ \mathsf {BWF}_k \Longrightarrow \mathsf {BBWF}_k \Longrightarrow \mathsf {FD}.\end{align*}$$

Proposition 3.4 below and its proof are similar to [Reference Doets2, Theorem 3.2] except that there, restricted definable induction instead of forward well-foundedness is used to approximate finiteness. Proposition 3.4 and its proof are also similar to the “vertical collapsing” construction used in [Reference Rogers, Backofen and Vijay-Shankar15] to obtain finite tree paths from infinite ones. The construction there, like Proposition 3.4, also approximates finiteness using definable forward well-foundedness. Here, however, we also give an upper bound for the size of the coloured finite linear order produced by the construction, that is n-equivalent to the given coloured quasi-finite linear order. Recall, from the discussion of characteristic sentences in Section 2.1, that $f\left (L_k,n\right )$ is the number of non-equivalent characteristic sentences of quantifier rank n in the language $L_k$ of linear orders expanded with k colours, and that $f\left (L_k,n\right )$ is necessarily finite.

Proposition 3.4. For every coloured quasi-finite linear order $\mathfrak {A} = \left (A;<,\bar {\mathbf {c}}_k\right )$ with k colours and for each natural number n there exists a k-coloured finite linear order $\mathfrak {A}_n$ such that $\mathfrak {A} \equiv _n \mathfrak {A}_n$ . Moreover, taking

$$ \begin{align*}S := {\{ [\kern-0.15em[ \mathfrak{A}^{\geqslant u} ]\kern-0.15em]^n : u \in A\}} / \mathord{\equiv}\end{align*} $$

to be the set of equivalence classes of all the n-characteristic sentences of the orders $\mathfrak {A}^{\geqslant u}$ for $u \in A$ , the cardinality of $\mathfrak {A}_n$ is given by $\left |A_n\right | = \left | S \right | \leqslant f\left (L_k,n\right )$ .

Proof Let $\mathfrak {A}$ be a coloured quasi-finite linear order and let $m = \left |S\right |$ . We start by defining three sequences of coloured linear orders: $\mathfrak {B}_1,\mathfrak {B}_2,\ldots ,\mathfrak {B}_{m-1}$ , $\mathfrak {C}_1,\mathfrak {C}_2,\ldots ,\mathfrak {C}_{m-1}$ , and $\mathfrak {D}_1,\mathfrak {D}_2,\ldots ,\mathfrak {D}_{m-1}$ , where $\mathfrak {B}_i = \mathfrak {C}_i + \mathfrak {D}_i$ and where $\mathfrak {C}_i$ and $\mathfrak {D}_i$ are substructuresFootnote ³ of $\mathfrak {A}$ for each i, as described below. Informally, each $\mathfrak {C}_i$ will consist of the first i elements x in $\mathfrak {A}$ that are maximal with respect to satisfying their n-characteristic formula $[\kern -0.15em[ \mathfrak {A}^{\geqslant x} ]\kern -0.15em]^n\left (x\right )$ , and $\mathfrak {D}_i$ then consists of the elements in $\mathfrak {A}$ that are greater than all of the elements in $\mathfrak {C}_i$ . Formally, $\mathfrak {B}_i$ , $\mathfrak {C}_i$ , and $\mathfrak {D}_i$ will have the following properties for each i:

1. (i) $\mathfrak {B}_i \equiv _n \mathfrak {A}$ ;

2. (ii) for each $u \in B_i$ , $\mathfrak {B}_i^{\geqslant u} \equiv _n \mathfrak {A}^{\geqslant u}$ ;

3. (iii) $\mathfrak {C}_i$ is a coloured finite linear order with domain $C_i$ , such that $\left |C_i \right | = i$ ;

4. (iv) $\mathfrak {D}_i$ is a coloured quasi-finite linear order of the form $\mathfrak {A}^{> u}$ for some $u \in A$ ;

5. (v) for $u \in C_i$ and $v \in B_i$ with $u \neq v$ , $\mathfrak {B}_i^{\geqslant u} \not \equiv _n \mathfrak {B}_i^{\geqslant v}$ .

The exact construction of $\mathfrak {C}_i$ and $\mathfrak {D}_i$ will now be described. Let a be the least element of $\mathfrak {A}$ . We define the formula

The set $\mathfrak {A}^{\varphi _0}$ is non-empty because $\mathfrak {A} \models \varphi _0\left (a\right )$ , and it is definable. Hence, by the forward well-foundedness of $\mathfrak {A}$ , $\mathfrak {A}^{\varphi _0}$ contains a greatest element $a_0$ . Since $a,a_0 \in \mathfrak {A}^{\varphi _0}$ then $\mathfrak {A}^{\geqslant a} \equiv _n \mathfrak {A}^{\geqslant a_0}$ hence

$$ \begin{align*}\mathfrak{A} = \mathfrak{A}^{\geqslant a} \equiv_n \mathfrak{A}^{\geqslant a_0} \cong \mathfrak{A}^{\left[a_0,a_0\right]} + \mathfrak{A}^{> a_0}.\end{align*} $$

Let $\mathfrak {C}_1 := \mathfrak {A}^{\left [a_0,a_0\right ]}$ , $\mathfrak {D}_1 := \mathfrak {A}^{> a_0}$ , and $\mathfrak {B}_1 := \mathfrak {C}_1 + \mathfrak {D}_1$ . Observe that properties (i)–(v) are all satisfied by $\mathfrak {B}_1$ , $\mathfrak {C}_1$ , and $\mathfrak {D}_1$ ; property (iv) follows using part 4 of Lemma 3.2; property (v) follows using property (ii) along with the fact $a_0$ is the greatest element in $\mathfrak {A}^{\varphi _0}$ ; the other properties are straightforward.

Given $\mathfrak {B}_i$ , $\mathfrak {C}_i$ , and $\mathfrak {D}_i$ for some i with $1 \leqslant i < m-1$ , that satisfy properties (i)–(v), the coloured linear orders $\mathfrak {B}_{i+1}$ , $\mathfrak {C}_{i+1}$ , and $\mathfrak {D}_{i+1}$ are obtained as follows. Since $\mathfrak {D}_i$ is a coloured quasi-finite linear order, it contains a least element, say $d_i$ . Define the formula

$$\begin{align*}\varphi_i\left(x\right) := \left(\left[\kern-0.15em[ \mathfrak{D}_i \right]\kern-0.15em]^n\right)^{\geqslant x}.\end{align*}$$

Again, the set $\mathfrak {D}_i^{\varphi _i}$ is non-empty (because $\mathfrak {D}_i \models \varphi _i\left (d_i\right )$ ) and definable, hence, by the definable forward well-foundedness of $\mathfrak {D}_i$ , $\mathfrak {D}_i^{\varphi _i}$ contains a greatest element $e_i$ . Then

(1) $$ \begin{align} \mathfrak{D}_i = \mathfrak{D}_i^{\geqslant d_i} \equiv_n \mathfrak{D}_i^{\geqslant e_i} \cong \mathfrak{D}_i^{\left[e_i,e_i\right]} + \mathfrak{D}_i^{> e_i}. \end{align} $$

Now take $\mathfrak {C}_{i+1} := \mathfrak {C}_i + \mathfrak {D}_i^{\left [e_i,e_i\right ]}$ , $\mathfrak {D}_{i+1} := \mathfrak {D}_i^{> e_i}$ , and $\mathfrak {B}_{i+1} := \mathfrak {C}_{i+1} + \mathfrak {D}_{i+1}$ , and again observe that properties (i)–(v) are all satisfied by $\mathfrak {B}_{i+1}$ , $\mathfrak {C}_{i+1}$ , and $\mathfrak {D}_{i+1}$ : for property (i),

$$ \begin{align*} \mathfrak{B}_{i+1} & = \mathfrak{C}_{i+1} + \mathfrak{D}_{i+1} = (\mathfrak{C}_i + \mathfrak{D}_i^{[e_i,e_i]}) + \mathfrak{D}_i^{> e_i} \\ &\cong \mathfrak{C}_i + (\mathfrak{D}_i^{[e_i,e_i]} + \mathfrak{D}_i^{> e_i}) \equiv_n \mathfrak{C}_i + \mathfrak{D}_i = \mathfrak{B}_i \equiv_n \mathfrak{A} \end{align*} $$

with the first instance of $\equiv _n$ following from (1) and Lemma 2.1; properties (ii) and (iii) are straightforward; property (iv) again follows using part 4 of Lemma 3.2 using the fact that $\mathfrak {D}_i$ is a coloured quasi-finite linear order; property (v) follows using property (ii) for $\mathfrak {B}_{i+1}$ , along with how $\mathfrak {C}_{i+1}$ and $\mathfrak {D}_{i+1}$ were constructed.

Finally, since $\left |S\right | = m$ there are at most m pairwise non-equivalent n-characteristic sentences that are satisfied by the structures $\mathfrak {B}_{m-1}^{\geqslant u}$ for $u \in B_{m-1}$ . Using property (v), the $m-1$ structures of the type $\mathfrak {B}_{m-1}^{\geqslant u}$ , where u ranges over $C_{m-1}$ , must all have pairwise non-equivalent n-characteristic sentences. Hence all structures of the type $\mathfrak {D}_{m-1}^{\geqslant u}$ , where $u \in D_{m-1}$ , must have equivalent n-characteristic sentences. In particular, the n-characteristic sentences of each of these structures $\mathfrak {D}_{m-1}^{\geqslant u}$ must be equivalent to the n-characteristic sentence of $\mathfrak {D}_{m-1}^{\geqslant b}$ , where b is the greatest element of $\mathfrak {D}_{m-1}$ . It follows that $\left |D_{m-1}\right |=1$ and so $\left |B_{m-1}\right | = m$ , i.e., $\mathfrak {A}_n := \mathfrak {B}_{m-1}$ may be taken to be a coloured finite linear order such that $\mathfrak {A} \equiv _n \mathfrak {A}_n$ , as required.⊣

3.3 The first-order theories of coloured well-orders and expansions of $\omega $

We now define the following theories, which will be shown further to axiomatise the first-order theories of the classes of all coloured well-orders, of all coloured expansions of $\omega $ , and of all coloured expansions of $\omega ^{\star }$ (the reverse order of $\omega $ ), respectively:

$$ \begin{align*} \mathsf{CWO}_k & := \left\{\mathsf{LO}\right\} \cup \mathsf{BWF}_k, \\ \mathsf{C}\omega_k & := \left\{\mathsf{LO},\neg\mathsf{Gr},\mathsf{BD}\right\} \cup \mathsf{BWF}_k, \\ \mathsf{C}\omega^{\star}_k & := \left\{\mathsf{LO},\neg\mathsf{Le},\mathsf{FD}\right\} \cup \mathsf{FWF}_k. \end{align*} $$

Corollary 3.7 below is similar to [Reference Doets2, Theorem 3.1] but uses backward well-foundedness instead of definable induction for approximating the structure of coloured $\omega $ .

Using a similar argument, it follows that the theory $\mathsf {C}\omega ^{\star }_k$ axiomatises the first-order theory of the class of coloured expansions of $\omega ^*$ :

3.4 The first-order theory of coloured expansions of $\zeta $

We now define the theory

$$ \begin{align*}\mathsf{C}\zeta_k := \left\{\mathsf{LO},\neg\mathsf{Le},\neg\mathsf{Gr}\right\} \cup \mathsf{BBWF}_k \cup \mathsf{BFWF}_k.\end{align*} $$

3.5 The first-order theory of coloured ordinals

Let $\alpha $ be a monochromatic ordinal such that $\omega < \alpha < \omega ^{\omega }$ . It is known (see [Reference Rosenstein16, Section 13.2]) that the FO theory of $\alpha $ is finitely axiomatised, i.e., there exists a first-order sentence $\Phi \left (\alpha \right )$ in the language $L_0$ such that, for any monochromatic linear order $\mathfrak {A}$ ,

$$ \begin{align*}\mathfrak{A} \models \Phi\left(\alpha\right) \Longleftrightarrow \mathfrak{A} \equiv \alpha,\end{align*} $$

and $\alpha $ is the only ordinal that is a model of $\Phi \left (\alpha \right )$ . The formulation of $\Phi \left (\alpha \right )$ is somewhat involved and for details we refer the reader to [Reference Rosenstein16, Section 13.2]. We now define the theory

$$ \begin{align*}\mathsf{C}\alpha_k := \left\{\Phi\left(\alpha\right)\right\} \cup \mathsf{BWF}_k.\end{align*} $$

3.6 The first-order theory of coloured expansions of $\eta $

We now define the theory

$$ \begin{align*}\mathsf{C}\eta_k := \left\{\mathsf{LO},\neg\mathsf{Le},\neg\mathsf{Gr},\mathsf{De}\right\}.\end{align*} $$

3.7 The first-order theory of coloured expansions of $\lambda $

An axiomatisation of the first-order theory of the class of coloured expansions of $\lambda $ is obtained in [Reference Doets2]. For the sake of completeness of this paper we will briefly describe that axiomatisation here, as it will be needed in Section 5 to axiomatise the first-order theory of the class of $\lambda $ -trees.

A coloured linear order is called definably bounded complete when each of its non-empty definable subsets that is bounded above has a least upper bound. For any formula $\varphi \left (x,\bar {z}\right )$ (where the tuple $\bar {z}$ may be empty) we define the formula

$$ \begin{align*}\mathsf{ub}_{\varphi}{\left(u,\bar{z}\right)} := \forall x \left(\varphi\left(x,\bar{z}\right) \rightarrow x \leqslant u \right),\end{align*} $$

which expresses that u is an upper bound of the set that is defined by $\varphi \left (x,\bar {z}\right )$ . The property of definable bounded completeness can now be expressed by the set $\mathsf {COM}_k$ that consists of all sentences of the form

$$ \begin{align*} \mathsf{COM}_k\left( \varphi\right) & := \forall \bar{z} (( \exists x( \varphi(x,\bar{z})) \wedge \exists u ( \mathsf{ub}_{\varphi}{(u,\bar{z})})) \\ & \;\,\quad \rightarrow \exists u( \mathsf{ub}_{\varphi}{(u,\bar{z})} \wedge \forall v( \mathsf{ub}_{\varphi}{(v,\bar{z})} \rightarrow u \leqslant v))) \end{align*} $$

for any formula $\varphi \left (x,\bar {z}\right )$ in the language $L_k$ .

Given a linear order $\mathfrak {A}$ and a partition P of A of which all members are intervals, we define the binary relation $<_{\mathfrak {P}}$ on P by specifying, for $X,Y \in P$ , that $X <_{\mathfrak {P}} Y$ iff $x <_{\mathfrak {A}} y$ for some $x \in X$ and $y \in Y$ . The linear order $\mathfrak {P} := \left (P;<_{\mathfrak {P}}\right )$ is called a condensation of $\mathfrak {A}$ . Given a transitive binary relation R on A, we define the relation $\sim _R$ on A by specifying, for $u,v \in A$ , that $u \sim _R v$ if and only if any of the following conditions hold:

1. (i) $u = v$ ,

2. (ii) $u <_{\mathfrak {A}} v$ and $sRt$ for all $s,t \in A$ such that $u \leqslant _{\mathfrak {A}} s <_{\mathfrak {A}} t \leqslant _{\mathfrak {A}} v$ , or

3. (iii) $v <_{\mathfrak {A}} u$ and $sRt$ for all $s,t \in A$ such that $v \leqslant _{\mathfrak {A}} s <_{\mathfrak {A}} t \leqslant _{\mathfrak {A}} u$ .

It is straightforward to see that for any transitive binary relation R, the relation $\sim _R$ is an equivalence relation, hence the set is a partition of A into intervals, and so the structure $\mathfrak {Q} = \left (Q;<_{\mathfrak {Q}}\right )$ is a condensation of $\mathfrak {A}$ . The relation R is said to induce the condensation $\mathfrak {Q}$ . If the relation R is definable then $\mathfrak {Q}$ is called a definable condensation. For any formula $\varphi \left (x,y,\bar {z}\right )$ (with the tuple $\bar {z}$ possibly empty) we define the formulas

$$ \begin{align*} \mathsf{bin}_{\varphi}{\left(\bar{z}\right)} & := \forall x \forall y \forall v (( \varphi(x,y,\bar{z}) \wedge \varphi(y,v,\bar{z})) \rightarrow \varphi(x,v,\bar{z})), \\ \mathsf{part}_{\varphi}{\left(u,v,\bar{z}\right)} & := u < v \wedge \forall s \forall t ( u \leqslant s < t \leqslant v \rightarrow \varphi(s,t,\bar{z})), \\ \mathsf{eq}_{\varphi}{\left(u,v,\bar{z}\right)} & := u = v \vee \mathsf{part}_{\varphi}{\left(u,v,\bar{z}\right)} \vee \mathsf{part}_{\varphi}{\left(v,u,\bar{z}\right)}, \\ \mathsf{dense}_{\varphi}{\left(\bar{z}\right)} & := \forall u \forall v \big( \left( u < v \wedge \neg\mathsf{eq}_{\varphi}{\left(u,v,\bar{z}\right)} \right) \\ & \;\,\quad \rightarrow \exists w ( u < w < v \wedge \neg\mathsf{eq}_{\varphi}{(u,w,\bar{z})} \wedge \neg\mathsf{eq}_{\varphi}{(w,v,\bar{z})})), \ \text{and} \\ \mathsf{singleton}_{\varphi}{\left(\bar{z}\right)} & := \forall u \forall v (( u < v \wedge \neg\mathsf{eq}_{\varphi}{(u,v,\bar{z})}) \rightarrow \exists w ( u < w < v \, \\ & \;\,\quad \wedge \neg\mathsf{eq}_{\varphi}{(u,w,\bar{z})} \wedge \neg\mathsf{eq}_{\varphi}{(w,v,\bar{z})} \wedge \forall t ( \mathsf{eq}_{\varphi}{(w,t,\bar{z})} \rightarrow t = w))). \end{align*} $$

The formula $\mathsf {bin}_{\varphi }{\left (\bar {z}\right )}$ expresses that $\varphi \left (x,y,\bar {z}\right )$ defines a transitive binary relation R, the formula $\mathsf {part}_{\varphi }{\left (u,v,\bar {z}\right )}$ expresses property (ii) in the above definition of the relation $\sim _R$ , $\mathsf {eq}_{\varphi }{\left (u,v,\bar {z}\right )}$ expresses that $u \sim _R v$ , $\mathsf {dense}_{\varphi }{\left (\bar {z}\right )}$ expresses that the condensation that is induced by R is densely ordered, and $\mathsf {singleton}_{\varphi }{\left (\bar {z}\right )}$ expresses that the condensation that is induced by R contains a set of singletons that is dense in the condensation.

Following the terminology of [Reference Doets2], a linear order $\mathfrak {A}$ is called definably- I when each of its densely ordered definable condensations contains a set of singletons that is dense in the condensation. The property of a k-coloured linear order being definably-I approximates the countable chain condition of $\mathbb {R}$ , and can be expressed by the set $\mathsf {I}_k$ that consists of all sentences of the form

$$ \begin{align*}\mathsf{I}_k(\varphi):= \forall \bar{z} \left( \big( \mathsf{bin}_{\varphi}{\left(\bar{z}\right)} \wedge \mathsf{dense}_{\varphi}{\left(\bar{z}\right)} \big) \rightarrow \mathsf{singleton}_{\varphi}{\left(\bar{z}\right)} \right)\end{align*} $$

for any formula $\varphi \left (x,y,\bar {z}\right )$ in the language $L_k$ and with the tuple $\bar {z}$ possibly empty.

Finally, the first-order theory of the class of k-coloured expansions of $\lambda $ is axiomatised by the theory

$$ \begin{align*}C\lambda_k := \left\{\mathsf{LO},\neg\mathsf{Le},\neg\mathsf{Gr},\mathsf{De}\right\} \cup \mathsf{COM}_k \cup \mathsf{I}_k,\end{align*} $$

as is seen from the following fact, the proof of which can be found in [Reference Doets2]:

4.1 Trees as coloured linear orders

A tree $\mathfrak {T}$ is called branching complete when for any two distinct paths $\mathsf {A}$ and $\mathsf {B}$ in $\mathfrak {T}$ , each of the sets $\mathsf {A} \setminus \mathsf {B}$ and $\mathsf {B} \setminus \mathsf {A}$ has an infimum in $\mathfrak {T}$ . Branching completeness is equivalent to the following property: for any antichain $\left \{a,b\right \} \subseteq T$ , the set

(2) $$ \begin{align} T_{ab} := \{ x \in T^{\leqslant a}: x \geqslant y \ \text{for each} \ y \in T^{\leqslant a} \cap T^{\leqslant b}\} \end{align} $$

has a least element. Recall the formula $\mathsf {ub}_{\varphi }(u,\bar {z})$ that was defined in Section 3.7 and which expresses the fact that u is an upper bound of the set that is defined by $\varphi (x,\bar {z})$ . Letting $\varphi \left (x,z_1,z_2\right ) := x \leqslant z_1 \wedge x \leqslant z_2$ , the property of branching completeness can therefore be expressed by the sentence

$$ \begin{align*} \mathsf{bc} &:= \forall z_1 \forall z_2 ( \neg (z_1 < z_2 \vee z_2 < z_1 \vee z_1 = z_2) \\ & \;\,\quad \rightarrow \exists u ( u \leqslant z_1 \wedge \mathsf{ub}_{\varphi}(u,z_1,z_2) \wedge \forall v (( v \leqslant z_1 \wedge \mathsf{ub}_{\varphi}(v,z_1,z_2)) \rightarrow u \leqslant v))). \end{align*} $$

A sufficient condition for branching completeness is that every path in the tree is a complete linear order. Thus, in particular, every $\lambda $ -tree is branching complete.

For $\mathfrak {T}$ any tree, $\mathsf {A}$ any stem in $\mathfrak {T}$ ( $\mathsf {A}$ will usually be a path), and $s \in \mathsf {A}$ , we define the following sets (to be explained shortly):

$$ \begin{align*} &\qquad F_l{\left(s\right)} := \left\{ \begin{array}{cl} \emptyset & \text{when}\ s\ \text{has an immediate predecessor,} \\ \displaystyle \left(\bigcap_{t<s}T^{>t}\right) \backslash T^{\geqslant s} & \text{otherwise,} \end{array} \right. \\ &\text{and} \ \ F_u{\left( s \backslash \mathsf{A} \right)} := T^{> s} \backslash \left(\,\bigcup_{t \in \mathsf{A} \cap T^{>s}} \!\!\!\! T^{\geqslant t} \right), \end{align*} $$

and, provided that these sets are non-empty, define the structures $\mathfrak {F}_l{\left (s\right )} := \mathfrak {T}^{F_l{\left (s\right )}}$ and $\mathfrak {F}_u{\left ( s \backslash \mathsf {A} \right )} := \mathfrak {T}^{F_u{\left ( s \backslash \mathsf {A} \right )}}$ . In general, either or both of the sets $F_l{\left (s\right )}$ and $F_u{\left ( s \backslash \mathsf {A} \right )}$ may be empty, in which case the corresponding structure is left undefined. The structures $\mathfrak {F}_l{\left (s\right )}$ and $\mathfrak {F}_u{\left ( s \backslash \mathsf {A} \right )}$ , if defined, are forests and will be called the lower side-forest of s, and the upper side-forest of s with respect to $\mathsf {A}$ , respectively. Finally, the side-forest of s with respect to $\mathsf {A}$ is the forest $\mathfrak {F}\left ( s \backslash \mathsf {A} \right ) := (\mathfrak {T}^{F( s \backslash \mathsf {A} )};s )$ where

$$ \begin{align*} F\left( {s}\backslash \mathsf{A} \right) := \{s\} \cup F_l{\left(s\right)} \cup F_u{\left( s \backslash \mathsf{A} \right)}. \end{align*} $$

The forests $\mathfrak {F}_l{\left (s\right )}$ and $\mathfrak {F}_u{\left ( s \backslash \mathsf {A} \right )}$ are depicted in Figure 2.

Figure 2 The side-forests $\mathfrak {F}_l{\left (s\right )}$ and $\mathfrak {F}_u{\left ( s \backslash \mathsf {A} \right )}$ .

Intuitively, the upper side-forest of s with respect to $\mathsf {A}$ consists of those nodes that sit above s but do not sit above any nodes on $\mathsf {A} \cap T^{>s}$ , and the lower side-forest of s consists of those nodes that sit above $T^{<s}$ but are incomparable with s, unless s has an immediate predecessor, in which case its lower side-forest is left empty so as not to coincide with the upper side-forest of that predecessor. Observe that if $\mathsf {A}$ is a stem with a greatest node b then $F_u{\left ( b \backslash \mathsf {A} \right )} = T^{>b}$ .

The property of branching completeness ensures that if $\mathsf {A}$ is either a path in $\mathfrak {T}$ , or a stem with a greatest node, then the set $\displaystyle \left \{ F\left ( s \backslash \mathsf {A} \right ) \right \}_{s \in \mathsf {A}}$ forms a partition of T. Indeed, each side-forest $F\left ( s \backslash \mathsf {A} \right )$ is non-empty since $s \in F\left ( s \backslash \mathsf {A} \right )$ , and different side-forests $F\left ( s \backslash \mathsf {A} \right )$ and $F\left ( t \backslash \mathsf {A} \right )$ are disjoint by the way that side-forests are defined. To see that $\displaystyle \left \{ F\left ( s \backslash \mathsf {A} \right ) \right \}_{s \in \mathsf {A}}$ covers T, pick any node $u \in T$ , and consider the following cases.

• Case 1: $u \in \mathsf {A}$ . Then $u \in F\left ( u \backslash \mathsf {A} \right )$ .

• Case 2: $u \not \in \mathsf {A}$ .

  • Case 2.1: $u \geqslant x$ for each $x \in \mathsf {A}$ . Then $\mathsf {A}$ must be a stem with a greatest node b, in which case $u \in F\left ( b \backslash \mathsf {A} \right )$ .

  • Case 2.2: There exists $v \in \mathsf {A}$ such that $\left \{u,v\right \}$ is an antichain. By the branching completeness of $\mathfrak {T}$ , the set $T_{vu}$ has a least element $w \in \mathsf {A}$ .

    • Case 2.2.1: $w < u$ . Then $u \in F_u{\left ( w \backslash \mathsf {A} \right )}$ .

    • Case 2.2.2: $w \not < u$ . Then $u \in F_l{\left (w\right )}$ .

This shows that $\bigcup _{s \in \mathsf {A}} F\left ( s \backslash \mathsf {A} \right ) = T$ .

Given $s,t \in \mathsf {A}$ such that $t> s$ , the sets $F_l{\left (s\right )}$ , $F_u{\left ( s \backslash \mathsf {A} \right )}$ , and $F\left ( s \backslash \mathsf {A} \right )$ can be defined in $\left (\mathfrak {T};s,t\right )$ (the expansion of $\mathfrak {T}$ obtained by adding the constants s and t) by the formulas

$$ \begin{align*} &\mathsf{lsf}\left(x,s\right) := \big(\exists u \big( u < s \wedge \neg \exists v \left( u < v < s \right) \big) \rightarrow \neg \left(x = x\right) \big) \\ & \quad \wedge \big( \forall u \big( u < s \rightarrow \exists v \left( u < v < s \right) \big) \rightarrow \big( \forall w \left(w < s \rightarrow w < x \right) \wedge \neg \left(s \leqslant x\right) \big) \big),\\ &\kern-12pt\mathsf{usf}\left(x,s,t\right) := s < x \wedge \neg \exists u \left( s < u \leqslant t \wedge u \leqslant x \right), \ \text{and} \\ &\kern-7pt\mathsf{sf}\left(x,s,t\right) := \left(x = s\right) \vee \mathsf{lsf}\left(x,s\right) \vee \mathsf{usf}\left(x,s,t\right). \end{align*} $$

(The first conjunct in $\mathsf {lsf}\left (x,s\right )$ covers the case where s has an immediate predecessor, and the second conjunct covers the case where s has no immediate predecessor.)

Now suppose that the tree $\mathfrak {T}$ has $k\geq 0$ colours, say $\mathfrak {T} = \left (T;<,\bar {\mathbf {c}}\right )$ where $\bar {\mathbf {c}} = \bar {\mathbf {c}}_k$ (or, simply $\mathfrak {T} = \left (T;<\right )$ if $k=0$ ). Recall that $L_k'$ denotes the signature $L_k$ of k-coloured trees, expanded with a single constant symbol, and $f\left (L_k',n\right )$ denotes the number of non-equivalent n-characteristic sentences of k-coloured trees that have an added constant symbol. Let $p = f\left (L_k',n\right )$ and define an additional set of colours, called extended colours, by $\bar {\mathbf {e}} := \bar {\mathbf {e}}_p = \left (\mathbf {e}_{1},\mathbf {e}_{2},\ldots ,\mathbf {e}_{p}\right )$ . Recall the definition of the sentence $\tau _{L,n,i}$ from the discussion on characteristic formulas in Section 2.1. Now, consider the coloured linear order

$$ \begin{align*} \mathsf{A}^{\mathfrak{T}}\left[\bar{\mathbf{e}}\right] := \left(\mathfrak{T}^{\mathsf{A}};\bar{\mathbf{e}}\right) = \left(\mathsf{A};<,\bar{\mathbf{c}},\bar{\mathbf{e}}\right) \ \ \ \ \text{(or, just} \left(\mathsf{A};<,\bar{\mathbf{e}}\right)\ \text{when}\ \mathfrak{T}\ \text{is monochromatic)} \end{align*} $$

and where the extended colours are defined by specifying, for each $s \in \mathsf {A}$ and each i such that $1 \leqslant i \leqslant p$ ,

$$ \begin{align*}\mathsf{A}^{\mathfrak{T}}\left[\bar{\mathbf{e}}\right] \models \mathbf{e}_{i}\left(s\right) \ \ \text{if and only if} \ \ \mathfrak{F}\left( s \backslash \mathsf{A} \right) \models \tau_{L_k',n,i},\end{align*} $$

i.e., the extended colour of s corresponds to the n-characteristic sentence that is satisfied in $\mathfrak {F}\left ( s \backslash \mathsf {A} \right )$ ).

The linear order $\mathsf {A}^{\mathfrak {T}}\left [\bar {\mathbf {e}}\right ]$ can be viewed as the k-coloured stem $\mathsf {A}$ of $\mathfrak {T}$ that is further enriched with p additional colours, the role of which is to capture, for each $s \in \mathsf {A}$ , the n-equivalence class of the side-forest $\mathfrak {F}\left ( s \backslash \mathsf {A} \right )$ when viewed within $\mathfrak {T}$ . This will allow us to approximate a tree as a coloured linear order, and thereby adapt results on coloured linear orders to trees.

The next theorem relates the first-order equivalence of two trees to the first-order equivalence of their corresponding coloured linear orders.

Let $k,n \in \mathbb {N}$ and $p = f\left (L_k',n\right )$ . Given a formula $\varphi \left (\bar {x}\right )$ (where $\varphi $ may be a sentence) in the language $L_{k+p}$ with colours $\bar {\mathbf {c}}_k$ and $\bar {\mathbf {e}}_p$ , and a variable z that does not occur in $\varphi $ , let $\varphi ^n_z\left (\bar {x}\right )$ denote the formula that is obtained from $\varphi ^{<z}$ (the relativisation of $\varphi $ to the formula $\theta \left (u,z\right ) := u < z$ where z is treated as a parameter) by replacing, for each i, for $1 \leqslant i \leqslant p$ , every atomic formula of the form $\mathbf {e}_{i}\left (y\right )$ that occurs in $\varphi ^{< z}$ with the formula $\tau _{L_k',n,i}^{\mathsf {sf}\left (u,y,z\right )}$ (i.e., $\tau _{L_k',n,i}$ relativised to $\mathsf {sf}\left (u,y,z\right )$ where y and z are treated as parameters).

In other words, the formula $\varphi ^n_z$ is the same as the relativised formula $\varphi ^{<z}$ , except that instead of stating that a node y has colour $\mathbf {e}_{i}$ , $\varphi ^n_z$ states that the side-forest of y with respect to the stem $T^{<z}$ satisfies the characteristic sentence $\tau _{L_k',n,i}$ . If $\varphi $ does not contain any atomic formulas of the form $\mathbf {e}_{i}\left (y\right )$ then $\varphi ^n_z$ is simply the formula $\varphi ^{<z}$ .

The following result, which relates the truth of a first-order formula in a tree to the truth of that formula in the coloured linear order approximating that tree, now follows immediately from the definition of $\varphi ^n_z$ .

Corollary 4.3. Let $k\geq 0$ and $\mathfrak {T}$ be a k-coloured tree with colours $\bar {\mathbf {c}}_k$ , $n \in \mathbb {N}$ , $p = f\left (L_k',n\right )$ , and $\bar {\mathbf {e}} = \bar {\mathbf {e}}_p$ , and let $\varphi \left (\bar {x}\right )$ be a formula in the language $L_{k+p}$ with colours $\bar {\mathbf {c}}_k$ and $\bar {\mathbf {e}}_p$ . For each $a \in T$ and tuple $\bar {b}$ of nodes in $T^{<a}$ of the same arity as $\bar {x}$ ,

$$ \begin{align*} (\mathfrak{T};a,\bar{b}) \models \varphi_a^n (\bar{b}) \ \text{if and only if} \ ((T^{< a})^{\mathfrak{T}} [\bar{\mathbf{e}}];\bar{b}) \models \varphi(\bar{b}).\end{align*} $$

In particular, if $\varphi $ is a sentence then for each $a \in T$ , $\left (\mathfrak {T};a\right ) \models \varphi _a^n$ if and only if $\left (T^{< a}\right )^{\mathfrak {T}}\left [\bar {\mathbf {e}}\right ] \models \varphi $ .

4.2 Towards axiomatising the first-order theory of $\zeta $ -trees

We will now use Theorem 4.2 and Corollary 4.3 to show how the first-order theories of certain classes of coloured $\mathcal {C}$ -trees can be axiomatised. The method used in this section will have the set $\mathcal {C} = \{\zeta \}$ in mind, but can also be used on the sets $\mathcal {C} = \{\omega ^{\star }\}$ and $\mathcal {C} = \{\zeta ,\omega ^{\star }\}$ .

Say that a class of monochromatic linear orders $\mathcal {C}$ has the fusion closure property when the following condition holds:

Consider any class $\mathcal {C}$ of monochromatic linear orders with the following properties:

1. (C1) $\mathcal {C}$ does not contain the singleton linear order;

2. (C2) $\mathcal {C}$ has the fusion closure property;

3. (C3) all linear orders in $\mathcal {C}$ are discrete; and

4. (C4) every $\mathcal {C}$ -tree is branching complete.

The property (C1) is needed to eliminate degenerate cases, (C2) is needed to ensure that paths belong to $\mathcal {C}$ when constructing models of the axiomatisation that will be given below, (C3) is to ensure that all components in the lower and upper side-forests of any $\mathcal {C}$ -tree have roots, and (C4) is needed to ensure that the set of side-forests along any path form a partition of the tree.

Now let k be any natural number and let $\mathcal {S} = \mathcal {T}_k(\mathcal {C})$ be the class of k-coloured $\mathcal {C}$ -trees. Suppose that the following are known:

1. (i) an axiomatisation $\Sigma ^k_{\uparrow }$ of the first-order theory of the class of k-coloured trees

   $$ \begin{align*}\left\{\mathfrak{T}^{\geqslant a} : \mathfrak{T} \in \mathcal{S}, \, a \in T \right\};\end{align*} $$

2. (ii) for each natural number n, an axiomatisation $\Sigma ^{k,n}_{\downarrow }$ of the first-order theory of the class of $\left (k+f\left (L_k',n\right )\right )$ -coloured linear orders

   $$ \begin{align*}\{ \left(T^{<a}\right)^{\mathfrak{T}}\left[\bar{\mathbf{e}}\right] : \mathfrak{T} \in \mathcal{S}, \, a \in T \}.\end{align*} $$

Let

$$ \begin{align*} (\Sigma^k_{\uparrow})' & := \{ \forall x \left( \sigma^{\geqslant x} \right) : \sigma \in \Sigma^k_{\uparrow} \} \ \text{and} \\ (\Sigma^k_{\downarrow})' & := \{ \forall z ( \exists y (y < z) \rightarrow \sigma^n_z ) : n \in \mathbb{N}, \, \sigma \in \Sigma^{k,n}_{\downarrow}\}. \end{align*} $$

In essence, the theory $ (\Sigma ^k_{\uparrow } )'$ expresses for a k-coloured tree $\mathfrak {T}$ that each principal subtree of $\mathfrak {T}$ satisfies $\Sigma ^k_{\uparrow }$ , while, using Corollary 4.3, the theory $ (\Sigma ^k_{\downarrow } )'$ expresses of $\mathfrak {T}$ that, for each natural number n and each principal stem $\mathsf {A}$ in $\mathfrak {T}$ , the linear order $\mathsf {A}^{\mathfrak {T}}\left [\bar {\mathbf {e}}\right ]$ satisfies $\Sigma ^{k,n}_{\downarrow }$ .

Then, the first-order theory of $\mathcal {S}$ can be axiomatised by the theoryFootnote ⁵

$$ \begin{align*}\mathsf{Ax}\left(\mathcal{S}\right) := \left\{\mathsf{Tree},\mathsf{bc}\right\} \cup (\Sigma^k_{\uparrow})' \cup (\Sigma^k_{\downarrow})'\end{align*} $$

as is shown in the next result.

4.3 Applications of the results so far

Theorem 4.4 can be used to axiomatise the first-order theories of classes of trees of the type $\mathcal {S} = \mathcal {T}_k(\mathcal {C})$ , where the requirements on $\mathcal {C}$ are firstly that it must satisfy the properties (C1)–(C4), and secondly, that the axiomatisations $(\Sigma ^k_{\uparrow })'$ and $(\Sigma ^k_{\downarrow })'$ are known. There are three classes $\mathcal {C}$ that fulfill these requirements, namely the sets $\left \{\zeta \right \}$ , $\left \{\omega ^{\star }\right \}$ , and $\left \{\zeta ,\omega ^{\star }\right \}$ .

Theorem 4.4 will hence be used in Section 5.2 to axiomatise the first-order theory of the class of k-coloured $\zeta $ -trees. The two simpler axiomatisations $(\Sigma ^k_{\uparrow })'$ and $(\Sigma ^k_{\downarrow })'$ that are needed for that purpose are those of the first-order theories of the class of k-coloured $\omega $ -trees (to be given in Section 5.1) and of the class of $\left (k+f\left (L_k',n\right )\right )$ -coloured expansions of the linear order $\omega ^{\star }$ (given in Section 3.3).

In the case of the sets $\mathcal {C} = \left \{\omega ^{\star }\right \}$ and $\mathcal {C} = \left \{\zeta ,\omega ^{\star }\right \}$ , an axiomatisation of the first-order theory of the class of $\left (k+f\left (L_k',n\right )\right )$ -coloured expansions of $\omega ^{\star }$ is also needed for $(\Sigma ^k_{\downarrow })'$ . For $(\Sigma ^k_{\uparrow })'$ , one uses in the case $\mathcal {C} = \left \{\omega ^{\star }\right \}$ an axiomatisation of the first-order theory of the class of k-coloured trees of which all paths are finite (which can be deduced from [Reference Rogers, Backofen and Vijay-Shankar15]), and in the case $\mathcal {C} = \left \{\zeta ,\omega ^{\star }\right \}$ one uses an axiomatisation of the first-order theory of the class of k-coloured well-founded trees of which all paths have height at most $\omega $ (a trivial exercise). Axiomatisations for the cases $\mathcal {C} = \left \{\omega ^{\star }\right \}$ and $\mathcal {C} = \left \{\zeta ,\omega ^{\star }\right \}$ will not be presented here however.

5.1 The first-order theory of coloured $\omega $ -trees

The following result will be needed to axiomatise the first-order theory of the class of k-coloured $\omega $ -trees.

It now follows that the theory

$$ \begin{align*}T\omega_k := \left\{\mathsf{Tree}, \mathsf{Le}, \neg\mathsf{Gr}, \mathsf{BD}, \mathsf{FD} \right\} \cup \mathsf{BWF}_k\end{align*} $$

axiomatises the class of k-coloured $\omega $ -trees:

5.2 The first-order theory of coloured $\zeta $ -trees

Using Theorem 4.4, we will now show that the theory

$$ \begin{align*}T\zeta_k := \left\{\mathsf{Tree}, \neg\mathsf{Le}, \neg\mathsf{Gr}, \mathsf{BD}, \mathsf{FD} \right\} \cup \mathsf{BBWF}_k \cup \mathsf{BFWF}_k\end{align*} $$

axiomatises the first-order theory of the class of k-coloured $\zeta $ -trees.

5.3 The first-order theory of coloured $\eta $ -trees

We now define the theory

$$ \begin{align*}T\eta := \left\{\mathsf{Tree}, \neg\mathsf{Le}, \neg\mathsf{Gr}, \mathsf{De} \right\}.\end{align*} $$

The first-order theory of the class of k-coloured $\eta $ -trees is axiomatised by $T\eta $ , as seen from the next theorem.

5.4 The first-order theory of coloured $\lambda $ -trees

Here we will present an axiomatisation of the first-order theory of the class of k-coloured $\lambda $ -trees. We will make use of Fact 3.12, along with the method of partitioning into side-forests from Section 4, to prove that our axiomatisation is complete. In essence, the axiomatisation will express the fact that the linear orders $\mathsf {A}^{\mathfrak {T}}\left [\bar {\mathbf {e}}\right ]$ obtained from a coloured $\lambda $ -tree by partitioning it into side-forests are themselves coloured expansions of $\lambda $ . The proof of completeness of the axiomatisation that we give here follows a similar idea as in the proof of completeness of the axiomatisation of the class of well-founded trees, given in [Reference Doets2], but with several essential differences.

Recall the definition of the formula $\varphi ^n_z$ that was given before Corollary 4.3. By applying it to each $\sigma \in C\lambda _{k+f\left (L_k',n\right )}$ , for any $k \in \mathbb {N}$ we define

$$ \begin{align*}\left(C\lambda_k\right)' := \{ \forall z \left(\sigma_z^n\right) : n \in \mathbb{N}, \, \sigma \in C\lambda_{k+f\left(L_k',n\right)}\}.\end{align*} $$

We will show (Theorem 5.9) that the first-order theory of the class of k-coloured $\lambda $ -trees is axiomatised by the set of sentences

$$ \begin{align*}T\lambda_k := \left\{ \mathsf{Tree}, \neg\mathsf{Gr}, \mathsf{bc} \right\} \cup \left(C\lambda_k\right)'.\end{align*} $$

First, note that every k-coloured $\lambda $ -tree, being branching complete, is a model of $T\lambda _k$ . Next, a few technical lemmas and propositions are needed.

Proof Let $\mathfrak {F}$ be a component in $\mathfrak {T}^{>a}$ . It is immediate that $\mathfrak {F}$ satisfies the sentences $\mathsf {Tree}$ , $\neg \mathsf {Gr}$ , and $\mathsf {bc}$ . To see that $\mathfrak {F}$ satisfies $\left (C\lambda _k\right )'$ , let $n \in \mathbb {N}$ , $p = f\left (L_k',n\right )$ , and $b \in F$ . It then suffices to show that $\left (\mathfrak {F};b\right ) \models \left \{\sigma ^n_b : \sigma \in C\lambda _{k+p}\right \}$ . Clearly $\left (\mathfrak {F};b\right ) \models \left (\mathsf {LO}\right )^n_b$ . It follows from the fact that $\mathfrak {T} \models \left (C\lambda _k\right )'$ that $\mathfrak {T}$ is dense, hence $\left (\mathfrak {F};b\right ) \models \left \{\left (\neg \mathsf {Le}\right )^n_b,\left (\neg \mathsf {Gr}\right )^n_b,\left (\mathsf {De}\right )^n_b\right \}$ .

Since $\mathfrak {T} \models \left (C\lambda _k\right )'$ then in particular $\left (\mathfrak {T};b\right ) \models \left \{ \sigma ^n_b : \sigma \in \mathsf {COM}_{k+p} \right \}$ and $\left (\mathfrak {T};b\right ) \models \left \{ \sigma ^n_b : \sigma \in \mathsf {I}_{k+p} \right \}$ . Hence, by Corollary 4.3, we obtain $\left (T^{<b}\right )^{\mathfrak {T}}[\bar {\mathbf {e}}_p] \models \mathsf {COM}_{k+p}$ and $\left (T^{<b}\right )^{\mathfrak {T}}[\bar {\mathbf {e}}_p] \models \mathsf {I}_{k+p}$ .

To show that $\left (\mathfrak {F};b\right ) \models \left \{ \sigma ^n_b : \sigma \in \mathsf {COM}_{k+p} \right \}$ it suffices, again by Corollary 4.3, to show that $\left (F^{<b}\right )^{\mathfrak {F}}[\bar {\mathbf {e}}_p] \models \mathsf {COM}_{k+p}$ . Let $\bar {d}$ be a tuple of nodes in $F^{<b}$ and let $\varphi (x,\bar {d})$ define the non-empty set $B \subseteq F^{<b}$ in the linear order $ (F^{< b} )^{\mathfrak {F}}[\bar {\mathbf {e}}_p]$ . Suppose that B has an upper bound $u \in F^{<b}$ . By properties of relativised formulas, $\varphi ^{>a}(x,\bar {d})$ defines B in $((T^{< b})^{\mathfrak {T}}[\bar {\mathbf {e}}_p];a )$ . Since $(T^{< b})^{\mathfrak {T}}[\bar {\mathbf {e}}_p] \models \mathsf {COM}_{k+p}$ , we obtain that B has a least upper bound in $T^{<b}$ , hence also in $F^{<b}$ , as required.

Lastly, it will be shown that $\left (\mathfrak {F};b\right ) \models \left \{ \sigma ^n_b : \sigma \in \mathsf {I}_{k+p} \right \}$ by showing, instead, that $(F^{<b} )^{\mathfrak {F}}[\bar {\mathbf {e}}_p] \models \mathsf {I}_{k+p}$ . To this end, let $\bar {d}$ be a tuple of nodes in $F^{<b}$ and let $\varphi (x,y,\bar {d})$ define in the linear order $((F^{< b})^{\mathfrak {F}}[\bar {\mathbf {e}}_p];\bar {d} )$ a transitive binary relation on $F^{<b}$ that induces a densely ordered condensation $\mathfrak {P} = (P;<_{\mathfrak {P}} )$ of $F^{<b}$ . Let

$$ \begin{align*}\psi(x,y,a,\bar{d}) := \left( x \leqslant a \wedge x=y \right) \vee ( a < x \wedge a < y \wedge \varphi^{>a}(x,y,\bar{d})).\end{align*} $$

The formula $\psi (x,y,a,\bar {d})$ defines in $\left (T^{<b}\right )^{\mathfrak {T}}[\bar {\mathbf {e}}_p]$ a transitive binary relation on $T^{<b}$ that induces a densely ordered condensation $\mathfrak {Q} = \left (Q;<_{\mathfrak {Q}}\right )$ of $T^{<b}$ and $\mathfrak {P}$ is a tail of $\mathfrak {Q}$ . Since $\left (T^{<b}\right )^{\mathfrak {T}}[\bar {\mathbf {e}}_p] \models \mathsf {I}_{k+p}$ then it follows that $\mathfrak {Q}$ must contain a set S of singletons that is dense in $\mathfrak {Q}$ , hence ${S}\mathord {\upharpoonright }_{P}$ is a set of singletons in P that is dense in $\mathfrak {P}$ , as required.⊣

Given a k-coloured forest $\mathfrak {F} := \left (F;<,\bar {\mathbf {c}}\right )$ , let $F_r$ denote the (possibly empty) set of roots of the components of $\mathfrak {F}$ and let $F' := F \backslash F_r$ . Consider the following property:

In other words, property $\mathsf {Comp}_{\lambda }\left (\mathfrak {F}\right )$ states that for each component X in $\mathfrak {F}$ , if $\mathfrak {F}^X$ has no root then $\mathfrak {S}^X$ is a model of $T\lambda _k$ , while if $\mathfrak {F}^X$ has a root r then $\mathfrak {F}^Y$ is a model of $T\lambda _k$ for each component Y in $\left (\mathfrak {F}^X\right )^{>r}$ .