# Constructive theory of ordinals

Thierry Coquand, Henri Lombardi, Stefan Neuwirth

► To cite this version:

Thierry Coquand, Henri Lombardi, Stefan Neuwirth. Constructive theory of ordinals. Marco Benini; Olaf Beyersdorff; Michael Rathjen; Peter Schuster. Mathematics for Computation - M4C, World Scientific, In press. hal-03522215

HAL Id: hal-03522215

https://hal.science/hal-03522215

Submitted on 11 Jan 2022

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.
# Constructive theory of ordinals

Thierry Coquand, Henri Lombardi, Stefan Neuwirth

► To cite this version:

Thierry Coquand, Henri Lombardi, Stefan Neuwirth. Constructive theory of ordinals. Marco Benini; Olaf Beyersdorff; Michael Rathjen; Peter Michael Schuster. Mathematics for Computation - M4C, World Scientific, pp.287-318, 2023, 978-981-124-521-3. 10.1142/9789811245220_0012. hal-03522215v2

HAL Id: hal-03522215

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

Submitted on 7 Dec 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
Constructive theory of ordinals

Thierry Coquand*, Henri Lombardi**, and Stefan Neuwirth**

*Computer Science and Engineering Department, University of Gothenburg,
Fax: +46-31-772-3663, Tel.: +46-31-772-1030, coquand@chalmers.se.

**Laboratoire de mathématiques de Besançon, Université Bourgogne Franche-Comté,
Fax: +33-3-8166-6623, henri.lombardi@univ-fcomte.fr, Tel.: +33-3-8166-6330 and
stefan.neuwirth@univ-fcomte.fr, Tel.: +33-3-8166-6351.

January 11, 2022

Abstract

Martin-Löf [1970] describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of computable functions is not needed from a constructive point of view. We give in this paper a constructive theory of ordinals that is similar to Martin-Löf's theory, but based only on the two relations “$x \le y$” and “$x < y$”, i.e. without considering sequents whose intuitive meaning is a classical disjunction. In our setting, the operation “supremum of ordinals” plays an important rôle through its interactions with the relations “$x \le y$” and “$x < y$”. This allows us to approach as much as we may the notion of linear order when the property “$\alpha \le \beta$ or $\beta \le \alpha$” is provable only within classical logic. Our aim is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties.

Contents

<table><tr><td>1</td><td>Introduction</td><td>2</td></tr><tr><td>2</td><td>Linear orders associated to a set of index sets</td><td>6</td></tr><tr><td>2.1</td><td>Index sets</td><td>6</td></tr><tr><td>2.2</td><td>Axioms</td><td>7</td></tr><tr><td>2.3</td><td>Some properties</td><td>8</td></tr></table>
In this file you find the English version, starting on the page numbered E1:

# Constructive theory of ordinals

This paper has appeared in the book Mathematics for Computation – M4C edited by Marco Benini, Olaf Beyersdorff, Michael Rathjen and Peter Michael Schuster (2023). Singapore: World Scientific.

Then the French version begins on the page numbered F1:

# Une théorie constructive des ordinaux

Le lecteur ou la lectrice sera sans doute surprise de l'alternance des sexes ainsi que de l'orthographe du mot «corolaire», avec d'autres innovations auxquelles elle n'est pas habituée. En fait, nous avons essayé de suivre au plus près les préconisations de l'orthographe nouvelle recommandée, telle qu'elle est enseignée aujourd'hui dans les écoles en France.

# Authors

Thierry Coquand, Computer Science and Engineering Department, University of Gothenburg, Sweden

email: thierry.coquand@cse.gu.se

Henri Lombardi, Université de Franche-Comté, CNRS, UMR 6623, LmB, 25000 Besançon, France

email: henri.lombardi@univ-fcomte.fr

Stefan Neuwirth, Université de Franche-Comté, CNRS, UMR 6623, LmB, 25000 Besançon, France

email: stefan.neuwirth@univ-fcomte.fr
<table><tr><td>3</td><td>Inductive construction of ordinals</td><td>10</td></tr><tr><td>3.1</td><td>Subordinals</td><td>11</td></tr><tr><td>3.2</td><td>Definition of the sup law</td><td>11</td></tr><tr><td>3.3</td><td>Definition of &le; and of &lt;</td><td>12</td></tr><tr><td>3.4</td><td>Finite ordinals, bounded ordinals</td><td>13</td></tr><tr><td>3.5</td><td>First consequences</td><td>14</td></tr><tr><td>3.6</td><td>Ordinals and limited principles of omniscience</td><td>17</td></tr><tr><td>3.7</td><td>In classical mathematics</td><td>17</td></tr></table>

<table><tr><td>4</td><td>Fundamental results</td><td>18</td></tr><tr><td>4.1</td><td>Ord<sub>&#x211D;</sub> is an initial object in the category of &#x211D;-orders</td><td>18</td></tr><tr><td>4.2</td><td>More properties</td><td>22</td></tr><tr><td>4.3</td><td>Elementary ordinal arithmetic</td><td>23</td></tr></table>

<table><tr><td>5</td><td>Countable ordinals</td><td>25</td></tr><tr><td>5.1</td><td>First steps</td><td>25</td></tr><tr><td>5.2</td><td>Comparison with Martin-L&ouml;f ordinals</td><td>25</td></tr><tr><td>5.2.1</td><td>Martin-L&ouml;f's formal system</td><td>25</td></tr><tr><td>5.2.2</td><td>Comparison with our system</td><td>26</td></tr></table>

<table><tr><td>Bibliography</td><td>27</td></tr></table>

# 1 Introduction

In classical mathematics, a natural definition for an ordinal is to be an order-type of a well-ordered set (see e.g. [Bourbaki, 1968, III.2.Ex.14]). Nevertheless it is more convenient to use von Neumann ordinals, for which many results can be proved without using choice (see e.g. [Krivine, 1998, Chapitre 2] and [Dehornoy, 2017, Chapitre II]).

Let us now propose a constructive approach. A binary relation < on a set X is said to be *well-founded* if for any family of sets $(E_x)_{x \in X}$ indexed by X, it is possible to construct elements of $\prod_{x \in X} E_x$ by <-induction. Precisely, each time a construction $\gamma$ is given which from an element $a \in X$ and an element $\varphi \in \prod_{x \in X, x < a} E_x$ constructs an element $\gamma(a, \varphi) \in E_a$, there exists a unique $\Phi \in \prod_{x \in X} E_x$ such that for all $a \in X$ we have $\Phi(a) = \gamma(a, \Phi|_{x \in X, x < a})$.

This notion has a clear constructive meaning.

In particular, let us consider a property for elements in X. If the property is <-hereditary, i.e. if it is true for $a \in X$ as soon as it is true for all $x \in X$ with $x < a$, then this property is true for all elements in X.

In constructive mathematics, *Mines, Richman, and Ruitenburg* [1988, Section I.6] define an ordinal as a linearly ordered set for which the order relation
Constructive theory of ordinals

Thierry Coquand, Henri Lombardi, Stefan Neuwirth

December 7, 2024

Abstract

Martin-Löf (1970) describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of computable functions is not needed from a constructive point of view. We give in this paper a constructive theory of ordinals that is similar to Martin-Löf's theory, but based only on the two relations "$x \le y$" and "$x < y$", i.e. without considering sequents whose intuitive meaning is a classical disjunction. In our setting, the operation "supremum of ordinals" plays an important rôle through its interactions with the relations "$x \le y$" and "$x < y$". This allows us to approach as much as we may the notion of linear order when the property "$\alpha \le \beta$ or $\beta \le \alpha$" is provable only within classical logic. Our aim is to give a formal definition corresponding to intuition and to prove that our constructive ordinals satisfy constructively all desirable properties.

**Keywords:** ordinal number; constructive mathematics.

MSC2020: 03E10 03F65.

<table><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>1</td><td>Introduction</td><td>E2</td></tr><tr><td>2</td><td>Linear orders associated to a set of index sets</td><td>E4</td></tr><tr><td>2.1</td><td>Index sets</td><td>E4</td></tr><tr><td>2.2</td><td>Axioms</td><td>E5</td></tr><tr><td>2.3</td><td>Some properties</td><td>E6</td></tr><tr><td>3</td><td>Inductive construction of ordinals</td><td>E7</td></tr><tr><td>3.1</td><td>Subordinals</td><td>E8</td></tr><tr><td>3.2</td><td>Definition of the sup law</td><td>E9</td></tr><tr><td>3.3</td><td>Definition of $\le$ and of $<$</td><td>E9</td></tr><tr><td>3.4</td><td>Finite ordinals, bounded ordinals</td><td>E10</td></tr><tr><td>3.5</td><td>First consequences</td><td>E11</td></tr><tr><td>3.6</td><td>Ordinals and limited principles of omniscience</td><td>E12</td></tr><tr><td>3.7</td><td>In classical mathematics</td><td>E13</td></tr><tr><td>4</td><td>Fundamental results</td><td>E13</td></tr><tr><td>4.1</td><td>Ord is an initial object in the category of $\mathfrak{F}$-orders</td><td>E13</td></tr><tr><td>4.2</td><td>More properties</td><td>E16</td></tr><tr><td>4.3</td><td>Elementary ordinal arithmetic</td><td>E17</td></tr><tr><td>5</td><td>Countable ordinals</td><td>E18</td></tr><tr><td>5.1</td><td>First steps</td><td>E18</td></tr><tr><td>5.2</td><td>Comparison with Martin-Löf ordinals</td><td>E18</td></tr><tr><td>5.2.1</td><td>Martin-Löf's formal system</td><td>E18</td></tr><tr><td>5.2.2</td><td>Comparison with our system</td><td>E19</td></tr><tr><td></td><td>References</td><td>E20</td></tr></tbody></table>
is well-founded. So all subsets of $\mathbb{N}$ are ordinals, even if we don't know whether they have a smallest element.

The **Univalent Foundations Program** [2013, Section 10.3] proceeds similarly in the framework of univalent homotopy type theory; the ordinals of a given universe turn out to form a set (and not a groupoid).

Among other constructive points of view there are descriptions of countable ordinals constructed by induction in the works Brouwer [1926], Gentzen [1936], Church [1938], Kleene [1938], Heyting [1961], and Martin-Löf [1970, Chapter 3].

Brouwer proposes an inductive construction based on the idea that when ordinals $\alpha_n$ are defined for all $n \in \mathbb{N}$ and are linearly ordered well-founded sets, then we can describe the ordinal $\alpha$ corresponding intuitively to $\alpha_1$ followed by $\alpha_2$ followed by $\alpha_3$ followed by $\dots$. The ordered set $\alpha$ defined by Brouwer will again be a linearly ordered well-founded set. And if the order relation on each $\alpha_i$ is decidable, the same is true for $\alpha$.

Two Brouwer ordinals are in general not comparable (within intuitionistic logic): there is no general criterion allowing us to decide whether two ordinals have the same order-type, and, when this is not the case, which is isomorphic to an initial segment of the other.

Martin-Löf describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. Intuitively, an ordinal à la Martin-Löf is inductively defined using two basic constructions:

* there is a minimum ordinal $\emptyset$;

* if $(\alpha_n)$ is an explicit sequence of ordinals (indexed by $\mathbb{N}$ or by an $\mathbb{N}_k = \{n \in \mathbb{N} | n < k\}$), the supremum of the successors of the $\alpha_n$'s is an ordinal<fnref n="1" />.

To say that the definition is inductive is to say that every ordinal is constructed using the indicated rules.

In a constructive framework, we can drop Turing machines and replace Turing computability by intuitive (undefined) computability. In this case, the main difference between Brouwer and Martin-Löf ordinals is that Martin-Löf ordinals, being defined in a “parallel” way rather than in a “sequential” way, are more general: it is possible for any sequence of well-defined ordinals $(\alpha_n)$ to construct the supremum of the successors of the ordinals $\alpha_n$. A drawback is that there is no way to associate to a Martin-Löf ordinal a linearly ordered well-founded set with the same order-type. E.g. if the $\alpha_n$ are all equal to 0 or 1, it is a priori impossible to decide whether the supremum of the successors of the $\alpha_n$'s equals 1 or 2.

<footnote n="1">¹Martin-Löf denotes this supremum by $sup(\alpha_n)$. In his setting, $\emptyset$ is in fact the supremum of the empty sequence. Except for this case, his $sup(\alpha_n)$ is the supremum of the successors of the $\alpha_n$'s; we shall prefer the notation $s(\alpha_n)$.</footnote>
# 1 Introduction

This paper is written in the framework of informal constructive mathematics. We use Bishop's constructive set theory enriched with generalised inductive definitions (Bishop used this kind of constructions for measure theory, Borel sets, and Lebesgue integration).

In classical mathematics, a natural definition for an ordinal is to be an order type of a well-ordered set (see e.g. Bourbaki 1968, III.2.Ex.14). Nevertheless it is more convenient to use von Neumann ordinals, for which many results can be proved without using choice (see e.g. Krivine 1998, Chapitre 2 and Dehornoy 2017, Chapitre II).

Let us now propose a constructive approach. A binary relation $<$ on a set $X$ is said to be well-founded if for any family of sets $(E_x)_{x \in X}$ indexed by $X$ it is possible to construct elements of $\prod_{x \in X} E_x$ by $<$-induction. Precisely, each time a construction $\gamma$ is given which from an element $a \in X$ and an element $\varphi \in \prod_{x \in X, x<a} E_x$ constructs an element $\gamma(a, \varphi) \in E_a$, there exists a unique $\Phi \in \prod_{x \in X} E_x$ such that for all $a \in X$ we have $\Phi(a) = \gamma(a, \Phi|_{x \in X, x<a})$. This notion has a clear constructive meaning.

In particular, let us consider a property for elements in $X$. If the property is $<$-hereditary, i.e. if it is true for $a \in X$ as soon as it is true for all $x \in X$ with $x < a$, then this property is true for all elements in $X$.

In constructive mathematics, Mines, Richman, and Ruitenburg (1988, Section I.6) spell out well-foundedness in a different but equivalent way and define an ordinal as a linearly ordered set for which the order relation is well-founded. So all subsets of $\mathbb{N}$ are ordinals even if we don't know whether they have a smallest element.

The Univalent Foundations Program (2013, Section 10.3) considers “Grayson ordinals” (see Mines, Richman, and Ruitenburg 1988, Exercise I.6.12) in the framework of univalent homotopy type theory; the ordinals of a given universe turn out to form a set (and not a groupoid). This theory of ordinals differs from ours with respect to Axioms 8 and 9 for $\mathfrak{F}$-orders in the following.

Among other constructive points of view there are descriptions of countable ordinals constructed by induction in the works Brouwer 1926, Gentzen 1936, Church 1938, Kleene 1938, Heyting 1961, and Martin-Löf 1970, Chapter 3.

A constructive treatment of von Neumann ordinals based on transfinite recursion is given by Aczel and Rathjen (2010, Section 9.4).

Brouwer proposes an inductive construction based on the idea that when ordinals $\alpha_n$ are defined for all $n \in \mathbb{N}$ and are linearly ordered well-founded sets, then we can describe the ordinal $\alpha$ corresponding intuitively to $\alpha_1$ followed by $\alpha_2$ followed by $\alpha_3$ followed by $\dots$. The ordered set $\alpha$ defined by Brouwer will again be a linearly ordered well-founded set. And if the order relation on each $\alpha_i$ is decidable, the same is true for $\alpha$.

Two Brouwer ordinals are in general not comparable (within intuitionistic logic): there is no general criterion allowing us to decide whether two ordinals have the same order type, and, when this is not the case, which is isomorphic to an initial segment of the other.

The paper Kraus, Nordvall Forsberg, and Xu 2021 compares three distinct constructive approaches to constructive ordinals, denoted by Cnf, Brw and Ord, which are available in the framework of univalent homotopy type theory. The approach Brw is directly inspired by Brouwer ordinals.

Martin-Löf describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. Intuitively, an ordinal à la Martin-Löf is inductively defined using the following two basic constructions:

• there is a minimum ordinal $\emptyset$;

• if $(\alpha_n)$ is an explicit sequence of ordinals (indexed by $\mathbb{N}$ or by an $\mathbb{N}_k = \{n \in \mathbb{N} | n < k\}$), the supremum of the successors of the $\alpha_n$'s is an ordinal.<fnref n="1" />

<footnote n="1">1. Martin-Löf denotes this supremum by $\sup(\alpha_n)$. In his setting, $\emptyset$ is in fact the supremum of the empty sequence. Except for this case, his $\sup(\alpha_n)$ is the supremum of the successors of the $\alpha_n$'s; we shall prefer the notation $s(\alpha_n)$.</footnote>
Ordinals as trees

Martin-Löf proposes to visualise an ordinal $\alpha$ as a *well-founded tree with finite or
countable branchings*. The ordinal $\alpha$ is given with an index set denoted by $In_\alpha$; in
the sequel, it will be an element of the set $\mathfrak{F}_2$ of index sets consisting of $\mathbb{N}$ and its
finite subsets $\mathbb{N}_k$.

• The tree with only its root represents $0$.

• If $(t_i)_{i \in In_\alpha}$ is a family of ordinal trees for a family of ordinals $(\alpha_i)_{i \in In_\alpha}$, the supremum $\alpha = \text{s}(\alpha_i)_{i \in In_\alpha}$ of the successors of the $\alpha_i$'s is given by the ordinal tree for which there are $\#\text{In}_\alpha$ branches above the root and a copy of $t_i$ is attached to the branch indexed by $i \in \text{In}_\alpha$.

If $n \in \mathbb{N}$, the ordinal $\underline{n}$ can be represented by the tree with $n$ successive unary branchings at $n$ nodes, so that it has $n+1$ nodes.

The first infinite ordinal $\omega$ can be represented by the tree that has a countable
branching above the root, the branches being the preceding trees (representing $\underline{n}$,
$n \in \mathbb{N}$).

Its successor, denoted by $\omega + \underline{1}$, can be represented by the tree with unary
branching above the root, the branch being the preceding tree.

The ordinal $\omega + \underline{2}$ can be represented by the tree with unary branching above
the root, the branch being the preceding tree.

The ordinal $\omega + \omega$ can be represented by the tree that has a countable branching
above the root, the branches being the trees representing $\omega + \underline{n}$, $n \in \mathbb{N}$.

<figure><img src="image_1.png" /><figcaption>Figure 1: Ordinal trees.</figcaption></figure>

More formally, such a tree can be defined as the set of its nodes, or branching
points, suitably named. We may consider the set $\text{Lst}(\mathbb{N})$ of finite lists of elements
of $\mathbb{N}$. Let $n \in \mathbb{N}$ and $\ell, \ell' \in \text{Lst}(\mathbb{N})$. We denote by $n \sim \ell$ the list $[n, \ell_1, \dots, \ell_k]$, where
$\ell = [\ell_1, \dots, \ell_k]$, by $\ell \sim n$ the list $[\ell_1, \dots, \ell_k, n]$, and by $\ell \sim \ell'$ the concatenation of
the lists $\ell$ and $\ell'$.
To say that the definition is inductive is to say that every ordinal is constructed using the indicated rules.

In a constructive framework, we can drop Turing machines and replace Turing computability by intuitive (undefined) computability. In this case, the main difference between Brouwer and Martin-Löf ordinals is that Martin-Löf ordinals, being defined in a “parallel” way rather than in a “sequential” way, are more general: it is possible for any sequence of well-defined ordinals ($\alpha_n$) to construct the supremum of the successors of the ordinals $\alpha_n$. A drawback is that there is no way to associate to a Martin-Löf ordinal a linearly ordered well-founded set with the same order type. For example, if the $\alpha_n$ are all equal to $0$ or $1$, it is a priori impossible to decide whether the supremum of the successors of the $\alpha_n$'s equals $1$ or $2$.

## Ordinals as trees

Martin-Löf proposes to visualise an ordinal $\alpha$ as a well-founded tree with finite or countable branchings. The ordinal $\alpha$ is given with an index set denoted by $\text{In}_\alpha$; in the sequel, it will be an element of the set $\mathfrak{F}_2$ of index sets consisting of $\mathbb{N}$ and its finite subsets $\mathbb{N}_k$.

* The tree with only its root represents $0$.

* If $(t_i)_{i \in \text{In}_\alpha}$ is a family of ordinal trees for a family of ordinals $(\alpha_i)_{i \in \text{In}_\alpha}$, the supremum $\alpha = \text{s}(\alpha_i)_{i \in \text{In}_\alpha}$ of the successors of the $\alpha_i$'s is given by the ordinal tree for which there are $\#\text{In}_\alpha$ branches above the root and a copy of $t_i$ is attached to the branch indexed by $i \in \text{In}_\alpha$.

Consider the trees in Figure 1.

If $n \in \mathbb{N}$, the ordinal $\underline{n}$ can be represented by the tree with $n$ successive unary branchings at $n$ nodes, so that it has $n + 1$ nodes.

The first infinite ordinal $\omega$ can be represented by the tree that has a countable branching above the root, the branches bearing the preceding trees (representing $\underline{n}$, $n \in \mathbb{N}$).

Its successor, denoted by $\omega + 1$, can be represented by the tree with unary branching above the root, the branch bearing the preceding tree.

The ordinal $\omega + 2$ can be represented by the tree with unary branching above the root, the branch bearing the preceding tree.

The ordinal $\omega + \omega$ can be represented by the tree that has a countable branching above the root, the branches bearing the trees representing $\omega + \underline{n}$, $n \in \mathbb{N}$.

<figure><img src="image_2.png" /><figcaption>Figure 1 – Ordinal trees.</figcaption></figure>

More formally, such a tree can be defined as the set of its nodes, or branching points, suitably named. We may consider the set $\text{Lst}(\mathbb{N})$ of finite lists of elements of $\mathbb{N}$. Let $n \in \mathbb{N}$ and $\ell$, $\ell' \in \text{Lst}(\mathbb{N})$. We denote by $n \sim \ell$ the list $[n, \ell_1, \dots, \ell_k]$, where $\ell = [\ell_1, \dots, \ell_k]$, by $\ell \sim n$ the list $[\ell_1, \dots, \ell_k, n]$, and by $\ell \sim \ell'$ the concatenation of the lists $\ell$ and $\ell'$.

We remark that $\text{Lst}(\mathbb{N})$ can be enumerated in a natural way<fnref n="2" /> and that the notion of an $\mathbb{N}$-indexed family in $\text{Lst}(\mathbb{N})$ corresponds, via such an enumeration, to the basic (undefined) notion

<footnote n="2">2. For example, for $\ell = [\ell_1, \dots, \ell_k] \in \text{Lst}(\mathbb{N})$, we let $\mu(\ell) = \sum_{i=1}^k (\ell_i + 1)$ and we enumerate the lists by increasing $\mu(\ell)$.</footnote>
We remark that Lst($\mathbb{N}$) can be enumerated in a natural way<fnref n="2" /> and that the notion of an $\mathbb{N}$-indexed family in Lst($\mathbb{N}$) corresponds, via such an enumeration, to the basic (undefined) notion of map from $\mathbb{N}$ to $\mathbb{N}$.

A well-founded tree with finite or countable branchings can then be described as a detachable subset $T$ of Lst($\mathbb{N}$) which is inductively constructed according to the previously indicated process. $T$ is stable by initial segments: if $\ell \in \text{Lst}(\mathbb{N})$, $p \in \mathbb{N}$, and $\ell \sim p \in T$, then $\ell \in T$. Thus, to each ordinal $\alpha$, we are associating a tree, defined as a suitable subset of Lst($\mathbb{N}$), denoted by Tree($\alpha$).

If $n \in \mathbb{N}$, the ordinal $n$ can be described by the finite sequence of $n+1$ lists $[0], [0, 0], \dots, [0, \dots, 0]$.

The first infinite ordinal $\omega$ can be described by the subset of Lst($\mathbb{N}$) enumerated by the infinite sequence $[0], [1], [1, 0], [2], [2, 0], [2, 0, 0], [3], [3, 0], [3, 0, 0], [3, 0, 0, 0]$, etc.

The ordinal $\omega + \frac{1}{2}$ can be described by the infinite sequence $[0], [0, 0], [0, 1], [0, 1, 0], [0, 2], [0, 2, 0], [0, 2, 0, 0], [0, 3], [0, 3, 0], [0, 3, 0, 0], [0, 3, 0, 0, 0]$, etc.

The ordinal $\omega + \frac{1}{2}$ can be described by the infinite sequence $[0], [0, 0], [0, 0, 0], [0, 0, 1], [0, 0, 1, 0], [0, 0, 2], [0, 0, 2, 0], [0, 0, 2, 0, 0], [0, 0, 3], [0, 0, 3, 0], [0, 0, 3, 0, 0], [0, 0, 3, 0, 0, 0]$, etc.

The ordinal $\omega + \omega$ can be described by the doubly infinite sequence $[0], [0, 0], [0, 1], [0, 1, 0], [0, 2], [0, 2, 0], [0, 2, 0, 0], [0, 3], [0, 3, 0], [0, 3, 0, 0], [0, 3, 0, 0, 0], etc., $[1]$ $[1, 0], [1, 0, 0], [1, 0, 1], $[1, 0, 1, 0], $[1, 0, 2], [1, 0, 2, 0], [1, 0, 2, 0, 0], $[1, 0, 3], $[1, 0, 3, 0], $[1, 0, 3, 0, 0], $[1, 0, 3, 0, 0, 0]$, etc., $[2]$, $[2, 0], [2, 0, 0], [2, 0, 0, 0], $[2, 0, 0, 1]$, $[2, 0, 0, 1, 0]$, $[2, 0, 0, 2]$, $[2, 0, 0, 2, 0]$, $[2, 0, 0, 2, 0, 0]$, $[2, 0, 0, 3]$, $[2, 0, 0, 3, 0]$, $[2, 0, 0, 3, 0, 0]$, $[2, 0, 0, 3, 0, 0, 0]$, etc., etc.

* * *

We give in this paper a constructive theory of ordinals that is similar to Martin-Löf's theory, but based only on the two relations "$x \leqslant y$" and "$x < y$", i.e. without considering sequents whose intuitive meaning is a classical disjunction.

In our setting, the operation "supremum of ordinals" plays an important rôle through its interactions with the relations "$x \leqslant y$" and "$x < y$". This allows us to approach as much as we may the notion of linear order when the property "$\alpha \leqslant \beta$ or $\beta \leqslant \alpha$" is provable only within classical logic.

Our problem is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties.

* * *

The first step in Section 2 is to describe which these desirable properties are.

<footnote n="2">²For example, for $\ell = [\ell_1, \dots, \ell_k] \in \text{Lst}(\mathbb{N})$, we let $\mu(\ell) = \sum_{i=1}^k (\ell_i + 1)$ and we enumerate the lists by increasing $\mu(\ell)$.</footnote>
of map from $\mathbb{N}$ to $\mathbb{N}$.

A well-founded tree with finite or countable branchings can then be described as a detachable subset $T$ of $\text{Lst}(\mathbb{N})$ which is inductively constructed according to the previously indicated process. $T$ is closed by initial segments: if $\ell \in \text{Lst}(\mathbb{N})$, $p \in \mathbb{N}$, and $\ell \sim p \in T$, then $\ell \in T$. Thus, to each ordinal $\alpha$, we are associating a tree, defined as a suitable subset of $\text{Lst}(\mathbb{N})$, denoted by $\text{Tree}(\alpha)$.

If $n \in \mathbb{N}$, the ordinal $\underline{n}$ can be described by the finite sequence of $n+1$ lists $[1], [0], [0, 0], \dots, [0, \dots, 0]$.

The first infinite ordinal $\omega$ can be described by the subset of $\text{Lst}(\mathbb{N})$ enumerated by the infinite sequence $[1], [1], [1, 0], [2], [2, 0], [2, 0, 0], [3], [3, 0], [3, 0, 0], [3, 0, 0, 0], \dots$.

The ordinal $\omega + \underline{1}$ can be described by the infinite sequence $[1], [0], [0, 0], [0, 1], [0, 1, 0], [0, 2], [0, 2, 0], [0, 2, 0, 0], [0, 3], [0, 3, 0], [0, 3, 0, 0], [0, 3, 0, 0, 0], \dots$.

The ordinal $\omega + \underline{2}$ can be described by the infinite sequence $[1], [0], [0, 0], [0, 0, 0], [0, 0, 1], [0, 0, 1, 0], [0, 0, 2], [0, 0, 2, 0], [0, 0, 2, 0, 0], [0, 0, 3], [0, 0, 3, 0], [0, 0, 3, 0, 0], [0, 0, 3, 0, 0, 0], \dots$.

The ordinal $\omega + \omega$ can be described by the doubly infinite sequence $[1], [0], [0, 0], [0, 1], [0, 1, 0], [0, 2], [0, 2, 0], [0, 2, 0, 0], [0, 3], [0, 3, 0], [0, 3, 0, 0], [0, 3, 0, 0, 0], \dots, [1], [1, 0], [1, 0, 0], [1, 0, 1], [1, 0, 1, 0], [1, 0, 2], [1, 0, 2, 0], [1, 0, 2, 0, 0], [1, 0, 3], [1, 0, 3, 0], [1, 0, 3, 0, 0], [1, 0, 3, 0, 0, 0], \dots, [2], [2, 0], [2, 0, 0], [2, 0, 0, 0], [2, 0, 0, 1], [2, 0, 0, 1, 0], [2, 0, 0, 2], [2, 0, 0, 2, 0], [2, 0, 0, 2, 0, 0], [2, 0, 0, 3], [2, 0, 0, 3, 0], [2, 0, 0, 3, 0, 0], [2, 0, 0, 3, 0, 0, 0], \dots, \dots$.

These trees, seen as subsets of $\text{Lst}(\mathbb{N})$ defined by induction, form a well-defined set in the context of intuitive constructive mathematics. It can be denoted by $\text{ord}_2$ (see Definition 3.1). Note that from a constructive point of view, $\text{ord}_2$ is a discrete set if, and only if, the Markov principle is valid. This set $\text{ord}_2$ is a “set of ordinal names” in Martin-Löf 1970. And the set of Martin-Löf ordinals, $\text{Ord}_2^{\text{ML}}$, is a quotient of $\text{ord}_2$ by a correctly proved equivalence relation. The set $\text{Ord}_2^{\text{ML}}$ and our set $\text{Ord}_2$ are discrete if the little principle of omniscience LPO is valid. See Section 5.2 for more details.

***

We give in this paper a constructive theory of ordinals that is similar to Martin-Löf's theory, but based only on the two relations "$x \le y$" and "$x < y$", i.e. without considering sequents whose intuitive meaning is a classical disjunction.

In our setting, the operation “supremum of ordinals” plays an important rôle through its interactions with the relations "$x \le y$” and “$x < y$”. This allows us to approach as much as we may the notion of linear order when the property "$\alpha \le \beta$ or $\beta \le \alpha$” is provable only within classical logic. In the same way, the impossibility of constructively proving linear order for real numbers is circumvented by the introduction of $x < y$, $x \le y$ and $\sup(x, y)$, which are all three indispensable.

Our problem is to give a formal definition corresponding to intuition and to prove that our constructive ordinals satisfy constructively all desirable properties.

***

The first step in Section 2 is to describe these desirable properties.

## 2 Linear orders associated to a set of index sets

We define in this section the structure of linear orders associated to a set $\mathfrak{F}$ of index sets, $\mathfrak{F}$-orders for short.

### 2.1 Index sets

First we need a set $\mathfrak{F}$ of index sets. An index set will be denoted by $I, J, K, I', I'', J', I_a, I_b$, etc.

An *index set* is simply a set that will be used as a set of indices for the families we shall consider. In the sequel, a finitely enumerated subset of *A* is always a subset of *A* defined à la Bishop by a map $N_k \to A$. If *A* is discrete, a finitely enumerated subset of *A* is a detachable subset.
## 2 Linear orders associated to a set of index sets

We define in this section the structure of linear orders associated to a set $\mathfrak{F}$ of index sets, $\mathfrak{F}$-orders for short.

### 2.1 Index sets

First we need a set $\mathfrak{F}$ of index sets. An index set will be denoted by $I, J, K, I'$, $I''$, $J'$, $I_a, I_b$, etc.

An *index set* is simply a set that will be used as a set of indices for the families we shall consider. In the sequel a finitely enumerated subset of $A$ is always a subset of $A$ defined à la Bishop by a map $N_k \to A$. If $A$ is discrete, a finitely enumerated subset of $A$ is a detachable subset.

**Properties of the set $\mathfrak{F}$ of index sets.** We will assume that

* $N$ and the finite sets $N_k = \{n \in \mathbb{N} | n < k\} (k \ge 0)$ are elements of $\mathfrak{F}$;

* any finitely enumerated subset$^3$ of an element of $\mathfrak{F}$ is isomorphic$^4$ to an element of $\mathfrak{F}$;

* if $J \in \mathfrak{F}$, the set of finitely enumerated subsets of $J$ is isomorphic to an element of $\mathfrak{F}$;

* $\mathfrak{F}$ is stable by disjoint unions indexed by $\mathfrak{F}$: we will denote by $I+J$ a disjoint union of $I$ and $J$, and by $\sum_{i \in I} J_i$ a disjoint union of the family $(J_i)_{i \in I}$.

Disjoint unions are to be understood as direct sums in the category of sets. The disjoint union $J = \sum_{i \in I} J_i$ comes with a family $\iota_\ell : J_\ell \to J$ of injective maps realising $J$ as the direct sum of the $J_i$'s in the category of sets.

If we restrict ourselves to countable ordinals, we can take for $\mathfrak{F}$ the set

$$ \mathfrak{F}_2 = \{ N_k \mid k \in \mathbb{N}, k \ge 0 \} \cup \{ \mathbb{N} \} $$

with convenient operations for the set of finite subsets of an $I \in \mathfrak{F}$ and for disjoint unions of elements of $\mathfrak{F}$ indexed by an element of $\mathfrak{F}$. Any other set $\mathfrak{F}$ of index sets will contain $\mathfrak{F}_2$.

An $\mathfrak{F}$-indexed family of elements of $E$ is a family $(x_i)_{i \in I}$ where $I \in \mathfrak{F}$ and the $x_i$'s $\in E$. The set of $\mathfrak{F}$-indexed families of elements of $E$ is denoted by $\text{Fam}(\mathfrak{F}, E)$.

We shall restrict the use of subscripts for ordinal variables to this meaning, and use superscripts for all other uses.

<footnote>$^3$By definition this is a subobject given by a function $N_k \to \mathfrak{F}$.</footnote>

<footnote>$^4$In the category of sets.</footnote>
**Properties of the set $\mathfrak{F}$ of index sets.** We will assume that

* $\mathbb{N}$ and the finite sets $\mathbb{N}_k = \{n \in \mathbb{N} | n < k\} (k \ge 0)$ are elements of $\mathfrak{F}$;

* any finitely enumerated subset<fnref n="3" /> of an element of $\mathfrak{F}$ is isomorphic<fnref n="4" /> to an element of $\mathfrak{F}$;

* if $J \in \mathfrak{F}$, the set of finitely enumerated subsets of $J$ is isomorphic to an element of $\mathfrak{F}$;

* $\mathfrak{F}$ is closed by disjoint unions indexed by $\mathfrak{F}$: we will denote by $I + J$ a disjoint union of $I$ and $J$, and by $\sum_{i \in I} J_i$ a disjoint union of the family $(J_i)_{i \in I}$.

Disjoint unions are to be understood as direct sums in the category of sets. The disjoint union $J = \sum_{i \in I} J_i$ comes with a family $\iota_\ell: J_\ell \to J$ of injective maps realising $J$ as the direct sum of the $J_i$'s in the category of sets.

If we restrict ourselves to countable ordinals, we can take for $\mathfrak{F}$ the set

$$ \mathfrak{F}_2 = \{ \mathbb{N}_k | k \in \mathbb{N}, k \ge 0 \} \cup \{ \mathbb{N} \} $$

with convenient operations for the set of finite subsets of an $I \in \mathfrak{F}$ and for disjoint unions of elements of $\mathfrak{F}$ indexed by an element of $\mathfrak{F}$. Any other set $\mathfrak{F}$ of index sets will contain $\mathfrak{F}_2$.

An $\mathfrak{F}$-indexed family of elements of $E$ is a family $(x_i)_{i \in I}$, where $I \in \mathfrak{F}$ and the $x_i$'s $\in E$. The set of $\mathfrak{F}$-indexed families of elements of $E$ is denoted by $\text{Fam}(\mathfrak{F}, E)$.

We shall restrict the use of subscripts for ordinal variables to this meaning, and use superscripts for all other uses.

## 2.2 Axioms

A structure of $\mathfrak{F}$-order on a set $(E, =)$ is given as $(E, <, \le, 0_E, \sup, \text{s})$, where

* $<$ and $\le$ are binary relations defined on $(E, =)$;

* $0_E$ is an element of $E$ and we let $E^* = \{\alpha \in E | 0_E < \alpha\}$;

* $\sup$ is a map from $\text{Fam}(\mathfrak{F}, E^*)$ to $E^*$: taking as input an element $(\alpha_i)_{i \in I}$ of $\text{Fam}(\mathfrak{F}, E^*)$, it constructs an element of $E^*$ denoted by $\alpha = \sup(\alpha_i)_{i \in I}$;

* $\text{s}$ is a unary map from $E$ to $E^*$: taking as input an element $\beta \in E$, it constructs an element of $E^*$ denoted by $\text{s}(\beta)$.

**Definition 2.1.** In order to write axioms with finite sup's, we define $\sup(\alpha, \beta)$ for $\alpha, \beta \in E$ in the following way (using implicitly Axiom 15): $\sup(0_E, \alpha) = \alpha = \sup(\alpha, 0_E)$; if $\alpha, \beta \in E^*$, $\sup(\alpha, \beta)$ is already defined.

These data are to satisfy the following axioms.

### Axioms for $\mathfrak{F}$-orders.

1. $\alpha = \beta$ if and only if $\alpha \le \beta$ and $\beta \le \alpha$ (reflexivity and antisymmetry);

2. $0_E \le \alpha$;

3. if $\alpha < \alpha$ then $0_E = \beta$ (irreflexivity);

4. if $\alpha < \beta$ then $\alpha \le \beta$;

5. if $\alpha \le \beta$ and $\beta \le \gamma$, then $\alpha \le \gamma$ (transitivity 1);

6. if $\alpha < \beta$ and $\beta \le \gamma$, then $\alpha < \gamma$ (transitivity 2);

7. if $\alpha \le \beta$ and $\beta < \gamma$, then $\alpha < \gamma$ (transitivity 3);

<footnote n="3">3. By definition this is a subobject given by a function $\mathbb{N}_k \to \mathfrak{F}$.</footnote>

<footnote n="4">4. In the category of sets.</footnote>
## 2.2 Axioms

A structure of $\mathfrak{F}$-order on a set ($E, =$) is given as ($E, <, \leqslant, 0_E, \sup, \text{s}$), where

* $<$ and $\leqslant$ are binary relations defined on ($E, =$);

* $0_E$ is an element of $E$ and we let $E^* = \{ \alpha \in E \mid 0_E < \alpha \}$;

* $\sup$ is a map from $\text{Fam}(\mathfrak{F}, E^*)$ to $E^*$: taking as input an element $(\alpha_i)_{i \in I}$ of $\text{Fam}(\mathfrak{F}, E^*)$, it constructs an element of $E^*$ denoted by $\alpha = \sup(\alpha_i)_{i \in I}$;

* $\text{s}$ is a unary map from $E$ to $E^*$: taking as input an element $\beta \in E$, it constructs an element of $E^*$ denoted by $\text{s}(\beta)$.

**Definition 2.1.** In order to write axioms with finite $\sup$'s we define $\sup(\alpha, \beta)$ for $\alpha, \beta \in E$ in the following way (using implicitly Axiom 15): $\sup(0_E, \alpha) = \alpha = \sup(\alpha, 0_E)$; if $\alpha, \beta \in E^*$, $\sup(\alpha, \beta)$ is already defined.

These data are to satisfy the following axioms.

### Axioms for $\mathfrak{F}$-orders.

1. $\alpha = \beta$ if and only if $\alpha \leq \beta$ and $\beta \leq \alpha$ (reflexivity and antisymmetry);

2. $0_E \leq \alpha$;

3. if $\alpha < \alpha$ then $0_E = \beta$ (irreflexivity);

4. if $\alpha < \beta$ then $\alpha \leq \beta$;

5. if $\alpha \leq \beta$ and $\beta \leq \gamma$, then $\alpha \leq \gamma$ (transitivity 1);

6. if $\alpha < \beta$ and $\beta \leq \gamma$, then $\alpha < \gamma$ (transitivity 2);

7. if $\alpha \leq \beta$ and $\beta < \gamma$, then $\alpha < \gamma$ (transitivity 3);

8. $\alpha < \text{s}(\beta)$ if and only if $\alpha \leq \beta$ (using Axiom 1 this gives $\alpha < \text{s}(\alpha)$);

9. $\text{s}(\beta) \leq \alpha$ if and only if $\beta < \alpha$;

10. if $\alpha < \gamma$ and $\beta < \gamma$, then $\sup(\alpha, \beta) < \gamma$;

11. if $\alpha < \sup(\alpha, \beta)$ then $\alpha < \beta$;

12. if $\gamma < \alpha$ and $\alpha \leq \sup(\beta, \gamma)$, then $\alpha \leq \beta$;

13. for $(\alpha_i)_{i \in I} \in \text{Fam}(\mathfrak{F}, E^*)$ and $\beta \in E$ we have (characteristic property of $\sup$)

$$ \alpha_i \leq \beta \text{ for all } i \in I \text{ if and only if } \sup(\alpha_i)_{i \in I} \leq \beta; $$
8. $\alpha < s(\beta)$ if and only if $\alpha \le \beta$ (using Axiom 1 this gives $\alpha < s(\alpha)$);

9. $s(\beta) \le \alpha$ if and only if $\beta < \alpha$;

10. if $\alpha < \gamma$ and $\beta < \gamma$, then $\sup(\alpha, \beta) < \gamma$;

11. if $\alpha < \sup(\alpha, \beta)$ then $\alpha < \beta$;

12. if $\gamma < \alpha$ and $\alpha \le \sup(\beta, \gamma)$, then $\alpha \le \beta$;

13. for $(\alpha_i)_{i \in I} \in \text{Fam}(\mathfrak{F}, E^*)$ and $\beta \in E$, we have

$$ \alpha_i \le \beta \text{ for all } i \in I \text{ if and only if } \sup(\alpha_i)_{i \in I} \le \beta $$

(characteristic property of sup);

14. if $\gamma < \beta$ for all $\gamma < \alpha$, then $\alpha \le \beta$;

15. either $\alpha \le 0_E$ or $0_E < \alpha$.

The category of $\mathfrak{F}$-orders is defined by its morphisms

$$ (E, <_E, \leq_E, 0_E, \sup_E, s_E) \to (F, <_F, \leq_F, 0_F, \sup_F, s_F), $$

which are maps from $E$ to $F$ preserving the structure (in the usual meaning).

**Comments.** 1) Let $\gamma \in E^*$ and $(\alpha_n)_{n \in \mathbb{N}}$ such that $\alpha_n = \gamma$ or $\alpha_n = s(\gamma)$ for each $n$. The element $\sup(\alpha_n)_{n \in \mathbb{N}}$ hesitates between $\gamma$ and $s(\gamma)$. Thus there is no hope that the disjunction "$\alpha \le \beta$ or $\beta < \alpha$" be constructive for arbitrary elements $\alpha, \beta \ne 0_E$. Consequently, we have introduced the sup map together with its axioms in order to best describe in what sense the order can be thought of as linear. Perhaps this is not optimal (reasonable axioms, satisfied for the set $\text{Ord}_2$ of ordinals of the second class constructed in Section 3, might be missing).

2) The irreflexivity is given a form that, instead of stating a negation, allows $E$ to reduce to a singleton. This happens if and only if $0_E = s(0_E)$, which implies $0_E < 0_E$ using Axiom 8.

3) Axiom 15 expresses that $\{0_E\}$ is detachable. This contrasts with the fact that elements other than $0_E$ do not define detachable singletons. We have defined sup on $E^*$ rather than on $E$ in order to satisfy constructively the disjunction of Axiom 15.

4) The characteristic property of sup shows that this law satisfies idempotence as well as generalised associativity and commutativity. ◇

## 2.3 Some properties

**Proposition and definition 2.2 (generalising Definition 2.1).**

For $\alpha^1, \dots, \alpha^r \in E$ we let

$$ \sup(\alpha^1, \dots, \alpha^r) \stackrel{\text{def}}{=} \begin{cases} 0_E & \text{if } \alpha^1 = \dots = \alpha^r = 0_E \\ \text{the sup of the } \alpha^k \ne 0_E & \text{otherwise.} \end{cases} $$

The characteristic property of sup is satisfied:

$$ \alpha^1 \le \beta \text{ and } \dots \text{ and } \alpha^r \le \beta \text{ if and only if } \sup(\alpha^1, \dots, \alpha^r) \le \beta. $$

**Fact 2.3.** Let $\alpha, \beta$ be elements of $E$.

* $s(\alpha) < s(\beta)$ if and only if $\alpha < \beta$.

* $s(\alpha) \le s(\beta)$ if and only if $\alpha \le \beta$.
14. if $\gamma < \beta$ for all $\gamma < \alpha$, then $\alpha \le \beta$;

15. either $\alpha \le 0_E$ or $0_E < \alpha$.

The category of $\mathfrak{F}$-orders is defined by its morphisms

$$(E, <_E, \leq_E, 0_E, \sup_E, s_E) \to (F, <_F, \leq_F, 0_F, \sup_F, s_F),$$

which are maps from $E$ to $F$ preserving the structure (in the usual meaning).

**Comments.** 1) Let $\gamma \in E^*$ and $(\alpha_n)_{n \in \mathbb{N}}$ such that $\alpha_n = \gamma$ or $\alpha_n = s(\gamma)$ for each $n$. The element $\sup(\alpha_n)_{n \in \mathbb{N}}$ hesitates between $\gamma$ and $s(\gamma)$. Thus there is no hope that the disjunction "$\alpha \le \beta$ or $\beta < \alpha$" be constructive for arbitrary elements $\alpha, \beta \ne 0_E$. Consequently, we have introduced the sup map together with its axioms in order to best describe in what sense the order can be thought of as linear. Perhaps this is not optimal (reasonable axioms, satisfied for the set $\text{Ord}_2$ of ordinals of the second class constructed in Section 3, might be missing).

2) The irreflexivity is given a form that, instead of stating a negation, allows $E$ to reduce to a singleton. This happens if and only if $0_E = s(0_E)$, which implies $0_E < 0_E$ using Axiom 8.

3) Axiom 15 expresses that $\{0_E\}$ is detachable. This contrasts with the fact that elements other than $0_E$ do not define detachable singletons. We have defined sup on $E^*$ rather than on $E$ in order to satisfy constructively the disjunction of Axiom 15.

4) The characteristic property of sup shows that this law satisfies idempotence as well as generalised associativity and commutativity. $\diamond$

## 2.3 Some properties

**Proposition and definition 2.2** (generalising Definition 2.1). For $\alpha^1, \dots, \alpha^r \in E$ we let

$$ \sup(\alpha^1, \dots, \alpha^r) \stackrel{\text{def}}{=} \begin{cases} 0_E & \text{if } \alpha^1 = \dots = \alpha^r = 0_E \\ \text{the sup of the } \alpha^k \ne 0_E \text{ otherwise.} & \end{cases} $$

The characteristic property of sup is satisfied:

$$ \alpha^1 \le \beta \text{ and } \dots \text{ and } \alpha^r \le \beta \text{ if and only if } \sup(\alpha^1, \dots, \alpha^r) \le \beta. $$

**Fact 2.3.** Let $\alpha, \beta$ be elements of $E$.

* $s(\alpha) < s(\beta)$ if and only if $\alpha < \beta$.
Proof. Use Axioms 8 and 9.

**Fact 2.4.** Axioms 10 to 12 and 14 are in fact equivalences:

10. $\alpha < \gamma$ and $\beta < \gamma$ hold simultaneously if and only if $\sup(\alpha, \beta) < \gamma$;

11. $\alpha < \sup(\alpha, \beta)$ if and only if $\alpha < \beta$;

12. if $\gamma < \alpha$, then $\alpha \leq \sup(\beta, \gamma)$ holds if and only if $\alpha \leq \beta$;

14. $\alpha \leq \beta$ if and only if $\gamma < \beta$ for all $\gamma < \alpha$.

Proof. Use the transitivities and the characteristic property of sup.

**Fact 2.5** (s commutes with finite sup's, notation as in Proposition and Definition 2.2). We have $\sup(s(\alpha), s(\beta)) = s(\sup(\alpha, \beta))$ and more generally $\sup(s(\alpha^1), \dots, s(\alpha^r)) = s(\sup(\alpha^1, \dots, \alpha^r))$. In particular, if $\alpha^1 < \gamma, \dots, \alpha^r < \gamma$, then $\sup(\alpha^1, \dots, \alpha^r) < \gamma$.

Proof. It suffices to prove $s(\sup(\alpha, \beta)) = \sup(s(\alpha), s(\beta))$. We have the following chain of equivalences: $s(\sup(\alpha, \beta)) \leq \gamma \iff \sup(\alpha, \beta) < \gamma \iff (\alpha < \gamma \text{ and } \beta < \gamma) \iff (s(\alpha) \leq \gamma \text{ and } s(\beta) \leq \gamma) \iff \sup(s(\alpha), s(\beta)) \leq \gamma$. $\square$

**Proposition and definition 2.6** (definition of infinitary s and its characteristic property). For any $(\alpha_i)_{i \in J} \in \text{Fam}(\mathfrak{F}, E)$, we define $s(\alpha_i)_{i \in J} = \sup(s(\alpha_i))_{i \in J}$. Then we get the following equivalence:

$$ \alpha_i < \beta \text{ for all } i \in J \text{ if and only if } s(\alpha_i)_{i \in J} \leq \beta. $$

Proof. Use Axioms 9 and 13.

We write $F \subseteq_f I$ in order to express that $F$ is a finitely enumerated subset of $I$.

**Fact 2.7.** Let $\alpha, \beta^1, \dots, \beta^m \in E$.

1. Assume that $\alpha = s(\alpha_i)_{i \in J}$ with $(\alpha_i)_{i \in J} \in \text{Fam}(\mathfrak{F}, E)$ and that $\alpha_i < \sup(\beta^1, \dots, \beta^m)$ for all $i \in J$. Then $\alpha \leq \sup(\beta^1, \dots, \beta^m)$.

2. Assume that $\beta^k = s((\beta^k)_i)_{i \in J_k}$ with $((\beta^k)_i)_{i \in J_k} \in \text{Fam}(\mathfrak{F}, E)$ for $k \in [1..m]$. Let $F_1 \subseteq_f J_1, \dots, F_m \subseteq_f J_m$ not all be empty. If

$$ \alpha \leq \sup((\beta^k)_j)_{k \in [1..m]}, \quad j \in F_k, $$

$$ \text{then } \alpha < \sup(\beta^1, \dots, \beta^m). $$

Proof. 1. This is Proposition and Definition 2.6.

2. Suppose e.g. that $F_1$ is nonempty. Then $\alpha \leq \sup((\beta^1)_j)_{j \in F_1} < \beta^1 \leq \sup(\beta^1, \dots, \beta^m)$. The strict inequality comes from Fact 2.5 because all $(\beta^1)_j$'s are $< \beta^1$ by Proposition and Definition 2.6. $\square$

# 3 Inductive construction of ordinals

In Sections 3 and 4, the set $\mathfrak{F}$ of index sets is fixed but often implied.

We shall define a set of ordinals $\text{Ord}$ (more precisely $\text{Ord}_{\mathfrak{F}}$) and we shall prove that it is an initial object in the category of $\mathfrak{F}$-orders.

First we define a set $\text{ord}$ of names for $\mathfrak{F}$-indexed ordinals by an inductive definition. The simplest inductive definition of an infinite set is that of $\mathbb{N}$: it admits an element 0 and a successor map $x \mapsto s(x): \mathbb{N} \to \mathbb{N}$. The inductive definition of $\text{ord}$ is very similar to that of $\mathbb{N}$. In $\mathbb{N}$, each element is either 0 or an $s(x)$ for an $x \in \mathbb{N}$. Similarly, in $\text{ord}$, each element is either 0 or the $s$ of an $\mathfrak{F}$-indexed family in $\text{ord}$; we denote by $\text{ord}^*$ the set of elements of this second type.
• $s(\alpha) \le s(\beta)$ if and only if $\alpha \le \beta$.

*Proof.* Use Axioms 8 and 9. $\square$

**Fact 2.4.** Axioms 10 to 12 and 14 are in fact equivalences:

10. $\alpha < \gamma$ and $\beta < \gamma$ hold simultaneously if and only if $\sup(\alpha, \beta) < \gamma$;

11. $\alpha < \sup(\alpha, \beta)$ if and only if $\alpha < \beta$;

12. if $\gamma < \alpha$, then $\alpha \le \sup(\beta, \gamma)$ holds if and only if $\alpha \le \beta$;

14. $\alpha \le \beta$ if and only if $\gamma < \beta$ for all $\gamma < \alpha$.

*Proof.* Use the transitivities and the characteristic property of sup. $\square$

**Fact 2.5** (s commutes with finite sup's, notation as in Proposition and definition 2.2).

We have $\sup(s(\alpha), s(\beta)) = \sup(\sup(\alpha, \beta))$. More generally, $\sup(s(\alpha^1), \dots, s(\alpha^r)) = s(\sup(\alpha^1, \dots, \alpha^r))$.

In particular, if $\alpha^1 < \gamma, \dots, \alpha^r < \gamma$, then $\sup(\alpha^1, \dots, \alpha^r) < \gamma$.

*Proof.* It suffices to prove $s(\sup(\alpha, \beta)) = \sup(s(\alpha), s(\beta))$. We have the following chain of equivalences: $s(\sup(\alpha, \beta)) \le \gamma \iff \sup(\alpha, \beta) < \gamma \iff (\alpha < \gamma$ and $\beta < \gamma) \iff (s(\alpha) \le \gamma$ and $s(\beta) \le \gamma) \iff \sup(s(\alpha), s(\beta)) \le \gamma$. $\square$

**Proposition and definition 2.6** (definition of infinitary s and its characteristic property). For any $(\alpha_i)_{i \in J} \in \text{Fam}(\mathfrak{F}, E)$, we define $s(\alpha_i)_{i \in J} = \sup(s(\alpha_i))_{i \in J}$. Then we get the following equivalence:

$\alpha_i < \beta$ for all $i \in J$ if and only if $s(\alpha_i)_{i \in J} \le \beta$.

*Proof.* Use Axioms 9 and 13. $\square$

We write $F \subseteq_I J$ in order to express that $F$ is a finitely enumerated subset of $I$.

**Fact 2.7.** Let $\alpha, \beta^1, \dots, \beta^m \in E$.

1. Assume that $\alpha = s(\alpha_i)_{i \in J}$ with $(\alpha_i)_{i \in J} \in \text{Fam}(\mathfrak{F}, E)$ and that $\alpha_i < \sup(\beta^1, \dots, \beta^m)$ for all $i \in J$. Then $\alpha \le \sup(\beta^1, \dots, \beta^m)$.

2. Assume that $\beta^k = s((\beta^k)_i)_{i \in J_k}$ with $((\beta^k)_i)_{i \in J_k} \in \text{Fam}(\mathfrak{F}, E)$ for $k \in [1..m]$. Let $F_1 \subseteq_I J_1, \dots, F_m \subseteq_I J_m$ not all be empty. If

$$\alpha \le \sup((\beta^k)_j)_{k \in [1..m]}, \quad j \in F_k,$$

$$\text{then } \alpha < \sup(\beta^1, \dots, \beta^m).$$
**Definition 3.1.** The set **ord** (more precisely **ord**<sub>F</sub>) is defined in an inductive way: it is to admit a distinguished element **0** and a map

$$s: \mathrm{Fam}(\mathfrak{F}, \mathrm{ord}) \to \mathrm{ord}.$$

N.B.: The only constraint in this inductive definition is that s be indeed a map from Fam(<sub>F</sub>, ord) to ord.

An element of **ord** will be called *name of an ordinal* in the sequel.

When <sub>F</sub> = <sub>F</sub><sub>2</sub>, we get the set of names of countable ordinals, denoted by **ord**<sub>2</sub>.

*Remark 3.2.* Each element $\alpha \in \mathrm{ord}^*$ is given with two data:

* the index set used in the definition of $\alpha$: it will be denoted by $\mathrm{In}_\alpha$;

* the family $\chi_{\mathrm{ord}}(\alpha, i)_{i \in \mathrm{In}_\alpha}$ of its *definitional subordinals*, i.e. the element of Fam(<sub>F</sub>, ord) such that $\alpha = s(\chi_{\mathrm{ord}}(\alpha, i))_{i \in \mathrm{In}_\alpha}$.

Thus the inductive definition of **ord** implies the existence of a map $\alpha \mapsto \mathrm{In}_\alpha: \mathrm{ord}^* \to \mathfrak{F}$ and the existence of a dependent family $(\alpha, i) \mapsto \chi_{\mathrm{ord}}(\alpha, i)$ which is defined for $\alpha \in \mathrm{ord}^*$ and $i \in \mathrm{In}_\alpha$. In order to make the text more readable, we shall perform a slight abuse of notation: we shall not mention the construction of the dependent family $\chi_{\mathrm{ord}}$, and the notation $\alpha_i$ will be an abbreviation for $\chi_{\mathrm{ord}}(\alpha, i)$. With these conventions we may write $\alpha = s(\alpha_i)_{i \in \mathrm{In}_\alpha}$. $\diamond$

For $\alpha^1, \dots, \alpha^r \in \mathrm{ord}$ we define $s(\alpha^1, \dots, \alpha^r) = s(\alpha^i)_{i \in [1..r]}$.

In particular, if $\alpha \in \mathrm{ord}$, its *immediate successor* $s(\alpha)$ is the element $\beta = s(\beta_i)_{i \in \mathrm{In}_\beta}$, where $\mathrm{In}_\beta = \mathbb{N}_1 = \{0\}$ and $\beta_0 = \alpha$. The sequence $(\underline{m})_{m \in \mathbb{N}}$ in **ord** is defined inductively by $\underline{m} + 1 = s(\underline{m})$. Then we can define $\omega = s(\underline{n})_{n \in \mathbb{N}}$.

In order to prove a property for $\alpha = s(\alpha_i)_{i \in \mathrm{In}_\alpha}$, it is sufficient to prove the property for each $\alpha_i$. In a similar way we can construct inductively a map whose domain is **ord**, or define inductively a predicate on **ord**. This is stated precisely in Fact 3.4 and done e.g. in Definitions 3.3 and 3.6 and more generally throughout the rest of this article.

## 3.1 Subordinals

Here is a correct inductive definition.

**Definition 3.3.** Let $\alpha = s(\alpha_i)_{i \in \mathrm{In}_\alpha} \in \mathrm{ord}^*$. An element $\beta$ of **ord** is a *definitional subordinal* of $\alpha$ if $\beta = \alpha_i$ for an $i \in \mathrm{In}_\alpha$: we write this $\beta \prec_1 \alpha$. An element $\gamma$ is a *subordinal of* $\alpha$ if it is a *definitional subordinal* of $\alpha$ or a *subordinal of* a *definitional subordinal* of $\alpha$. We write this $\gamma \prec \alpha$.

Thus **0** is the only element of **ord** which has no subordinal.

The following fact acknowledges that the definition of the relations $\prec_1$ and $\prec$ is a correct inductive definition on **ord**.

**Fact 3.4.** The relations $\prec_1$ and $\prec$ on **ord** are *well-founded*.

Consequently there is no infinite branch in the tree of subordinals of an element of **ord**, in the following sense.

**Fact 3.5.** A sequence $(\alpha^j)_{j=1,2,...}$ in **ord**, where each $\alpha^{j+1}$ is a *subordinal of* $\alpha^j$, reaches in a finite number of steps $\alpha^r = \underline{0}$.

Remark that in order to perform a construction (or a proof) by $\prec_1$-induction or by $\prec$-induction, the case **0** has to be dealt with separately since it has no subordinal. Nevertheless, we shall be able to avoid this case distinction until considering ordinal arithmetic on page E17.
### 3.2 Definition of the sup law

**Definition 3.6.** 1. The law sup: Fam($\mathfrak{F}$, ord*) → ord* is defined in the following way. Let $(\alpha^j)_{j \in J}$ be a family in ord* with $J \in \mathfrak{F}$. If $\alpha^j = s((\alpha^j)_i)_{i \in I_j}$, then $\sup(\alpha^j)_{j \in J}$ is the element $\varepsilon = s(\varepsilon_k)_{k \in K}$, where

* $K$ is the disjoint union of the $I_j$'s;

* $(\varepsilon_k)_{k \in K}$ is the family defined by $\varepsilon_k = (\alpha^j)_i$ if $\iota_j(i) = k$

(here $\iota_j: I_j \to K$ is the injective map from $I_j$ to the disjoint union of the $I_j$'s). We shall write $\sup(\alpha^j)_{j \in [1..r]} = \sup(\alpha^1, \dots, \alpha^r)$.

2. The sup of a finite family in ord is defined in the following way.

$$ \sup(\alpha^1, \dots, \alpha^r) \stackrel{\text{def}}{=} \begin{cases} \emptyset & \text{if } \alpha^1 = \dots = \alpha^r = \emptyset \\ \text{the sup of the } \alpha^k \in \text{ord}^* & \text{otherwise.} \end{cases} $$

We note that Item 2 is formally included in Item 1 if we adopt the convention $\text{In}_{\emptyset} = \mathbb{N}_0$. However, this convention would not allow us to define an arbitrary $\mathfrak{F}$-indexed sup in ord.

### 3.3 Definition of $\le$ and of $<$

The main job remains to be done, i.e. to define two binary relations $\le$ and $<$ on ord with the required properties, viz.

* the relation "$\alpha \le \beta$ and $\beta \le \alpha$" has to be an equivalence relation (we shall denote by Ord the quotient set);

* the relations $\le$ and $<$ and the maps sup and s have to descend to the quotient (we shall not change their names), i.e. they have to be compatible with the equivalence relation;

* with these maps and relations, Ord has to be an $\mathfrak{F}$-order.

Moreover, since the map s: Fam($\mathfrak{F}$, ord) → ord* is defined before the map sup: Fam($\mathfrak{F}$, ord*) → ord*, we have to verify in our construction that Axiom 13 is satisfied in Ord. This will be a consequence of Fact 3.11 in the following.

For our job, we define inductively two asymmetric relations between, on the left side, an element of ord and, on the right side, a nonempty finitely enumerated set of elements of ord, written as a list:

$$ \alpha \le \beta^1, \dots, \beta^m \quad \text{and} \quad \alpha < \beta^1, \dots, \beta^m \quad (m \ge 1). $$

**Conventions.** 
* The letters $\alpha, \beta, \gamma, \varepsilon$, possibly with exponents, indices or primes, are used for elements of ord.

* If $\alpha$ is an element of ord and if $F$ is a finite list, possibly empty, in $\text{In}_\alpha$, we denote by $\alpha_F$ the list of the $\alpha_i$'s with $i$ in $F$.

The two relations are defined by simultaneous induction in the following way.

Particular cases involving $\emptyset$ are avoided by using the convention $\text{In}_{\emptyset} = \mathbb{N}_0$. Let $m$ be an integer $\ge 1$.

$\alpha \le \beta^1, \dots, \beta^m$ is defined as $\alpha_i < \beta^1, \dots, \beta^m$ for all $i \in \text{In}_\alpha$.

$\alpha < \beta^1, \dots, \beta^m$ is defined as there are $F_1 \subseteq_f \text{In}_{\beta^1}, \dots, F_m \subseteq_f \text{In}_{\beta^m}$ not all empty with $\alpha \le \beta^1_{F_1}, \dots, \beta^m_{F_m}$.
For $\alpha^1, \dots, \alpha^r \in \mathbf{ord}$ we define $s(\alpha^1, \dots, \alpha^r) = s(\alpha^i)_{i \in \llbracket 1..r \rrbracket}$.

In particular, if $\alpha \in \mathbf{ord}$, its immediate successor $s(\alpha)$ is the element $\beta = s(\beta_i)_{i \in \mathbf{In}_\beta}$ where $\mathbf{In}_\beta = \mathbb{N}_1 = \{0\}$ and $\beta_0 = \alpha$. The sequence $(\underline{m})_{m \in \mathbb{N}}$ in $\mathbf{ord}$ is defined inductively by $\underline{m} + 1 = s(\underline{m})$. Then we can define $\underline{\omega} = s(\underline{n})_{n \in \mathbb{N}}$.

In order to prove a property of $\alpha = s(\alpha_i)_{i \in \mathbf{In}_\alpha}$, it is sufficient to prove the property for each $\alpha_i$. In a similar way we can construct inductively a map whose domain is $\mathbf{ord}$, or define inductively a predicate on $\mathbf{ord}$. This is stated precisely in Fact 3.4.

## 3.1 Subordinals

Here is a correct inductive definition.

**Definition 3.3.** Let $\alpha = s(\alpha_i)_{i \in \mathbf{In}_\alpha} \in \mathbf{ord}^*$. An element $\beta$ of $\mathbf{ord}$ is a definitional subordinal of $\alpha$ if $\beta = \alpha_i$ for an $i \in \mathbf{In}_\alpha$: we write this $\beta \prec_1 \alpha$. An element $\gamma$ is a subordinal of $\alpha$ if it is a definitional subordinal of $\alpha$ or a subordinal of a definitional subordinal of $\alpha$. We write this $\gamma \prec \alpha$.

Thus $\mathfrak{Q}$ is the only element of $\mathbf{ord}$ which has no subordinal.

**Fact 3.4.** The relations $\prec_1$ and $\prec$ on $\mathbf{ord}$ are well-founded.

Consequently there is no infinite branch in the tree of subordinals of an element of $\mathbf{ord}$, in the following sense.

**Fact 3.5.** A sequence $(\alpha^j)_{j=1,2,...}$ in $\mathbf{ord}$, where each $\alpha^{j+1}$ is a subordinal of $\alpha^j$, reaches in a finite number of steps $\alpha^r = \mathfrak{Q}$.

Remark that in order to perform a construction (or a proof) by $\prec_1$-induction or by $\prec$-induction, the case $\mathfrak{Q}$ has to be dealt with separately since it has no subordinal. Nevertheless, we shall be able to avoid this case distinction until considering ordinal arithmetic on page 23.

## 3.2 Definition of the sup law

**Definition 3.6.**

1. The law $\sup : \mathrm{Fam}(\mathfrak{F}, \mathbf{ord}^*) \to \mathbf{ord}^*$ is defined in the following way.

Let $(\alpha^j)_{j \in J}$ be a family in $\mathbf{ord}^*$ with $J \in \mathfrak{F}$.

If $\alpha^j = s((\alpha^j)_i)_{i \in I_j}$, then $\sup((\alpha^j)_{j \in J})$ is the element $\varepsilon = s(\varepsilon_k)_{k \in K}$ where

* $K$ is the disjoint union of the $I_j$'s;

* $(\varepsilon_k)_{k \in K}$ is the family defined by $\varepsilon_k = (\alpha^j)_i$ if $\iota_j(i) = k$
This definition is correct since elements of **ord** are inductively defined and the pair of clauses is inductive.

Without the convention that $\text{In}_0 = \mathbb{N}_0$, we would have had to include Fact 3.8 below in the definition. This convention is a little miracle allowing us to avoid a case-by-case reasoning with respect to the disjunction "$\alpha = \emptyset$ or $\alpha \in \text{ord}^*$" in the proofs.

The meaning of the two relations is $\alpha \le \sup(\beta^1, \dots, \beta^m)$ and $\alpha < \sup(\beta^1, \dots, \beta^m)$.

**Lemma 3.7.** We have $\alpha < \beta^1, \dots, \beta^m$ if and only if $\alpha < \sup(\beta^1, \dots, \beta^m)$. Similarly, we have $\alpha \le \beta^1, \dots, \beta^m$ if and only if $\alpha \le \sup(\beta^1, \dots, \beta^m)$.

*Proof.* Let us write

$$ \alpha < \beta^1, \dots, \beta^m \text{ for } \alpha < \sup(\beta^1, \dots, \beta^m), $$

$$ \alpha \le \beta^1, \dots, \beta^m \text{ for } \alpha \le \sup(\beta^1, \dots, \beta^m). $$

Let $\varepsilon = \sup(\beta^1, \dots, \beta^m)$. Then $\alpha < \beta^1, \dots, \beta^m$ if and only if $\alpha \le \varepsilon_F$ with $F$ a nonempty finitely enumerated subset of the disjoint union $K$ of the $\text{In}_{\beta j}$'s and $\varepsilon_k = (\beta^j)_i$ if $k$ is the image of $i$ in $K$; letting $F_j = F \cap \text{In}_{\beta j}$, not all $F_j$'s are empty and this may be rewritten as $\alpha \le \beta^1_{F_1}, \dots, \beta^m_{F_m}$. This holds if and only if $\alpha < \beta^1, \dots, \beta^m$.

We have $\alpha \le \beta^1, \dots, \beta^m$ if and only if, for all $i \in \text{In}_\alpha$, $\alpha_i < \varepsilon$, i.e. $\alpha_i < \beta^1, \dots, \beta^m$, i.e. $\alpha_i < \beta^1, \dots, \beta^m$; this holds if and only if $\alpha \le \beta^1, \dots, \beta^m$. $\square$

The relation $\alpha =_{\text{Ord}} \beta$ is defined as meaning "$\alpha \le \beta$ and $\beta \le \alpha$".

We shall show in Section 4 that the relation $\cdot =_{\text{Ord}}$ is an equivalence relation and we shall define the set **Ord** as the quotient of **ord** by this relation.

Let us note that until Theorem 4.8, the symbol $=$ between two elements of **ord** is the equality in **ord** and has not the meaning of $=_{\text{Ord}}$. Nevertheless, after having shown that the relations and the laws of **ord** descend to the quotient **Ord**, the statements with the symbol $=$ will also work for the symbol $=_{\text{Ord}}$.

## 3.4 Finite ordinals, bounded ordinals

We start with a few properties of $\emptyset$.

**Fact 3.8.** Let $m$ be an integer $\ge 1$, $\alpha, \beta^1, \dots, \beta^m \in \text{ord}$, and $\gamma \in \text{ord}^*$. We have

1. $\emptyset \le \beta^1, \dots, \beta^m$;

2. $\emptyset < \gamma, \beta^2, \dots, \beta^m$;

3. $\alpha < \underbrace{\emptyset, \dots, \emptyset}_{m \text{ times}}$ is impossible.

*Proof.* This is straightforward from the definitions. $\square$

*Remark 3.9.* Axiom 15 will be valid in **Ord** because every element of **ord** is given either as $\emptyset$ or as an element $\gamma \in \text{ord}^*$, so that always $\emptyset < \gamma$ by Item 2 of Fact 3.8. $\diamond$

**Fact 3.10.** Let $m, n \in \mathbb{N}$. Then

1. $m \le n$ if and only if $\underline{m} \le \underline{n}$;

2. $m < n$ if and only if $\underline{m} < \underline{n}$;

3. $\underline{m} \le \underline{n}$ and $\underline{n} < \underline{m}$ are incompatible.

*Proof.* Concerning the direct implications in 1 and 2, we write $n = m+r$ and we do an induction on $r$. For the reverse implications, cases $m = 0$ and $n = 0$ are already known. Next, we see that $\underline{m}+1 \le \underline{n}+1$ implies $\underline{m} \le \underline{n}$, and that $\underline{m}+1 < \underline{n}+1$ implies $\underline{m} < \underline{n}$. This allows us to conclude by induction on $m$.

Item 3 follows from Items 1 and 2. $\square$
(here $\iota_j : I_j \to K$ is the injective map from $I_j$ to the disjoint union of the $I_j$'s).

We shall write $\sup(\alpha^j)_{j \in [1..r]} = \sup(\alpha^1, \dots, \alpha^r)$.

2. The sup of a finite family in **ord** is defined in the following way.

$$ \sup(\alpha^1, \dots, \alpha^r) \stackrel{\text{def}}{=} \begin{cases} \underline{0} & \text{if } \alpha^1 = \dots = \alpha^r = \underline{0} \\ \text{the sup of the } \alpha^k \in \mathbf{ord}^* \text{ otherwise.} \end{cases} $$

We note that Item 2 is formally included in Item 1 if we adopt the convention $\mathfrak{In}_0 = \mathbb{N}_0$. However, this convention would not allow us to define an arbitrary $\mathfrak{F}$-indexed sup in **ord**.

### 3.3 Definition of $\leq$ and of $<$

The main job remains to be done, i.e. to define two binary relations $\leq$ and $<$ on **ord** with the required properties, viz.

* the relation "$\alpha \leq \beta$ and $\beta \leq \alpha$" has to be an equivalence relation (we shall denote by **Ord** the quotient set);

* the relations $\leq$ and $<$ and the maps sup and s have to descend to the quotient (we shall not change their names);

* with these maps and relations, **Ord** has to be an $\mathfrak{F}$-order.

Moreover, since the maps s: $\text{Fam}(\mathfrak{F}, \mathbf{ord}) \to \mathbf{ord}^*$ is defined before the map sup: $\text{Fam}(\mathfrak{F}, \mathbf{ord}^*) \to \mathbf{ord}^*$, we have to verify in our construction that Proposition and definition 2.6 is satisfied in **Ord**. This will be a consequence of Fact 3.11 below.

For our job, we define inductively two asymmetric relations between, on the left side, an element of **ord** and, on the right side, a nonempty finitely enumerated set of elements of **ord**, written as a list:

$$ \alpha \leq \beta^1, \dots, \beta^m \quad \text{and} \quad \alpha < \beta^1, \dots, \beta^m \quad (m \geq 1) $$

#### Conventions.

* The letters $\alpha, \beta, \gamma, \varepsilon$, possibly with exponents, indices or primes, are used for elements of **ord**.

* If $\alpha$ is an element of **ord** and if $F$ is a finite list, possibly empty, in $\text{In}_\alpha$, we denote by $\alpha_F$ the list of the $\alpha_i$'s with $i$ in $F$.

The two relations are defined by simultaneous induction in the following way.
An element $\alpha \in \mathbf{ord}$ is said to be *finite* if $\alpha = \mathbf{Ord} \underline{m}$ for an $m \in \mathbb{N}$, *bounded* if $\alpha \le \underline{m}$ for an $m \in \mathbb{N}$. Bounded ordinals are much more complicated than finite ordinals (see Examples 3.17 and 3.18).

In Section 3.7, we shall discuss what the relations $\le$ and $<$ on the set $\mathbf{ord}_\mathfrak{F}$ become in classical mathematics.

## 3.5 First consequences

The following fact shows that the sup law will satisfy the characteristic property given in Axiom 13 when we shall know that it descends to the quotient Ord.

**Fact 3.11 (sdef).** We have $\alpha \le \beta$ if and only if $\alpha_i < \beta$ for all $i \in \text{In}_\alpha$.

*Proof.* This property is tautological: this is the definition of $\alpha \le \beta$.

☐

Similarly, the following fact shows that the sup law will satisfy the characteristic property given in Axiom 13 when we shall know that it descends to the quotient Ord.

**Fact 3.12 (supdef).** Let $(\alpha^j)_{j \in J}$ be a family in $\mathbf{ord}^*$ with $J \in \mathfrak{F}$, $\gamma = \sup(\alpha^j)_{j \in J}$, and $\beta \in \mathbf{ord}$. We have $\gamma \le \beta$ if and only if $\alpha^j \le \beta$ for all $j \in J$. In particular, $\sup(\alpha, \beta) \le \beta$ if and only if $\alpha \le \beta$.

N.B.: The result is equally true for the sup of a finite family in $\mathbf{ord}$.

*Proof.* This is another linguistic tautology. We have $\alpha^j = \text{s}((\alpha^j)_i)_{i \in I_j}$ for an $I_j \in \mathfrak{F}$. By the definition of $\gamma$ and of $\le$, the inequality $\gamma \le \beta$ means that for each $j \in J$ and each $i \in I_j$ we have $(\alpha^j)_i < \beta$, i.e. that for each $j \in J$ we have $\alpha^j \le \beta$. ☐

☐

The following fact shows that Axioms 8 and 9 will be valid when we shall descend to the quotient Ord.

**Fact 3.13.** 1. **ax8.** We have $\alpha < \text{s}(\beta)$ if and only if $\alpha \le \beta$.

2. **ax9.** We have $\beta < \alpha$ if and only if $\text{s}(\beta) \le \alpha$.

*Proof.* Recall that the element $\gamma = \text{s}(\beta)$ is defined by $\text{In}_\gamma = \{0\}$ and $\gamma_0 = \beta$.

1. By definition, $\alpha < \gamma$ means that $\alpha \le \gamma_F$ for a nonempty list $F \subseteq_f \{0\}$. This forces $F = [0]$ and $\gamma_F = \beta$.

2. By definition, $\gamma \le \alpha$ means that $\gamma_0 < \alpha$, i.e. $\beta < \alpha$.

Thus, better than equivalences, these are tautologies.

☐

The following fact will allow us to shorten certain proofs by induction.

**Fact 3.14.** a. We have an inequality $\alpha \le \beta$ if and only if for each $i \in \text{In}_\alpha$, there exists a nonempty $F_i \subseteq_f \text{In}_\beta$ such that $\alpha_i \le \beta_{F_i}$.

b. We have an inequality $\alpha < \beta$ if and only if there exists a nonempty $F \subseteq_f \text{In}_\beta$ such that for each $i \in \text{In}_\alpha$ we have $\alpha_i < \beta_F$.

*Proof.* Straightforward from the definitions.

☐

Now we leave behind tautological proofs and turn to inductive proofs.
Particular cases involving $\underline{0}$ are avoided by using the convention $\text{In}_{\underline{0}} = \mathbb{N}_0$.

$\alpha \le \beta^1, \dots, \beta^m (m \ge 1)$ is defined as $\alpha_i < \beta^1, \dots, \beta^m$ for all $i \in \text{In}_\alpha$.

$\alpha < \beta^1, \dots, \beta^m (m \ge 1)$ is defined as there are $F_1 \subseteq_f \text{In}_{\beta^1}, \dots, F_m \subseteq_f \text{In}_{\beta^m}$ not all empty with $\alpha \le \beta^1_{F_1}, \dots, \beta^m_{F_m}$.

This definition is correct since elements of **ord** are inductively defined and the pair of clauses is inductive.

Without the convention that $\text{In}_{\underline{0}} = \mathbb{N}_0$, we would have had to include Fact 3.8 below in the definition. This convention is a little miracle allowing us to avoid a case-by-case reasoning with respect to the disjunction "$\alpha = \underline{0}$ or $\alpha \in \text{ord}^*$" in the proofs.

The meaning of the two relations is $\alpha \le \sup(\beta^1, \dots, \beta^m)$ and $\alpha < \sup(\beta^1, \dots, \beta^m)$.

**Lemma 3.7.** We have $\alpha < \beta^1, \dots, \beta^m$ if and only if $\alpha < \sup(\beta^1, \dots, \beta^m)$. Similarly, we have $\alpha \le \beta^1, \dots, \beta^m$ if and only if $\alpha \le \sup(\beta^1, \dots, \beta^m)$.

*Proof.* Let us write

$\alpha < \beta^1, \dots, \beta^m$ for $\alpha < \sup(\beta^1, \dots, \beta^m)$,

$\alpha \le \beta^1, \dots, \beta^m$ for $\alpha \le \sup(\beta^1, \dots, \beta^m)$.

Let $\varepsilon = \sup(\beta^1, \dots, \beta^m)$. Then $\alpha < \beta^1, \dots, \beta^m$ if and only if $\alpha \le \varepsilon_F$ with $F$ a nonempty finitely enumerated subset of the disjoint union $K$ of the $\text{In}_{\beta^j}$'s and $\varepsilon_k = (\beta^j)_i$ if $k$ is the image of $i$ in $K$; letting $F_j = F \cap \text{In}_{\beta^j}$, not all $F_j$ are empty and this may be rewritten as $\alpha \le \beta^1_{F_1}, \dots, \beta^m_{F_m}$. This holds if and only if $\alpha < \beta^1, \dots, \beta^m$.

We have $\alpha \le \beta^1, \dots, \beta^m$ if and only if, for all $i \in \text{In}_\alpha$, $\alpha_i < \varepsilon$, i.e. $\alpha_i < \beta^1, \dots, \beta^m$, i.e. $\alpha_i < \beta^1, \dots, \beta^m$; this holds if and only if $\alpha \le \beta^1, \dots, \beta^m$. $\square$

The relation $\alpha =_{\text{Ord}} \beta$ is defined as meaning "$\alpha \le \beta$ and $\beta \le \alpha$".

We shall show in Section 4 that the relation $\cdot =_{\text{Ord}}$ is an equivalence relation and we shall define the set **Ord** as the quotient of **ord** by this relation.

Let us note that until Theorem 4.8, the symbol $=$ between two elements of **ord** is the equality in **ord** and has not the meaning of $=_{\text{Ord}}$. Nevertheless, after having shown that the relations and the laws of **ord** descend to the quotient **Ord**, the statements with the symbol $=$ will also work for the symbol $=_{\text{Ord}}$.

## 3.4 Finite ordinals, bounded ordinals

We start with a few properties of $\underline{0}$.
**Fact 3.15.** • **weakening.** If $\alpha \le \beta^1, \dots, \beta^m$, then for each $\beta$ we have $\alpha \le \beta, \beta^1, \dots, \beta^m$.

• **contraction.** If $\alpha \le \beta^1, \beta^1, \beta^2, \dots, \beta^m$ then $\alpha \le \beta^1, \beta^2, \dots, \beta^m$.

• The same properties hold with $<$ instead of $\le$.

*Proof.* Use induction applying the definitions. $\square$

The following lemma is a corollary of Fact 3.14. Item 1 (resp. 2) will imply that the $s$ (resp. sup) map descends to the quotient in **Ord** (resp. **Ord**\*). Item 3 will imply that the relations $\le$ and $=$ are reflexive in **Ord**; Items 5 and 7 will imply Axioms 3 and 14 for **Ord**.

**Lemma 3.16.** 1. **s0.** Let $\alpha, \beta \in \mathbf{ord}$ with $\mathrm{In}_\alpha = \mathrm{In}_\beta$ and $\alpha_i \le \beta_i$ for all $i \in \mathrm{In}_\alpha$. Then $\alpha \le \beta$.

2. **sup0.** Let $\alpha, \beta \in \mathbf{ord}^*$ with $\mathrm{In}_\alpha = \mathrm{In}_\beta$ and $\alpha_i \le \beta_i$ for all $i \in \mathrm{In}_\alpha$. Then

$$ \sup(\alpha_i)_{i \in \mathrm{In}_\alpha} \le \sup(\beta_i)_{i \in \mathrm{In}_\beta}. $$

The result works also for the sup of a finite family in **ord**.

3. **rfl.** For all $\alpha \in \mathbf{ord}$, we have $\alpha \le \alpha$. A fortiori, $\alpha \le \alpha, \beta^1, \dots, \beta^m$.

4. **s1.** For all $\alpha \in \mathbf{ord}^*$ and all $i \in \mathrm{In}_\alpha$, we have $\alpha_i < \alpha$. A fortiori, $\alpha_i < \alpha, \beta^1, \dots, \beta^m$.

5. **irfl.** For all $\alpha \in \mathbf{ord}$, $\alpha < \alpha$ is impossible.

6. $\alpha < s(\alpha)$.

7. **ax14.** If $\gamma < \beta$ for all $\gamma < \alpha$, then $\alpha \le \beta$.

*Proof.* 1. Straightforward from Fact 3.14a. We take $F = \{i\}$.

2. Let $\gamma = \sup(\alpha_i)_{i \in \mathrm{In}_\alpha}$ and $\epsilon = \sup(\beta_i)_{i \in \mathrm{In}_\beta}$. By Fact 3.14a, for each $j \in \mathrm{In}_{\alpha_i}$ there exists a nonempty $F_{i,j} \subseteq_f \mathrm{In}_{\beta_i}$ with $(\alpha_i)_j \le (\beta_i)_{F_{i,j}}$; $F_{i,j}$ is a fortiori in the disjoint union of the $\mathrm{In}_{\beta_i}$'s, so that $(\alpha_i)_j < \epsilon$ by definition of $\epsilon$. By definition, $\alpha_i \le \epsilon$, so that by Fact 3.12 $\gamma \le \epsilon$.

3. By induction: we use Fact 3.14a, we take $F = \{i\}$ and $\alpha \le \alpha$ reduces to $\alpha_i \le \alpha_i$.

4. By induction: we use Fact 3.14b, we take $F = \{i\}$ and $\alpha_i < \alpha$ reduces to $(\alpha_i)_j < \alpha_i$.

5. By induction: we use Fact 3.14b, we take $F = \{i\}$ and "$\alpha < \alpha$ is impossible" reduces to: "$\alpha_i < \alpha_i$ is impossible".

6. Apply **s1** to $\beta = s(\alpha)$.

7. If $\alpha = \emptyset$, the conclusion is clear. If $\alpha = s(\alpha_i)_{i \in I}$, as $\alpha_i < \alpha$ for each $i \in \mathrm{In}_\alpha$ (Item 4), the hypothesis that $\gamma < \beta$ for all $\gamma < \alpha$ shows that $\alpha_i < \beta$ for all $i \in \mathrm{In}_\alpha$. We conclude by Fact 3.11 that $\alpha \le \beta$. $\square$

## 3.6 Ordinals and limited principles of omniscience

*Example 3.17.* Let $(v_n)_{n \in \mathbb{N}}$ be a sequence in $\{0, 1\}$ which takes at most once the value 1. The lesser limited principle of omniscience **LLPO** says that we have

$$ \exists k \in \{0, 1\} \ \forall n \ (v_n = 1 \Rightarrow n \equiv k \ \mathrm{mod} \ 2). \quad (*) $$

From such a sequence $(v_n)_{n \in \mathbb{N}}$ let us define $\epsilon$, $\epsilon^1$ and $\epsilon^2 \in \mathbf{ord}$ in the following way:

$$ \epsilon = s(\underline{v_n})_{n \in \mathbb{N}}, \quad \epsilon^1 = s(\underline{v_{2m}})_{m \in \mathbb{N}}, \quad \epsilon^2 = s(\underline{v_{2m+1}})_{m \in \mathbb{N}}. $$

Then we have $\epsilon \le \sup(\epsilon^1, \epsilon^2)$. But $\epsilon \le \epsilon^1$ gives $k = 0$ in (*) and $\epsilon \le \epsilon^2$ gives $k = 1$ in (*).

Thus, the disjunction $\epsilon \le \epsilon^1$ or $\epsilon \le \epsilon^2$ has no constructive proof: assuming the disjunction for an arbitrary $(v_n)$ would imply **LLPO**.
**Fact 3.8.** Let $m$ be an integer $\ge 1$, $\alpha, \beta^1, \dots, \beta^m \in \mathbf{ord}$, and $\gamma \in \mathbf{ord}^*$. We have

1. $\underline{0} \le \beta^1, \dots, \beta^m$;

2. $\underline{0} < \gamma, \beta^2, \dots, \beta^m$;

3. $\alpha < \underbrace{\underline{0}, \dots, \underline{0}}_{m \text{ times}}$ is impossible.

*Proof.* This is straightforward from the definitions. $\square$

*Remark 3.9.* Axiom 15 will be valid in **Ord** because every element of **ord** is given either as $\underline{0}$ or as an element $\gamma \in \mathbf{ord}^*$, so that always $\underline{0} < \gamma$ by Item 2 of Fact 3.8.
$\diamond$

**Fact 3.10.** Let $m, n \in \mathbb{N}$. Then

1. $m \le n$ if and only if $\underline{m} \le \underline{n}$;

2. $m < n$ if and only if $\underline{m} < \underline{n}$;

3. $\underline{m} \le \underline{n}$ and $\underline{n} < \underline{m}$ are incompatible.

*Proof.* Concerning the direct implications in 1 and 2, we write $n = m + r$ and we do an induction on $r$. For the reverse implications, cases $m = 0$ and $n = 0$ are already known. Next we see that $\underline{m} + \underline{1} \le \underline{n} + \underline{1}$ implies $\underline{m} \le \underline{n}$, and that $\underline{m} + \underline{1} < \underline{n} + \underline{1}$ implies $\underline{m} < \underline{n}$. This allows us to conclude by induction on $m$. Item 3 follows from items 1 and 2.
$\square$

An element $\alpha \in \mathbf{ord}$ is said to be *finite* if $\alpha =_{\mathbf{Ord}} \underline{m}$ for an $m \in \mathbb{N}$, *bounded* if $\alpha \le \underline{m}$ for an $m \in \mathbb{N}$. Bounded ordinals are much more complicated than finite ordinals (see Examples 3.17 and 3.18).

In Section 3.7, we shall discuss what the relations $\le$ and $<$ on the set $\mathbf{ord}_\beta$ become in classical mathematics.

**3.5 First consequences**

The following fact shows that the law will satisfy the characteristic property given in Proposition and definition 2.6 when we shall know that it descends to the quotient **Ord**.

**Fact 3.11 (sdef).** We have $\alpha \le \beta$ if and only if $\alpha_i < \beta$ for all $i \in \text{In}_\alpha$.

*Proof.* This property is tautological: this is the definition of $\alpha \le \beta$. $\square$

Similarly, the following fact shows that the sup law will satisfy the characteristic property given in Axiom 13 when we shall know that it descends to the quotient **Ord**.
**Example 3.18.** Let $(u_n)_{n \in \mathbb{N}}$ be a nondecreasing sequence in $\{0, 1\}$. The limited principle of omniscience **LPO** says that such a sequence is eventually constant:

$$ \exists n \in \mathbb{N} \ \forall m \in \mathbb{N} \ u_m \le u_n. \quad (*) $$

From such a sequence $(u_n)_{n \in \mathbb{N}}$ let us define $\alpha$ and $\beta \in \mathbf{ord}$ in the following way:

$$ \alpha = s(\underline{u_n})_{n \in \mathbb{N}}, \quad \beta = s(\underline{u_n + 1})_{n \in \mathbb{N}}. $$

We note that the strict inequality $\alpha < \beta$ is equivalent (using Facts 3.10 and 3.14 and Lemma 3.7) to

$$ \exists n \in \mathbb{N} \ \forall m \in \mathbb{N} \ u_m < u_n + 1, $$

which amounts to $(*)$. In fact, $\alpha$ hesitates between 1 and 2, $\beta$ hesitates between 2 and 3, and the inequality $\alpha < \beta$ is valid if we assume **LPO**. But asserting $\alpha < \beta$ for all sequences $(u_n)$ implies **LPO** in constructive mathematics. Here we see that hesitating between 1 and 2 for an infinite sequence has the same flavour as hesitating (in a classical setting) between bounded and unbounded for an infinite sequence of natural numbers: adding 1 to each term of the sequence increases strictly the sup only if the sequence is bounded.

## 3.7 In classical mathematics

Proposition 3.19 shows that the law of excluded middle (**LEM**) simplifies and/or obscures dramatically the structure of the set $\mathbf{ord}_{\mathfrak{F}}$ with respect to the relations $<$ and $\le$.

**Proposition 3.19.** Assume **LEM**. Then for $\alpha, \beta \in \mathbf{ord}$, we have $\alpha \le \beta$ or $\beta < \alpha$. Moreover, if $\beta < \alpha$, there exists an $i \in \text{In}_\alpha$ such that $\beta \le \alpha_i$.

*Proof.* We prove by simultaneous induction the two following properties.

$$ \text{"$\alpha \le \beta$ or $\beta < \alpha$" and "$\beta \le \alpha$ or $\alpha < \beta$".} $$

By induction hypothesis, we have for all $i \in \text{In}_\alpha$ and all $j \in \text{In}_\beta$, "$\alpha \le \beta_j$ or $\beta_j < \alpha$", and also "$\beta \le \alpha_i$ or $\alpha_i < \beta$".

The first disjunction implies by **LEM** that either $\beta_j < \alpha$ for all $j \in \text{In}_\beta$ or there is $j \in \text{In}_\beta$ such that $\alpha \le \beta_j$. In the first case, we have $\beta \le \alpha$ by definition of $\cdot \le \dots$. In the second case, we have $\alpha < \beta$ by definition of $\cdot < \dots$, with for $F \subseteq_f \text{In}_\beta$ the list $[j]$. The symmetric reasoning yields the second disjunction. $\square$

N.B.: For countable ordinals, the limited principle of omniscience (**LPO**) suffices to prove the proposition.

**Corollary 3.20.** Assume **LEM**. Any ordinal $\alpha \neq \emptyset$ is either an immediate successor or the sup of the ordinals $\gamma < \alpha$.

*Proof.* Consider $\alpha = s(\alpha_i)_{i \in \text{In}_\alpha}$ and compare $\alpha$ with $\sup(\alpha_i)_{i \in \text{In}_\alpha}$. The details are left to the reader. $\square$

**Corollary 3.21.** Assume **LEM**. Any bounded ordinal is finite.

*Proof.* Left to the reader: use Fact 3.13. $\square$

# 4 Fundamental results

## 4.1 Ord$_{\mathfrak{F}}$ is an initial object in the category of $\mathfrak{F}$-orders

**Lemma 4.1.** For $\alpha^1, \dots, \alpha^r$ in $\mathbf{ord}$ ($r \ge 1$), we have

$$ \sup(\alpha^j)_{j \in \llbracket 1..r \rrbracket} < s(\alpha^j)_{j \in \llbracket 1..r \rrbracket}. $$
**Fact 3.12 (supdef).** Let $(\alpha^j)_{j \in J}$ be a family in ord* with $J \in \mathfrak{F}$, $\gamma = \sup(\alpha^j)_{j \in J}$, and $\beta \in \text{ord}$.

We have $\gamma \le \beta$ if and only if $\alpha^j \le \beta$ for all $j \in J$. In particular, $\sup(\alpha, \beta) \le \beta$ if and only if $\alpha \le \beta$.

N.b.: the result is equally true for the sup of a finite family in ord.

*Proof.* This is another linguistic tautology. We have $\alpha^j = s((\alpha^j)_i)_{i \in I_j}$ for an $I_j \in \mathfrak{F}$. By the definition of $\gamma$ and of $\le$, the inequality $\gamma \le \beta$ means that for each $j \in J$ and each $i \in I_j$ we have $(\alpha^j)_i < \beta$, i.e. that for each $j \in J$ we have $\alpha^j \le \beta$. $\square$

The following fact shows that Axioms **8** and **9** will be valid when we shall descend to the quotient Ord.

**Fact 3.13.** **1. ax8.** We have $\alpha < s(\beta)$ if and only if $\alpha \le \beta$.

**2. ax9.** We have $\beta < \alpha$ if and only if $s(\beta) \le \alpha$

*Proof.* Recall that the element $\gamma = s(\beta)$ is defined by $\text{In}_{\gamma} = \{0\}$ and $\gamma_0 = \beta$.

1. By definition, $\alpha < \gamma$ means that $\alpha \le \gamma_F$ for a nonempty list $F \subseteq_f \{0\}$. This forces $F = [0]$ and $\gamma_F = \beta$.

2. By definition, $\gamma \le \alpha$ means that $\gamma_0 < \alpha$, i.e. $\beta < \alpha$.

Thus, better than equivalences, these are tautologies. $\square$

The following fact will allow us to shorten certain proofs by induction.

**Fact 3.14.**

a. We have an inequality $\alpha \le \beta$ if and only if for each $i \in \text{In}_\alpha$, there exists a nonempty $F_i \subseteq_f \text{In}_\beta$ such that $\alpha_i \le \beta_{F_i}$.

b. We have an inequality $\alpha < \beta$ if and only if there exists a nonempty $F \subseteq_f \text{In}_\beta$ such that for each $i \in \text{In}_\alpha$ we have $\alpha_i < \beta_F$.

*Proof.* Straightforward from the definitions. $\square$

Now we leave behind tautological proofs and turn to inductive proofs.
*Proof.* Let us show e.g. that $\epsilon = \sup(\alpha, \beta) < \gamma = \text{s}(\alpha, \beta)$. We have $\text{In}_\epsilon = \text{In}_\alpha + \text{In}_\beta$, with $\epsilon_k = \alpha_i$ if $\iota_1(i) = k$, and $\epsilon_k = \beta_j$ if $\iota_2(j) = k$. We have $\text{In}_\gamma = \{1,2\}$ with $\gamma_1 = \alpha$ and $\gamma_2 = \beta$. We apply Fact 3.14b with $F = \{1,2\}$. For an arbitrary $k$ in $\text{In}_\epsilon$, we have $\epsilon_k < \alpha, \beta$ since $\epsilon_k$ is $\alpha_i$ or $\beta_j$ and, by **S1**, we have $\alpha_i < \alpha$ (a fortiori $\alpha_i < \alpha, \beta$) and $\beta_j < \beta$ (a fortiori $\beta_j < \alpha, \beta$). $\square$

Let us note that the preceding proof relies on the fact that the definitions of $\leqslant$ and $<$ have been given with lists on the right-hand side.

**Lemma 4.2 (transitivities).** 1. **trans1.** If $\alpha \leqslant \beta^1, \dots, \beta^m$ and, for each $j \in [1..m]$, $\beta^j \leqslant \gamma^1, \dots, \gamma^r$, then $\alpha \leqslant \gamma^1, \dots, \gamma^r$.

2. **trans2.** If $\alpha < \beta^1, \dots, \beta^m$ and, for each $j \in [1..m]$, $\beta^j \leqslant \gamma^1, \dots, \gamma^r$, then $\alpha < \gamma^1, \dots, \gamma^r$.

3. **trans3.** If $\alpha \leqslant \beta^1, \dots, \beta^m$ and, for each $j \in [1..m]$, $\beta^j < \gamma^1, \dots, \gamma^r$, then $\alpha < \gamma^1, \dots, \gamma^r$.

As particular cases, Axioms 5 to 7 will be valid when we shall descend to the quotient **Ord**:

* if $\alpha \leqslant \beta$ and $\beta \leqslant \gamma$ then $\alpha \leqslant \gamma$;

* if $\alpha < \beta$ and $\beta \leqslant \gamma$ then $\alpha < \gamma$;

* if $\alpha \leqslant \beta$ and $\beta < \gamma$ then $\alpha < \gamma$.

*Proof.* The three transitivities are being proved by simultaneous induction.

In order to prove **trans1**, we note that the hypothesis means that we have $\alpha_i < \beta^1, \dots, \beta^m$ for all $i \in \text{In}_\alpha$. Let us fix such an $i$. We use **trans2** with this $\alpha_i$ instead of $\alpha$ and we get $\alpha_i < \gamma^1, \dots, \gamma^r$. Since this works for all $i \in \text{In}_\alpha$, this gives the desired conclusion $\alpha \leqslant \gamma^1, \dots, \gamma^r$.

In order to prove **trans2**, we note that the hypothesis implies that there are $G_j \subseteq_f \text{In}_{\beta j}$ not all empty such that $\alpha \leqslant \beta_{G_1}^1, \dots, \beta_{G_m}^m$. We have also for $j \in [1..m]$ and for all $h \in \text{In}_{\beta j}$, $\beta_h^j < \gamma^1, \dots, \gamma^r$. A fortiori, this is true for the $h$'s $\in G_j$. We use **trans3** with these $\beta_h^j$'s instead of the $\beta^j$'s. This gives the desired conclusion $\alpha < \gamma^1, \dots, \gamma^r$.

In order to prove **trans3**, we note that the hypothesis implies (by weakening) that there are $F_k \subseteq_f \text{In}_{\gamma k}$ not all empty such that $\beta^j \leqslant \gamma_{F_1}^1, \dots, \gamma_{F_r}^r$ for $j \in [1..m]$. This time we use **trans1** with the $\gamma_\ell^k$'s instead of the $\gamma^k$'s and we deduce that $\alpha \leqslant \gamma_{F_1}^1, \dots, \gamma_{F_r}^r$, which implies $\alpha < \gamma^1, \dots, \gamma^r$. $\square$

The following lemma shows that when descending to the quotient, Axiom 4 will be valid in **Ord**.

**Lemma 4.3 (ax4).** Let $\alpha, \beta^1, \dots, \beta^m \in \text{ord}$. If $\alpha < \beta^1, \dots, \beta^m$, then $\alpha \leqslant \beta^1, \dots, \beta^m$.

*Proof.* Proof by induction on $\alpha$. We have $\alpha < \beta^1, \dots, \beta^m$ if and only if we can find $F_k \subseteq_f \text{In}_{\beta^k}$ not all empty such that, for each $i \in \text{In}_\alpha$, we have $\alpha_i \leqslant \beta_{F_1}^1, \dots, \beta_{F_m}^m$. Let us fix an $i \in \text{In}_\alpha$. For $j \in F_k$, we have $\beta_j^k < \beta^k$, and by weakening $\beta_j^k < \beta^1, \dots, \beta^m$. By **trans3**, we get $\alpha_i < \beta^1, \dots, \beta^m$. Finally, since this is true for all $i \in \text{In}_\alpha$, we have $\alpha \leqslant \beta^1, \dots, \beta^m$. $\square$

The following fact shows that Axiom 10 will be valid when we shall descend to the quotient **Ord**.

**Lemma 4.4 (ax10).** If $\alpha < \gamma$ and $\beta < \gamma$, then $\text{sup}(\alpha, \beta) < \gamma$.

*Proof.* By definition, we have $\text{s}(\alpha, \beta) \leqslant \gamma$. Lemma 4.1 gives $\text{sup}(\alpha, \beta) < \text{s}(\alpha, \beta)$. By transitivity, we get $\text{sup}(\alpha, \beta) < \gamma$. $\square$

**Lemma 4.5.** Let $n$ be a positive integer and $\alpha^1, \dots, \alpha^n \in \text{ord}$. It is impossible that, for each $i \in [1..n]$, we have $\alpha^i < \alpha^1, \dots, \alpha^n$.
**Fact 3.15.**

* weakening. If $\alpha \le \beta^1, \dots, \beta^m$, then for each $\beta$ we have $\alpha \le \beta, \beta^1, \dots, \beta^m$.

* contraction. If $\alpha \le \beta^1, \beta^1, \beta^2, \dots, \beta^m$ then $\alpha \le \beta^1, \beta^2, \dots, \beta^m$.

* The same properties hold with $<$ instead of $\le$.

*Proof.* Use induction applying the definitions. □

The following lemma is a corollary of Fact 3.14. Item 1 (resp. 2) will imply that the $s$ (resp. $\sup$) map descends to the quotient in $\mathbf{Ord}$ (resp. $\mathbf{Ord}^*$). Item 3 will imply that the relations $\le$ and $=$ are reflexive in $\mathbf{Ord}$; Items 5 and 7 will imply Axioms 3 and 14 for $\mathbf{Ord}$.

**Lemma 3.16.**

1. s0. Let $\alpha, \beta \in \mathbf{ord}$ with $\mathrm{In}_\alpha = \mathrm{In}_\beta$ and $\alpha_i \le \beta_i$ for all $i \in \mathrm{In}_\alpha$. Then $\alpha \le \beta$.

2. sup0. Let $\alpha, \beta \in \mathbf{ord}^*$ with $\mathrm{In}_\alpha = \mathrm{In}_\beta$ and $\alpha_i \le \beta_i$ for all $i \in \mathrm{In}_\alpha$. Then

$$ \sup(\alpha_i)_{i \in \mathrm{In}_\alpha} \le \sup(\beta_i)_{i \in \mathrm{In}_\beta}. $$

The result works also for the sup of a finite family in ord.

3. rfl. For all $\alpha \in \mathbf{ord}$, we have $\alpha \le \alpha$. A fortiori, $\alpha \le \alpha, \beta^1, \dots, \beta^m$.

4. s1. For all $\alpha \in \mathbf{ord}^*$ and all $i \in \mathrm{In}_\alpha$, we have $\alpha_i < \alpha$. A fortiori, $\alpha_i < \alpha, \beta^1, \dots, \beta^m$.

5. irfl. For all $\alpha \in \mathbf{ord}$, $\alpha < \alpha$ is impossible.

6. $\alpha < s(\alpha)$.

7. ax14. If $\gamma < \beta$ for all $\gamma < \alpha$, then $\alpha \le \beta$.

*Proof.* 1. Straightforward from Fact 3.14a. We take $F = \{i\}$.

2. Let $\gamma = \sup(\alpha_i)_{i \in \mathrm{In}_\alpha}$ and $\epsilon = \sup(\beta_i)_{i \in \mathrm{In}_\beta}$. By Fact 3.14a, for each $j \in \mathrm{In}_{\alpha_i}$ there exists a nonempty $F_{i,j} \subseteq_f \mathrm{In}_{\beta_i}$ with $(\alpha_i)_j \le (\beta_i)_{F_{i,j}}$; $F_{i,j}$ is a fortiori in the disjoint union of the $\mathrm{In}_{\beta_i}$'s, so that $(\alpha_i)_j < \epsilon$ by definition of $\epsilon$. By definition, $\alpha_i \le \epsilon$, so that by Fact 3.12 $\gamma \le \epsilon$.

3. By induction: we use Fact 3.14a, we take $F = \{i\}$ and $\alpha \le \alpha$ reduces to $\alpha_i \le \alpha_i$.

4. By induction: we use Fact 3.14b, we take $F = \{i\}$ and $\alpha_i < \alpha$ reduces to $(\alpha_i)_j < \alpha_i$.

5. By induction: we use Fact 3.14b, we take $F = \{i\}$ and "$\alpha < \alpha$ is impossible" reduces to: "$\alpha_i < \alpha_i$ is impossible".
**Proof.** By induction. Using weakening, the hypothesis to be proven impossible gives finite lists

$$F_1 \subseteq_f \mathrm{In}_{\alpha_1}, \dots, F_n \subseteq_f \mathrm{In}_{\alpha_n},$$

not all empty, such that

$$\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n \text{ for } i \in [1..m].$$

In particular, for $j \in F_i$ (if $F_i$ is nonempty), we have

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_n}^n.$$

This reduces to the hypothesis with the nonempty list $\alpha_{F_1}^1, \dots, \alpha_{F_n}^n$ instead of the list $\alpha^1, \dots, \alpha^n$. $\square$

**Lemma 4.6.** Let $\alpha^1, \dots, \alpha^n, \beta^1, \dots, \beta^m \in \mathrm{ord} (n, m \ge 1)$.

1. If $\alpha^i < \alpha^1, \dots, \alpha^n, \beta^1, \dots, \beta^m$ for $i \in [1..n]$, then $\alpha^i < \beta^1, \dots, \beta^m$ for each $i$.

2. Let $F_1 \subseteq_f \mathrm{In}_{\alpha_1}, \dots, F_n \subseteq_f \mathrm{In}_{\alpha_n}$. If $\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m$ for $i \in [1..n]$, then $\alpha^i \le \beta^1, \dots, \beta^m$ for each $i$.

**Proof.** 1. The hypothesis yields finite lists

$$F_1 \subseteq_f \mathrm{In}_{\alpha^1}, \dots, F_n \subseteq_f \mathrm{In}_{\alpha^n}, G_1 \subseteq_f \mathrm{In}_{\beta^1}, \dots, G_m \subseteq_f \mathrm{In}_{\beta^m},$$

not all empty, such that

$$\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m \text{ for } i \in [1..n]. \quad (*)$$

Thus we have for $i \in [1..n]$ and $j \in \mathrm{In}_{\alpha^i}$

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m.$$

Let us fix $i$ and $j$: a fortiori, with $F'_i = F_i \cup \{j\}$

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F'_i}^i, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m.$$

We have also by weakening, for $k \in [1..n]$ and $\ell \in F_k$

$$\alpha_{\ell}^k < \alpha_{F_1}^1, \dots, \alpha_{F'_i}^i, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m.$$

Thus by induction $\alpha_j^i < \beta_{G_1}^1, \dots, \beta_{G_m}^m$. Since $j$ is arbitrary, we get $\alpha^i \le \beta_{G_1}^1, \dots, \beta_{G_m}^m$. This gives the desired conclusion, $\alpha^i < \beta^1, \dots, \beta^m$, if at least one list $G_k$ is nonempty, for an arbitrary $i \in [1..n]$. If this is not the case, (*) yields $\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n$ for $i \in [1..n]$, with lists $F_i$ not all empty. By definition, this implies $\alpha^i < \alpha^1, \dots, \alpha^n$ for $i \in [1..n]$, which is impossible by Lemma 4.5.

2. We have for $i \in [1..n]$ and $j \in \mathrm{In}_{\alpha^i}$

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m.$$

Let us fix $i$ and $j$: a fortiori, with $F'_i = F_i \cup \{j\}$,

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F'_i}^i, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m.$$

We have also by weakening, for $k \in [1..n]$ and $\ell \in F_k$

$$\alpha_{\ell}^k < \alpha_{F_1}^1, \dots, \alpha_{F'_i}^i, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m.$$

Item 1 then yields $\alpha_j^i < \beta^1, \dots, \beta^m$. As $j$ is arbitrary, we get what we want: $\alpha^i \le \beta^1, \dots, \beta^m$ for an arbitrary $i \in [1..n]$. $\square$
6. Apply s1 to $\beta = s(\alpha)$.

7. If $\alpha = \emptyset$, the conclusion is clear. If $\alpha = s(\alpha_i)_{i \in I}$, as $\alpha_i < \alpha$ for each $i \in \text{In}_\alpha$ (Item 4), the hypothesis that $\gamma < \beta$ for all $\gamma < \alpha$ shows that $\alpha_i < \beta$ for all $i \in \text{In}_\alpha$. We conclude by Fact 3.11 that $\alpha \le \beta$. $\square$

## 3.6 Ordinals and limited principles of omniscience

*Example 3.17.* Let $(v_n)_{n \in \mathbb{N}}$ be a sequence in $\{0, 1\}$ which takes at most once the value 1. The lesser limited principle of omniscience **LLPO** says that we have

$$ \exists k \in \{0, 1\} \ \forall n \ (v_n = 1 \Rightarrow n \equiv k \ \text{mod } 2). \quad (*) $$

From such a sequence $(v_n)_{n \in \mathbb{N}}$ let us define $\varepsilon$, $\varepsilon^1$ and $\varepsilon^2 \in \text{ord}$ in the following way:

$$ \varepsilon = s(v_n)_{n \in \mathbb{N}}, \quad \varepsilon^1 = s(v_{2m})_{m \in \mathbb{N}}, \quad \varepsilon^2 = s(v_{2m+1})_{m \in \mathbb{N}}. $$

Then we have $\varepsilon \le \sup(\varepsilon^1, \varepsilon^2)$. But $\varepsilon \le \varepsilon^1$ gives $k = 0$ in (*) and $\varepsilon \le \varepsilon^2$ gives $k = 1$ in (*). Thus, the disjunction $\varepsilon \le \varepsilon^1$ or $\varepsilon \le \varepsilon^2$ has no constructive proof: assuming the disjunction for an arbitrary $(v_n)$ would imply **LLPO**.

*Example 3.18.* Let $(u_n)_{n \in \mathbb{N}}$ be a nondecreasing sequence in $\{0, 1\}$. The limited principle of omniscience **LPO** says that such a sequence is eventually constant:

$$ \exists n \in \mathbb{N} \ \forall m \in \mathbb{N}, \ u_m \le u_n. \quad (*) $$

From such a sequence $(u_n)_{n \in \mathbb{N}}$ let us define $\varepsilon$ and $\varepsilon' \in \text{ord}$ in the following way:

$$ \varepsilon = s(u_n)_{n \in \mathbb{N}}, \quad \varepsilon' = s(u_n + 1)_{n \in \mathbb{N}}. $$

We notice that the strict inequality $\varepsilon < \varepsilon'$ is equivalent (using Facts 3.10 and 3.14 and Lemma 3.7) to

$$ \exists n \in \mathbb{N} \ \forall m \in \mathbb{N}, \ u_m < u_n + 1, $$

which is the same thing as (*). In fact, $\varepsilon$ hesitates between 1 and 2, $\varepsilon'$ hesitates between 2 and 3, and the inequality $\varepsilon < \varepsilon'$ is valid if we assume **LPO**. But asserting $\varepsilon < \varepsilon'$ for all sequences $(u_n)$ implies **LPO** in constructive mathematics. Here we see that hesitating between 1 and 2 for an infinite sequence has the same flavour as hesitating (in a classical setting) between bounded and unbounded for an infinite sequence of natural numbers: adding 1 to each term of the sequence increases strictly the sup only if the sequence is bounded.

## 3.7 In classical mathematics

Proposition 3.19 shows that the law of excluded middle (**LEM**) simplifies and/or obscures dramatically the structure of the set $\text{ord}_\beta$ with respect to the relations $<$ and $\le$.
**Proposition 3.19.** Assume LEM. Then for $\alpha, \beta \in \text{ord}$, we have $\alpha \le \beta$ or $\beta < \alpha$. Moreover, if $\beta < \alpha$, there exists an $i \in \text{In}_\alpha$ such that $\beta \le \alpha_i$.

*Proof.* We prove by simultaneous induction the two following properties.

“$\alpha \le \beta$ or $\beta < \alpha$” and “$\beta \le \alpha$ or $\alpha < \beta$”.

By induction hypothesis, we have for all $i \in \text{In}_\alpha$ and all $j \in \text{In}_\beta$, “$\alpha \le \beta_j$ or $\beta_j < \alpha$”, and also “$\beta \le \alpha_i$ or $\alpha_i < \beta$”.

The first disjunction implies by LEM that either $\beta_j < \alpha$ for all $j \in \text{In}_\beta$ or there is $j \in \text{In}_\beta$ such that $\alpha \le \beta_j$. In the first case, we have $\beta \le \alpha$ by definition of $\cdot \le \dots$. In the second case, we have $\alpha < \beta$ by definition of $\cdot < \dots$, with for $F \subseteq_f \text{In}_\beta$ the list $[j]$.

The symmetric reasoning yields the second disjunction.

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

N.b.: for countable ordinals, the limited principle of omniscience (LPO) suffices to prove the proposition.

**Corollary 3.20.** Assume LEM. Any ordinal $\alpha \ne \emptyset$ is either an immediate successor or the sup of the ordinals $\gamma < \alpha$.

*Proof.* Consider $\alpha = \text{s}(\alpha_i)_{i \in \text{In}_\alpha}$ and compare $\alpha$ with $\sup(\alpha_i)_{i \in \text{In}_\alpha}$. The details are left to the reader.

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

**Corollary 3.21.** Assume LEM. Any bounded ordinal is finite.

*Proof.* Left to the reader: use Fact 3.13.

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

# 4 Fundamental results

## 4.1 Ord$_\mathfrak{F}$ is an initial object in the category of $\mathfrak{F}$-orders

**Lemma 4.1.** For $\alpha^1, \dots, \alpha^r$ in ord ($r \ge 1$), we have

$$ \sup(\alpha^j)_{j \in [1..r]} < \text{s}(\alpha^j)_{j \in [1..r]}. $$

*Proof.* Let us show e.g. that $\epsilon = \sup(\alpha, \beta) < \gamma = \text{s}(\alpha, \beta)$. We have $\text{In}_\epsilon = \text{In}_\alpha + \text{In}_\beta$, with $\epsilon_k = \alpha_i$ if $\iota_1(i) = k$, and $\epsilon_k = \beta_j$ if $\iota_2(j) = k$. We have $\text{In}_\gamma = \{1, 2\}$ with $\gamma_1 = \alpha$ and $\gamma_2 = \beta$. We apply Fact 3.14b with $F = \{1, 2\}$. For an arbitrary $k$ in $\text{In}_\epsilon$, we have $\epsilon_k < \alpha, \beta$ since $\epsilon_k$ is $\alpha_i$ or $\beta_j$ and, by s1, we have $\alpha_i < \alpha$ (a fortiori $\alpha_i < \alpha, \beta$) and $\beta_j < \beta$ (a fortiori $\beta_j < \alpha, \beta$).

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

Let us note that the preceding proof relies on the fact that the definitions of $\le$ and $<$ have been given with lists on the right hand side.

**Lemma 4.2 (transitivities).** 1. trans1. If $\alpha \le \beta^1, \dots, \beta^m$ and, for each $j \in [1..m]$, $\beta^j \le \gamma^1, \dots, \gamma^r$, then $\alpha \le \gamma^1, \dots, \gamma^r$.
## 4.3 Elementary ordinal arithmetic

### (Sequential) addition

The sequential addition $\alpha + \beta$ ($\alpha$ followed by $\beta$: addition is not commutative) is defined by induction on $\beta$:

$$ \alpha + \underline{0} = \alpha \quad \text{and} \quad \alpha + \beta = s(\alpha + \beta_j)_{j \in \text{In}_\beta} \quad \text{if} \quad \beta = s(\beta_j)_{j \in \text{In}_\beta} \in \text{ord}^*. $$

The formula for $\alpha + \beta$ works only in the case $\text{In}_\beta \neq \text{N}_0$ (it would yield $\alpha + \underline{0} = \underline{0}$). We also have $\alpha + \beta = \sup((\alpha + \beta_j) + \underline{1})_{j \in \text{In}_\beta}$ if $\text{In}_\beta \neq \text{N}_0$.

The following properties can be proved by induction:

* if $\alpha \le \alpha'$ and $\beta \le \beta'$, then $\alpha + \beta \le \alpha' + \beta'$;

* $(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma)$;

* $\alpha + \underline{0} = \underline{0} + \alpha = \alpha$;

* $\alpha + \beta \le \alpha + \gamma$ if and only if $\beta \le \gamma$;

* $\alpha + \beta < \alpha + \gamma$ if and only if $\beta < \gamma$;

* $\alpha = \underline{1} + \alpha$ if and only if $\omega \le \alpha$;

* if $\alpha \le \gamma$, then there is $\beta$ such that $\gamma = \alpha + \beta$;

* if $\alpha < \gamma$, then there is $\beta \ne \underline{0}$ such that $\gamma = \alpha + \beta$.

### Sequential sum

Let $J \in \mathfrak{F}$ and consider a well-founded linear order relation $\prec$ on $J$ with a detachable minimal element $0_J$. Let $(\beta^j)_{j \in J}$ be an element of $\text{Fam}(J, \text{ord})$. The $\prec$-indexed sequential sum $\sum_{j \prec \ell} \beta^j$ is defined by induction on $\ell \in (J, \prec)$:

$$ \sum_{j \prec 0_J} \beta^j = 0_J \quad \text{and} \quad \sum_{j \prec \ell} \beta^j = \sup \left( \left( \sum_{j \prec k} \beta^j \right) + \beta^k \right)_{k \prec \ell} \quad \text{if } 0_J \prec \ell. $$

We show by induction on $\prec$ that, given two families $(\beta^j)_{j \in J}$ and $(\gamma^j)_{j \in J}$ such that $\beta^j \le \gamma^j$ for all $j \in J$, we have $\sum_{j \prec \ell} \beta^j \le \sum_{j \prec \ell} \gamma^j$ for all $\ell \in J$. This construction descends therefore to the quotient $\text{Ord}$.

**Remark 4.15.** This construction allows us to define a map $\text{ord}_2^{\text{Br}} \to \text{ord}_2$, where $\text{ord}_2^{\text{Br}}$ is the set of names of Brouwer ordinals. See Troelstra (1969) and Brouwer (1918, 1926). Troelstra only treats countable Brouwer ordinals.

### Multiplication

We define $\alpha \cdot \beta$ by induction on $\beta \in \text{ord}$:

$$ \alpha \cdot \underline{0} = \underline{0} \quad \text{and} \quad \alpha \cdot \beta = \sup(\alpha \cdot \beta_j + \alpha)_{j \in \text{In}_\beta} \quad \text{if} \quad \beta = s(\beta_j)_{j \in \text{In}_\beta} \in \text{ord}^*. $$

The following properties can be proved by induction:

* if $\alpha \le \alpha'$ and $\beta \le \beta'$, then $\alpha \cdot \beta \le \alpha' \cdot \beta'$;

* $(\alpha \cdot \beta) \cdot \gamma = \alpha \cdot (\beta \cdot \gamma)$;

* $\alpha \cdot \underline{1} = \underline{1} \cdot \alpha = \alpha$;

* $\alpha \cdot (\beta + \gamma) = (\alpha \cdot \beta) + (\alpha \cdot \gamma)$;

* if $\underline{1} \le \alpha$, then $\alpha \cdot \beta \le \alpha \cdot \gamma$ if and only if $\beta \le \gamma$;

* if $\underline{1} \le \alpha$, then $\alpha \cdot \beta < \alpha \cdot \gamma$ if and only if $\beta < \gamma$.
2. trans2. If $\alpha < \beta^1, \dots, \beta^m$ and, for each $j \in [1..m]$, $\beta^j \le \gamma^1, \dots, \gamma^r$, then $\alpha < \gamma^1, \dots, \gamma^r$.

3. trans3. If $\alpha \le \beta^1, \dots, \beta^m$ and, for each $j \in [1..m]$, $\beta^j < \gamma^1, \dots, \gamma^r$, then $\alpha < \gamma^1, \dots, \gamma^r$.

As particular cases, Axioms 5 to 7 will be valid when we shall descend to the quotient Ord:

* if $\alpha \le \beta$ and $\beta \le \gamma$ then $\alpha \le \gamma$;

* if $\alpha < \beta$ and $\beta \le \gamma$ then $\alpha < \gamma$;

* if $\alpha \le \beta$ and $\beta < \gamma$ then $\alpha < \gamma$.

*Proof.* The three transitivities are being proved by simultaneous induction.

In order to prove trans1, we note that the hypothesis means that we have $\alpha_i < \beta^1, \dots, \beta^m$ for all $i \in \text{In}_\alpha$. Let us fix such an $i$. We use trans2 with this $\alpha_i$ instead of $\alpha$ and we get $\alpha_i < \gamma^1, \dots, \gamma^r$. Since this works for all $i \in \text{In}_\alpha$, this gives the desired conclusion $\alpha \le \gamma^1, \dots, \gamma^r$.

In order to prove trans2, we note that the hypothesis implies that there are $G_j \subseteq_f \text{In}_{\beta j}$ not all empty such that $\alpha \le \beta_{G_1}^1, \dots, \beta_{G_m}^m$. We have also for $j \in [1..m]$ and for all $h \in \text{In}_{\beta j}$, $\beta_h^j < \gamma^1, \dots, \gamma^r$. A fortiori, this is true for the $h$'s $\in G_j$. We use trans3 with these $\beta_h^j$'s instead of the $\beta^j$'s. This gives the desired conclusion $\alpha < \gamma^1, \dots, \gamma^r$.

In order to prove trans3, we note that the hypothesis implies (by weakening) that there are $F_k \subseteq_f \text{In}_{\gamma^k}$ not all empty such that $\beta^j \le \gamma_{F_1}^1, \dots, \gamma_{F_r}^r$ for $j \in [1..m]$. This time we use trans1 with the $\gamma^k$'s instead of the $\gamma^k$'s and we deduce that $\alpha \le \gamma_{F_1}^1, \dots, \gamma_{F_r}^r$, which implies $\alpha < \gamma^1, \dots, \gamma^r$. $\square$

The following lemma shows that when descending to the quotient, Axiom 4 will be valid in Ord.

**Lemma 4.3 (ax4).** Let $\alpha, \beta^1, \dots, \beta^m \in \text{ord}$. If $\alpha < \beta^1, \dots, \beta^m$, then $\alpha \le \beta^1, \dots, \beta^m$.

*Proof.* Proof by induction on $\alpha$. We have $\alpha < \beta^1, \dots, \beta^m$ if and only if we can find $F_k \subseteq_f \text{In}_{\beta^k}$ not all empty such that, for each $i \in \text{In}_\alpha$, we have $\alpha_i \le \beta_{F_1}^1, \dots, \beta_{F_m}^m$. Let us fix an $i \in \text{In}_\alpha$. For $j \in F_k$, we have $\beta_j^k < \beta^k$, and by weakening $\beta_j^k < \beta^1, \dots, \beta^m$. By trans3, we get $\alpha_i < \beta^1, \dots, \beta^m$. Finally, since this is true for all $i \in \text{In}_\alpha$, we have $\alpha \le \beta^1, \dots, \beta^m$. $\square$

The following fact shows that Axiom 10 will be valid when we shall descend to the quotient Ord.
## Exponentiation

We define $\alpha^\beta$ by induction on $\beta \in \mathbf{ord}$, as follows:

$$ \alpha^0 = \underline{1} \quad \text{and} \quad \alpha^\beta = \sup(\alpha^{\beta_j} \cdot \alpha)_{j \in \mathbf{In}_\beta} \quad \text{if} \quad \beta = s(\beta_j)_{j \in \mathbf{In}_\beta} \in \mathbf{ord}^*. $$

## Ackermann

It is possible to continue this elementary arithmetic à la Ackermann as in Finsler 1951. We define by induction an ordinal $\underline{Ack}(\alpha, \beta, \gamma)$ that we get by iterating $\gamma$ times the preceding map, initialised at $\alpha$, i.e. more precisely

$$ \begin{align*} \underline{Ack}(\alpha, \beta, \underline{0}) &= \alpha + \beta \\ \underline{Ack}(\alpha, \underline{0}, \gamma) &= \alpha \quad \text{if } \gamma \in \mathbf{ord}^* \\ \underline{Ack}(\alpha, \beta, \gamma) &= \sup(\sup(\underline{Ack}(\alpha, \beta_j, \gamma), \alpha, \gamma_k))_{j \in \mathbf{In}_\beta} \quad \begin{array}{l} k \in \mathbf{In}_\gamma \\ \text{if } \beta = s(\beta_j)_{j \in \mathbf{In}_\beta} \text{ and } \gamma = s(\gamma_k)_{k \in \mathbf{In}_\gamma}. \end{array} \end{align*} $$

In particular, $\varepsilon_0 = \underline{Ack}(\omega, \omega, \underline{4})$.

# 5 Countable ordinals

## 5.1 First steps

As previously indicated, we get countable ordinals when we choose as set of index sets

$$ \mathfrak{F}_2 = \{ \mathbb{N}_k | k \in \mathbb{N}, k \ge 0 \} \cup \{ \mathbb{N} \} $$

with convenient operations for the set of finite subsets of an $I \in \mathfrak{F}_2$ and for disjoint unions. We write $\mathbf{ord}_2$ and $\mathbf{Ord}_2$ for $\mathbf{ord}_{\mathfrak{F}_2}$ and $\mathbf{Ord}_{\mathfrak{F}_2}$. Thus $\mathbf{Ord}_2$ is the set of ordinals of the second class and $\mathbf{ord}_2$ is a set of names for elements of $\mathbf{Ord}_2$.

**Lemma 5.1.** Any countable ordinal is the $s$ of a nondecreasing sequence of countable ordinals.

*Proof.* This is Lemma 4.14. □

**Proposition 5.2.** Assume LPO. Then, for $\alpha, \beta \in \mathbf{Ord}$, we have $\alpha \le \beta$ or $\beta < \alpha$.

*Proof.* Proceed as for Proposition 3.19, in the countable case. □

## 5.2 Comparison with Martin-Löf ordinals

We present a variation of the theory of ordinals in the book Notes on Constructive Mathematics (Martin-Löf 1970, Chapter 3). We write “variation” since Martin-Löf’s theory is formulated in the framework of Markov’s recursive mathematics, while we take as primitive intuitionistic logic with generalised inductive definitions, as does the work Heyting 1961 (the fact that this setting can provide a more elegant treatment than the one in recursive mathematics is stressed in Kreisel’s review (1963) of this work).

### 5.2.1 Martin-Löf’s formal system

In this system, ordinals are described inductively: if we have a finite or infinite sequence of ordinals $\sigma = \sigma_0, \dots, \sigma_n, \dots$ (maybe empty), then $s(\sigma)$ is an ordinal.

The (classical) semantics of this operation is the following: to $(\sigma_n)$ sequence of ordinals we associate the supremum of the sequence of the successors of the $\sigma_n$'s.

In particular, $\underline{0}$ is defined as $s(\sigma)$, where $\sigma$ is the empty sequence.

We write simply $s(\alpha)$ for $s(\sigma)$, where $\sigma$ is the sequence with one element $\sigma_0 = \alpha$.

In constructive mathematics, the set of all such ordinals is an example of a nondiscrete set.
**Lemma 4.4 (ax10).** If $\alpha < \gamma$ and $\beta < \gamma$, then $\sup(\alpha, \beta) < \gamma$.

*Proof.* By definition, we have $s(\alpha, \beta) \leq \gamma$. Lemma 4.1 gives $\sup(\alpha, \beta) < s(\alpha, \beta)$. By transitivity, we get $\sup(\alpha, \beta) < \gamma$. $\square$

**Lemma 4.5.** Let $n$ be a positive integer and $\alpha^1, \dots, \alpha^n \in \text{ord}$. It is impossible that, for each $i \in [1..n]$, we have $\alpha^i < \alpha^1, \dots, \alpha^n$.

*Proof.* By induction. Using weakening, the hypothesis to be proven impossible gives finite lists

$$F_1 \subseteq_f \text{In}_{\alpha_1}, \dots, F_n \subseteq_f \text{In}_{\alpha_n},$$

not all empty, such that

$$\alpha^i \leq \alpha_{F_1}^1, \dots, \alpha_{F_n}^n \text{ for } i \in [1..m].$$

In particular for $j \in F_i$ (if $F_i$ is nonempty) we have

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_n}^n.$$

This reduces to the hypothesis with the nonempty list $\alpha_{F_1}^1, \dots, \alpha_{F_n}^n$ instead of the list $\alpha^1, \dots, \alpha^n$. $\square$

**Lemma 4.6.** Let $\alpha^1, \dots, \alpha^n, \beta^1, \dots, \beta^m \in \text{ord} (n, m \geq 1)$.

1. If $\alpha^i < \alpha^1, \dots, \alpha^n, \beta^1, \dots, \beta^m$ for $i \in [1..n]$, then $\alpha^i < \beta^1, \dots, \beta^m$ for each $i$.

2. Let $F_1 \subseteq_f \text{In}_{\alpha_1}, \dots, F_n \subseteq_f \text{In}_{\alpha_n}$. If $\alpha^i \leq \alpha_{F_1}^1, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m$ for $i \in [1..n]$, then $\alpha^i \leq \beta^1, \dots, \beta^m$ for each $i$.

*Proof.* 1. The hypothesis yields finite lists

$$F_1 \subseteq_f \text{In}_{\alpha^1}, \dots, F_n \subseteq_f \text{In}_{\alpha^n}, G_1 \subseteq_f \text{In}_{\beta^1}, \dots, G_m \subseteq_f \text{In}_{\beta^m},$$

not all empty, such that

$$\alpha^i \leq \alpha_{F_1}^1, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m \text{ for } i \in [1..n]. \quad (*)$$

Thus we have for $i \in [1..n]$ and $j \in \text{In}_{\alpha^i}$

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m.$$

Let us fix $i$ and $j$: a fortiori, with $F'_i = F_i \cup \{j\}$

$$\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m.$$
As stated in the introduction, to any ordinal $\alpha$ we associate, by induction on $\alpha$, a tree $\text{Tree}(\alpha)$: $\text{Tree}(\alpha)$ always contains the empty sequence, and $\text{Tree}(s(\sigma))$ contains $n \sim \ell$ if $\ell$ is in $\text{Tree}(\sigma_n)$.

This set $\text{Tree}(\alpha)$ does not contain any infinite branch: if $f$ is a numerical function, we can always find $n$ such that $[f(0), \dots, f(n-1)]$ is not in $\text{Tree}(\alpha)$. This is proved directly by induction on $\alpha$. In other words, the tree $\text{Tree}(\alpha)$ is well-founded. The fact that we get in this way all well-founded trees is the content of Brouwer's bar theorem, which holds neither in Bishop's set theory nor in dependent type theory. This follows from the fact that both systems have an interpretation in recursive mathematics, while the bar theorem does not hold in recursive mathematics, as shown by an example due to Kleene (see Kleene and Vesley 1965).

We define next what an atomic formula is: a formula of the form $\alpha < \beta$ or $\alpha \le \beta$.

Finally, we can define when a sequent $\Gamma$ is provable, where $\Gamma$ is a finite set of atomic formulae. The formulation is quite elegant!

$$ \frac{\Gamma, \alpha \le \sigma_n}{\Gamma, \alpha < s(\sigma)} \qquad \frac{\dots \Gamma, \sigma_n < \beta \dots}{\Gamma, s(\sigma) \le \beta} $$

Note that there is a direct proof of $\emptyset \le \beta$ by the second rule.

The intuitive meaning of a sequent is the classical disjunction of the atomic formulae it contains.

Martin-Löf then defines an equivalence relation $\alpha =_{\text{ML}} \beta$ on $\text{ord}_2$ as expressing the fact that the sequents $\alpha \le \beta$ and $\beta \le \alpha$ are valid. The set of Martin-Löf ordinals, denoted by $\text{Ord}_2^{\text{ML}}$, is the quotient of $\text{ord}_2$ by this equivalence relation.

Martin-Löf proves for instance the sequent $\alpha < \beta, \beta \le \alpha$ by induction on $\beta$ and $\alpha$. He also shows that the following rule is admissible by induction on $\alpha$:

$$ \frac{\Gamma, \alpha < \alpha}{\Gamma}, $$

which implies in particular that $\alpha < \alpha$ is not provable.

Let us give an example of such proofs by induction.

**Lemma 5.3.** The sequents $\alpha \le \alpha$ and $\alpha < s(\alpha)$ are provable for all $\alpha$.

*Proof.* We prove $\alpha \le \alpha$ by induction on $\alpha$. If $\alpha = s(\sigma)$, we have to show $\sigma_n < s(\sigma)$ for all $n$, which follows from $\sigma_n \le \sigma_n$, which holds by induction.

It follows that we have $\alpha < s(\alpha)$ by the first derivation rule. $\square$

Martin-Löf also proves the analogue of Theorem 4.9 for $\text{Ord}_2^{\text{ML}}$. But the two statements, for $\text{Ord}_2^{\text{ML}}$ and for our $\text{Ord}_2$, are independent of each other.

### 5.2.2 Comparison with our system

Let us explain now why this definition does not coincide with ours by giving an example of the form $\alpha < \beta$ which is provable in this sequent calculus but implies LPO in our system.

Let us return to Example 3.18: define $\alpha = s(\sigma)$, where $\sigma_n = u_n$ with $(u_n)$ a nondecreasing sequence of 0's and 1's, and $\beta = s(\tau)$, where $\tau_n = s(\sigma_n) = u_n + 1/2$.

**Lemma 5.4.** The sequent $\alpha < \beta$ is provable.

*Proof.* By the first rule, it is enough to show $\alpha < s(\tau), \alpha \le \tau_0$. And for this we have to show $\sigma_n < \tau_0, \alpha < s(\tau)$ for all $n$. We fix $n$ and we show $\sigma_n < \tau_0, \alpha < s(\tau)$.

If we do have $\sigma_n < \tau_0 = s(\sigma_0)$, this is fine. Note that we can test whether or not $\sigma_n < \tau_0$ holds since both $\sigma_n$ and $\tau_0$ are of the form $\emptyset$ or $1/2$ or $1/2$.

Otherwise, we get explicitly $n$ such that $\sigma_n \ge s(\sigma_0)$ and we have then $\sigma_m \le \sigma_n$ and so $\sigma_m < \tau_n$ for all $m$. We can prove $\sigma_n < \tau_0, \alpha < s(\tau)$ by $\sigma_n < \tau_0, \alpha \le \tau_n$ which holds since $\sigma_n < \tau_0, \sigma_m < \tau_n$ holds for all $m$. $\square$
We have also by weakening, for $k \in [1..n]$ and $\ell \in F_k$

$$ \alpha_{\ell}^{k} < \alpha_{F_1}^{1}, \dots, \alpha_{F'_{i}}^{i}, \dots, \alpha_{F_n}^{n}, \beta_{G_1}^{1}, \dots, \beta_{G_m}^{m}. $$

Thus by induction $\alpha_j^i < \beta_{G_1}^1, \dots, \beta_{G_m}^m$. Since $j$ is arbitrary, we get $\alpha^i \le \beta_{G_1}^1, \dots, \beta_{G_m}^m$. This gives the desired conclusion, $\alpha^i < \beta^1, \dots, \beta^m$, if at least one list $G_k$ is nonempty, for an arbitrary $i \in [1..n]$. If this is not the case, (*) yields $\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n$ for $i \in [1..n]$, with lists $F_i$ not all empty. By definition, this implies $\alpha^i < \alpha^1, \dots, \alpha^n$ for $i \in [1..n]$, which is impossible by Lemma 4.5.

2. We have for $i \in [1..n]$ and $j \in \text{In}_{\alpha^i}$

$$ \alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m. $$

Let us fix $i$ and $j$: a fortiori, with $F'_i = F_i \cup \{j\}$,

$$ \alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F'_i}^i, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m. $$

We have also by weakening, for $k \in [1..n]$ and $\ell \in F_k$

$$ \alpha_{\ell}^{k} < \alpha_{F_1}^{1}, \dots, \alpha_{F'_{i}}^{i}, \dots, \alpha_{F_n}^{n}, \beta^{1}, \dots, \beta^{m}. $$

Item 1 then yields $\alpha_j^i < \beta^1, \dots, \beta^m$. As $j$ is arbitrary, we get what we wanted: $\alpha^i \le \beta^1, \dots, \beta^m$ for an arbitrary $i \in [1..n]$. $\square$

The following fact shows that Axioms 11 and 12 will be valid when we shall descend to the quotient Ord.

**Lemma 4.7.**

1. ax11. If $\alpha < \sup(\alpha, \beta)$, then $\alpha < \beta$;

2. ax12. If $\gamma < \alpha$ and $\alpha \le \sup(\beta, \gamma)$, then $\alpha \le \beta$.

*Proof.* 1. Assume $\alpha < \sup(\alpha, \beta)$. Lemma 3.7 gives $\alpha < \alpha, \beta$. Item 1 of Lemma 4.6 gives $\alpha < \beta$.

2. Assume $\gamma < \alpha$ and $\alpha \le \sup(\beta, \gamma)$. The first hypothesis gives $\gamma \le \alpha_F$ for a nonempty $F \subseteq_F \text{In}_\alpha$. The second hypothesis gives $\alpha \le \gamma, \beta$ (by Lemma 3.7). By transitivity we have $\alpha \le \alpha_F, \beta$. Item 2 of Lemma 4.6 gives $\alpha \le \beta$. $\square$

**Theorem 4.8.** We have constructed Ord as an $\mathfrak{F}$-order.

*Proof.* Using *rfl* and *trans1*, we first show that the equality is indeed an equivalence relation, and then that the relation $\le$ descends to the quotient in Ord.

Similarly, *trans2* and *trans3* imply that the relation $<$ descends to the quotient in Ord.
Note that we prove $\alpha < s(\tau)$ by proving $\alpha < s(\tau), \alpha \le \tau_0$, and we have to "keep" $\alpha < s(\tau)$: maybe $\alpha \le \tau_0$ does not hold (it may happen that the sequence $(\sigma_n)$ takes the value $\underline{1}$ and $\tau_0 = \underline{1}$).

In Example 3.18, we note that $\alpha < \beta$ implies **LPO** in our system. Therefore, in the set $\text{Ord}_2^{\text{ML}}$ of Martin-Löf ordinals, the equality is coarser than in the set $\text{Ord}_2$, though both are based on the set $\text{ord}_2$.

## References

Peter Aczel and Michael Rathjen. CST book draft. http://www1.maths.leeds.ac.uk/~rathjen/book.pdf, 2010. E2

Nicolas Bourbaki. *Elements of mathematics: theory of sets*. Hermann, Paris and Addison-Wesley, Reading, 1968. Translated from the French. E2

L. E. J. Brouwer. Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil: allgemeine Mengenlehre. *Verh. Nederl. Akad. Wetensch. Afd. Natuurk. Sect. 1*, 12(5):3–43, 1918. E17

L. E. J. Brouwer. Zur Begründung der intuitionistischen Mathematik. III. *Math. Ann.*, 96:451–488, 1926. http://eudml.org/doc/159181. E2, E17

Alonzo Church. The constructive second number class. *Bull. Amer. Math. Soc.*, 44:224–232, 1938. doi:10.1090/S0002-9904-1938-06720-1. E2

Patrick Dehornoy. *La théorie des ensembles: introduction à une théorie de l'infini et des grands cardinaux*. Tableau Noir, 106. Calvage et Mounet, Paris, 2017. E2

Paul Finsler. Eine transfinite Folge arithmetischer Operationen. *Comment. Math. Helv.*, 25:75–90, 1951. http://eudml.org/doc/139019. E18

Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. *Math. Ann.*, 112:493–565, 1936. http://eudml.org/doc/159839. Translation by M. Szabo: The consistency of elementary number theory, in *Szabo 1969*, pages 132–201. E2

Arend Heyting. Infinitistic methods from a finitist point of view. In *Infinitistic methods: proceedings of the symposium on foundations of mathematics*, Warsaw, 2–9 September 1959, pages 185–192. Pergamon, Oxford and Państwowe Wydawnictwo Naukowe, Warsaw, 1961. E2, E18, E20

Stephen Cole Kleene. On notation for ordinal numbers. *J. Symb. Log.*, 3:150–155, 1938. http://www.jstor.org/stable/2267778. E2

Stephen Cole Kleene and Richard Eugene Vesley. *The foundations of intuitionistic mathematics, especially in relation to recursive functions*. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1965. E19

Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting constructive notions of ordinals in homotopy type theory. In *46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)*, Leibniz International Proceedings in Informationics (LIPIcs), 202, pages 70:1–70:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.MFCS.2021.70. arXiv:2104.02549 contains an appendix with proofs. E2

Georg Kreisel. Review of *Heyting 1961*. *Math. Rev.*, 26, 1963. #2363 (MR0144822), http://mathscinet.ams.org/mathscinet-getitem?mr=144822. E18

Jean-Louis Krivine. *Théorie des ensembles*. Cassini, Paris, 1998. E2

Per Martin-Löf. *Notes on constructive mathematics*. Almqvist & Wiksell, Stockholm, 1970. E1, E2, E4, E18

Ray Mines, Fred Richman, and Wim Ruitenburg. *A course in constructive algebra*. Universitext. Springer, New York, 1988. doi:10.1007/978-1-4419-8640-5. E2

Manfred E. Szabo, editor. *The collected papers of Gerhard Gentzen*. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1969. E20

Anne S. Troelstra. *Principles of intuitionism: lectures presented at the summer conference on Intuitionism and Proof theory (1968) at SUNY at Buffalo, N.Y.* Lecture Notes in Mathematics, vol. 95. Springer, Berlin, 1969. E17

Univalent Foundations Program. *Homotopy type theory: univalent foundations of mathematics*. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013. E2
The sup map descends to the quotient by Lemma 3.16, Item 2.

The unary s map descends to the quotient by Fact 3.13.

It remains to note that Axioms 1 to 15 of $\mathfrak{F}$-orders have been proved above. See, respectively: Lemma 3.16 (Item 3); Fact 3.8 (Item 1); Lemma 3.16 (Item 5); Lemma 4.3; Lemma 4.2; Fact 3.13; Lemma 4.4; Lemma 4.7; Fact 3.12; Lemma 3.16 (Item 7); Remark 3.9. $\square$

The following theorem generalises Fact 3.10.

**Theorem 4.9.** The set $\mathbf{Ord}$ is not reduced to a point. More precisely:

* for all $\alpha, \beta \in \mathbf{Ord}$, $\beta \le \alpha$ and $\alpha < \beta$ are incompatible;

* the map $n \mapsto \underline{n} : \mathbb{N} \to \mathbf{Ord}$ is injective ($m < n$ if and only if $\underline{m} < \underline{n}$).

* for all $\alpha \in \mathbf{Ord}$ and $n > m$ in $\mathbb{N}$, it is impossible that $s^{(n)}(\alpha) =_{\mathbf{Ord}} s^{(m)}(\alpha)$;

*Proof*. The first item is a consequence of *irfl* and of *trans2*. The rest follows. $\square$

**Theorem 4.10.** $\mathbf{Ord}$ is an initial object in the category of $\mathfrak{F}$-orders.

*Sketch of proof.* The structure is purely algebraic and in order to construct $\mathbf{Ord}$, we have only used the axioms of the structure.

In fact, let us consider an object $(E, <_E, \leq_E, 0_E, \sup_E, s_E)$ in the category. Elements of $\mathbf{ord}$ do have their copies in $E$. Furthermore, the relations $\cdot < \dots$ and $\leq \dots$ defined in $\mathbf{ord}$ are valid in $E$ by Fact 2.7 if interpreted in $E$ with finite sup's on the right hand side (as we may by Lemma 3.7). This implies that there is a unique morphism from $\mathbf{Ord}$ to $E$ in the category. $\square$

## 4.2 More properties

**Proposition 4.11.** The binary relation $<$ on $\mathbf{Ord}$ is well-founded.

*Proof*. This is a direct consequence of Fact 3.4. $\square$

**Lemma 4.12** (weak forms of the disjunction "$\alpha \le \beta$ or $\beta < \alpha$") . Let $r \ge 1$ and $\alpha, \beta^1, \dots, \beta^r, \gamma \in \mathbf{ord}$.

1. If $\alpha \le \beta$ and $\beta < \alpha, \gamma^1, \dots, \gamma^r$, then $\beta < \gamma^1, \dots, \gamma^r$.

2. If $\beta < \alpha$ and $\alpha \le \beta, \gamma^1, \dots, \gamma^r$, then $\alpha \le \gamma^1, \dots, \gamma^r$.

*Proof*. Introduce $\gamma = \sup(\gamma^1, \dots, \gamma^r)$. Using Lemma 3.7, both items reduce to already established properties. $\square$

**Definition 4.13.** An element $\beta = s(\beta_i)_{i \in \text{In}_\beta} \in \mathbf{ord}$ is said to be *filtering* if for each $F \subseteq_f \text{In}_\beta$ there exists $j \in \text{In}_\beta$ such that $\sup(\beta_i)_{i \in F} \le \beta_j$.
<figure><img src="image_3.png" /></figure>
**Lemma 4.14.** For each $\alpha \in \text{ord}$, there exists $\beta \in \text{ord}$ such that $\alpha =_{\text{Ord}} \beta$ and $\beta$ is filtering.

*Proof.* If $\alpha = s(\alpha_i)_{i \in J}$, we let $K$ be the set of finitely enumerated subsets of $J$, and for $F \subseteq_f J$ we let $\beta_F = \sup(\alpha_j)_{j \in F}$. Then $\beta =_{\text{Ord}} s(\beta_F)_{F \in K}$. $\square$

## 4.3 Elementary ordinal arithmetic

### (Sequential) addition

The sequential addition $\alpha + \beta$ ($\alpha$ followed by $\beta$: addition is not commutative) is defined by induction on $\beta$:

$$ \alpha + \underline{0} = \alpha \quad \text{and} \quad \alpha + \beta = s(\alpha + \beta_j)_{j \in \text{In}_\beta} \quad \text{if} \quad \beta = s(\beta_j)_{j \in \text{In}_\beta} \in \text{ord}^*. $$

This formula works only for the case $\text{In}_\beta \neq \mathbb{N}_0$: it would yield $\alpha + \underline{0} = \underline{0}$ for $\text{In}_\beta = \mathbb{N}_0$.

We also have $\alpha + \beta = \sup((\alpha + \beta_j) + \underline{1})_{j \in \text{In}_\beta}$ if $\text{In}_\beta \neq \mathbb{N}_0$.

The following properties can be proved by induction:

* if $\alpha \le \alpha'$ and $\beta \le \beta'$, then $\alpha + \beta \le \alpha' + \beta'$;

* $(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma)$;

* $\alpha + \underline{0} = \underline{0} + \alpha = \alpha$;

* $\alpha + \beta \le \alpha + \gamma$ if and only if $\beta \le \gamma$;

* $\alpha + \beta < \alpha + \gamma$ if and only if $\beta < \gamma$;

* $\alpha = \underline{1} + \alpha$ if and only if $\omega \le \alpha$;

* if $\alpha \le \gamma$, then there is $\beta$ such that $\gamma = \alpha + \beta$;

* if $\alpha < \gamma$, then there is $\beta \ne \underline{0}$ such that $\gamma = \alpha + \beta$.

### Sequential sum

Let $J \in \mathfrak{F}$ and consider a well-founded linear order relation $\prec$ on $J$ with a detachable minimal element $0_J$. Let $(\beta^j)_{j \in J}$ be an element of $\text{Fam}(J, \text{ord})$. The $\prec$-indexed sequential sum $\sum_{j<\ell} \beta^j$ is defined by induction on $\ell \in (J, \prec)$:

$$ \sum_{j<0_J} \beta^j = 0_J \quad \text{and} \quad \sum_{j<\ell} \beta^j = \sup\left(\left(\sum_{j<k} \beta^j\right) + \beta^k\right)_{k<\ell} \quad \text{if } 0_J < \ell. $$

We show by induction on $\prec$ that, given two families $(\beta^j)_{j \in J}$ and $(\gamma^j)_{j \in J}$ such that $\beta^j \le \gamma^j$ for all $j \in J$, we have $\sum_{j<\ell} \beta^j \le \sum_{j<\ell} \gamma^j$ for all $\ell \in J$. This construction descends therefore to the quotient $\text{Ord}$.
# Une théorie constructive des ordinaux

Thierry Coquand, Henri Lombardi, Stefan Neuwirth

7 décembre 2024

## Résumé

Martin-Löf (1970) décrit des ordinaux construits de manière récursive. Il donne une version constructivement acceptable des ordinaux calculables de Kleene. En fait, la définition de Turing des fonctions calculables n’est pas nécessaire d’un point de vue constructif. Nous donnons dans cet article une théorie constructive des ordinaux similaire à la théorie de Martin-Löf, mais basée uniquement sur les deux relations «$x \le y$» et «$x < y$», c’est-à-dire sans considérer les séquents dont le sens intuitif est une disjonction classique. Dans notre cadre, l’opération «supremum d’une famille d’ordinaux» joue un rôle important à travers ses interactions avec les relations «$x \le y$» et «$x < y$». Cela permet d’approcher autant que possible la notion d’ordre total lorsque la propriété «$\alpha \le \beta$ ou $\beta \le \alpha$» n’est prouvable qu’en logique classique. Notre objectif est de donner une définition formelle correspondant à l’intuition et de démontrer que nos ordinaux constructifs satisfont de manière constructive toutes les propriétés souhaitables. Notons qu’en ajoutant la logique classique, on retrouverait les ordinaux des mathématiques classiques usuelles, au prix d’une perte de la calculabilité pour la plupart des énoncés donnés sous la forme usuelle.

**Mots clés** : nombre ordinal; mathématiques constructives.

**MSC2020** : 03E10 03F65.

<table><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>1</td><td>Introduction</td><td>F2</td></tr><tr><td>2</td><td>Ensembles presque totalement ordonnés associés à un ensemble d'indexeurs</td><td>F4</td></tr><tr><td>2.1</td><td>Ensemble d'indexeurs</td><td>F5</td></tr><tr><td>2.2</td><td>Les axiomes</td><td>F5</td></tr><tr><td>2.3</td><td>Quelques propriétés</td><td>F6</td></tr><tr><td>3</td><td>Construction inductive d'ensembles d'ordinaux</td><td>F7</td></tr><tr><td>3.1</td><td>Sous-ordinaux</td><td>F8</td></tr><tr><td>3.2</td><td>Définition de la loi sup</td><td>F9</td></tr><tr><td>3.3</td><td>Définitions de $\le$ et $<$</td><td>F9</td></tr><tr><td>3.4</td><td>Ordinaux finis, ordinaux bornés</td><td>F10</td></tr><tr><td>3.5</td><td>Premières conséquences</td><td>F11</td></tr><tr><td>3.6</td><td>Ordinaux et principes d'omniscience limités</td><td>F12</td></tr><tr><td>3.7</td><td>En mathématiques classiques</td><td>F13</td></tr><tr><td>4</td><td>Résultats fondamentaux</td><td>F13</td></tr><tr><td>4.1</td><td>Ord<sub>g</sub> est un objet initial dans la catégorie des g-ordres</td><td>F13</td></tr><tr><td>4.2</td><td>Quelques propriétés supplémentaires</td><td>F16</td></tr><tr><td>4.3</td><td>Arithmétique élémentaire des ordinaux</td><td>F17</td></tr><tr><td>5</td><td>Ordinaux dénombrables</td><td>F18</td></tr><tr><td>5.1</td><td>Premiers pas</td><td>F18</td></tr><tr><td>5.2</td><td>Comparaison avec les ordinaux de Martin-Löf</td><td>F18</td></tr><tr><td>5.2.1</td><td>Le système formel de Martin-Löf</td><td>F18</td></tr><tr><td>5.2.2</td><td>Comparaison avec notre système</td><td>F19</td></tr><tr><td></td><td>Références</td><td>F20</td></tr></tbody></table>
Remark 4.15. This construction allows us to define a map $\mathrm{ord}_2^{\mathrm{Br}} \to \mathrm{ord}_2$, where $\mathrm{ord}_2^{\mathrm{Br}}$ is the set of names of Brouwer ordinals. See Troelstra [1969] and Brouwer [1918, 1926]. Troelstra only treats countable Brouwer ordinals.

## Multiplication

We define $\alpha \cdot \beta$ by induction on $\beta \in \mathrm{ord}$:

$$ \alpha \cdot \underline{0} = \underline{0} \quad \text{and} \quad \alpha \cdot \beta = \sup(\alpha \cdot \beta_j + \alpha)_{j \in \mathrm{In}_{\beta}} \quad \text{if} \quad \beta = \mathrm{s}(\beta_j)_{j \in \mathrm{In}_{\beta}} \in \mathrm{ord}^*. $$

The following properties can be proved by induction:

* if $\alpha \le \alpha'$ and $\beta \le \beta'$, then $\alpha \cdot \beta \le \alpha' \cdot \beta'$;

* $(\alpha \cdot \beta) \cdot \gamma = \alpha \cdot (\beta \cdot \gamma)$;

* $\alpha \cdot \underline{1} = \underline{1} \cdot \alpha = \alpha$;

* $\alpha \cdot (\beta + \gamma) = (\alpha \cdot \beta) + (\alpha \cdot \gamma)$;

* if $\underline{1} \le \alpha$, then $\alpha \cdot \beta \le \alpha \cdot \gamma$ if and only if $\beta \le \gamma$;

* if $\underline{1} \le \alpha$, then $\alpha \cdot \beta < \alpha \cdot \gamma$ if and only if $\beta < \gamma$.

## Exponentiation

We define $\alpha^\beta$ by induction on $\beta \in \mathrm{ord}$:

$$ \alpha^{\underline{0}} = \underline{1} \quad \text{and} \quad \alpha^{\beta} = \sup(\alpha^{\beta_j} \cdot \alpha)_{j \in \mathrm{In}_{\beta}} \quad \text{if} \quad \beta = \mathrm{s}(\beta_j)_{j \in \mathrm{In}_{\beta}} \in \mathrm{ord}^*. $$

## Ackermann

It is possible to continue this elementary arithmetic à la Ackermann. We define by induction an ordinal $\underline{\mathrm{Ack}}(\alpha, \beta, \gamma)$ that we get by iterating $\gamma$ times the preceding map, initialised at $\alpha$, i.e. more precisely,

$$ \underline{\mathrm{Ack}}(\alpha, \beta, \underline{0}) = \alpha + \beta $$

$$ \underline{\mathrm{Ack}}(\alpha, \underline{0}, \gamma) = \alpha \quad \text{if} \quad \gamma \in \mathrm{ord}^* $$

$$ \underline{\mathrm{Ack}}(\alpha, \beta, \gamma) = \sup\left(\sup\left(\sup\left(\underline{\mathrm{Ack}}(\alpha, \underline{\mathrm{Ack}}(\alpha, \beta_j, \gamma), \gamma_k)\right)_{j \in \mathrm{In}_{\beta}}\right)_{k \in \mathrm{In}_{\gamma}}\right) \quad \text{if} \quad \beta = \mathrm{s}(\beta_j)_{j \in \mathrm{In}_{\beta}} \text{ and } \gamma = \mathrm{s}(\gamma_k)_{k \in \mathrm{In}_{\gamma}}. $$

In particular, $\varepsilon_0 = \underline{\mathrm{Ack}}(\omega, \omega, \underline{1})$.
# 1 Introduction

Ce papier est écrit dans le cadre des mathématiques constructives informelles. Nous utilisons la théorie des ensembles de Bishop enrichie par les définitions inductives généralisées (Bishop a utilisé ces sortes de constructions pour la théorie de la mesure, les ensembles boréliens et la théorie de l'intégrale de Lebesgue).

En mathématiques classiques, une définition naturelle d'un ordinal est d'être le type d'ordre d'un ensemble bien ordonné (voir par exemple Bourbaki 1970, III.2.Ex.14). Néanmoins, il est plus pratique d'utiliser les ordinaux de von Neumann, pour lesquels de nombreux résultats peuvent être prouvés sans recourir au choix (voir par exemple Krivine 1998, Chapitre 2 et Dehornoy 2017, Chapitre II).

Proposons maintenant une approche constructive. Une relation binaire $<$ sur un ensemble $X$ est dite bien fondée si pour toute famille d'ensembles $(E_x)_{x \in X}$ indexée par $X$ il est possible de construire des éléments de $\prod_{x \in X} E_x$ par $<$-induction. Précisément, chaque fois que l'on donne une construction $\gamma$ qui à partir d'un élément $a \in X$ et d'un élément $\varphi \in \prod_{x \in X, x<a} E_x$ construit un élément $\gamma(a, \varphi) \in E_a$, il existe un unique $\Phi \in \prod_{x \in X} E_x$ tel que pour tout $a \in X$ nous avons $\Phi(a) = \gamma(a, \Phi|_{a \in X, x<a})$. Cette notion a une signification constructive claire.

En particulier, considérons une propriété pour les éléments de $X$. Si la propriété est $<$-héréditaire, c'est-à-dire si elle est vraie pour $a \in X$ dès qu'elle est vraie pour tout $x \in X$ tel que $x < a$, alors cette propriété est vraie pour tous les éléments de $X$.

En mathématiques constructives, le livre Mines, Richman et Ruitenburg (1988, Section I.6) définit la notion de relation bien fondée d'une manière différente mais équivalente et un ordinal comme un ensemble totalement ordonné pour lequel la relation d'ordre est bien fondée. Ainsi, tous les sous-ensembles de $\mathbb{N}$ sont des ordinaux même si nous ne savons pas s'ils ont un plus petit élément.

L'Univalent Foundations Program (2013, Section 10.3) considère les «ordinaux de Grayson» (voir Mines, Richman et Ruitenburg 1988, Exercise I.6.12) dans le cadre de la théorie homotopique des types univalente; les ordinaux d'un univers donné s'avèrent former un ensemble (et non un grupoïde). Cette théorie des ordinaux diffère de la nôtre en ce qui concerne les axiomes 8 et 9 pour les $\mathfrak{F}$-ordres dans ce qui suit.

Entre autres points de vue constructifs, il existe des descriptions d'ordinaux dénombrables construits par induction dans les ouvrages Brouwer 1926, Gentzen 1936, Church 1938, Kleene 1938, Heyting 1961 et Martin-Löf 1970, Chapitre 3.

Un traitement constructif des ordinaux de von Neumann basé sur la récursion transfinie est donné par Aczel et Rathjen (2010, Section 9.4).

Brouwer propose une construction inductive basée sur l'idée que lorsque les ordinaux $\alpha_n$ sont définis pour tout $n \in \mathbb{N}$ et sont des ensembles bien fondés totalement ordonnés, alors on peut décrire l'ordinal $\alpha$ qui correspond intuitivement à $\alpha_1$ suivi de $\alpha_2$ suivi de $\alpha_3$ suivi de... L'ensemble ordonné $\alpha$ défini par Brouwer sera à nouveau un ensemble bien fondé totalement ordonné. Et si la relation d'ordre sur chaque $\alpha_i$ est décidable, il en va de même pour $\alpha$.

Deux ordinaux de Brouwer ne sont en général pas comparables (en logique intuitionniste) : il n'existe pas de critère général permettant de décider si deux ordinaux ont le même type d'ordre, et, lorsque ce n'est pas le cas, lequel est isomorphe à un segment initial de l'autre.

L'article Kraus, Nordvall Forsberg et Xu 2021 compare trois approches constructives distinctes des ordinaux constructifs, notées Cnf, Brw et Ord, qui sont disponibles dans le cadre de la théorie des types univalente. L'approche Brw est directement inspirée des ordinaux de Brouwer.

Martin-Löf décrit les ordinaux «récursivement construits». Il donne ainsi une version constructivement acceptable des ordinaux dénombrables récursifs tels que définis en mathématiques classiques par Kleene. Intuitivement, un ordinal construit à la Martin-Löf est défini par induction au moyen des deux constructions suivantes :

- on a un ordinal minimum $\emptyset$;

- si $(\alpha_n)_{n \in \mathbb{N}}$ est une suite explicite, finie ou infinie, d'ordinaux, la borne supérieure des $\alpha_n + 1$ est un ordinal<fnref n="1" />.

<footnote n="1">1. D'une manière qui nous semble peu intuitive, Martin-Löf note cette borne supérieure $\sup_{n \in \mathbb{N}}(\alpha_n)$. Cela</footnote>
# 5 Countable ordinals

## 5.1 First steps

As previously indicated, we get countable ordinals when we choose as set of index sets

$$ \mathfrak{F}_2 = \{ \mathbb{N}_k \mid k \in \mathbb{N}, k \ge 0 \} \cup \{ \mathbb{N} \} $$

with convenient operations for the set of finite subsets of an $I \in \mathfrak{F}_2$ and for disjoint unions. We write $\mathbf{ord}_2$ and $\mathbf{Ord}_2$ for $\mathbf{ord}_{\mathfrak{F}_2}$ and $\mathbf{Ord}_{\mathfrak{F}_2}$. Thus $\mathbf{Ord}_2$ is the set of ordinals of the second class and $\mathbf{ord}_2$ is a set of names for elements of $\mathbf{Ord}_2$.

**Lemma 5.1.** Any countable ordinal is the s of a nondecreasing sequence of countable ordinals.

*Proof.* This is Lemma 4.14. □

**Proposition 5.2.** Assume LPO. Then, for $\alpha, \beta \in \mathbf{Ord}$, we have $\alpha \le \beta$ or $\beta < \alpha$. □

*Proof.* Proceed as for Proposition 3.19, in the countable case. □

## 5.2 Comparison with Martin-Löf ordinals

We present a variation of the theory of ordinals in the book *Notes on Constructive Mathematics* [Martin-Löf, 1970, Chapter 3]. We write “variation” since Martin-Löf’s theory is formulated in the framework of Markov’s recursive mathematics, while we take as primitive intuitionistic logic with generalised inductive definitions, as does the work *Heyting* [1961] (the fact that this setting can provide a more elegant treatment than the one in recursive mathematics is stressed in Kreisel’s review of this work).

### 5.2.1 Martin-Löf’s formal system

In this system, ordinals are described inductively: if we have a finite or infinite sequence of ordinals $u = u_0, \dots, u_n, \dots$ (maybe empty), then $s(u)$ is an ordinal.

The (classical) semantics of this operation is the following: to $(\alpha_n)$ sequence of ordinals we associate the supremum of the sequence of the successors of the $\alpha_n$'s.

In particular $\emptyset$ is defined as $s(u)$, where $u$ is the empty sequence.

We write simply $s(a)$ for $s(u)$, where $u$ is the sequence with one element $u_0 = a$.

In constructive mathematics, the set of all such ordinals is an example of a nondiscrete set.

As stated in the introduction, to any ordinal $a$ we associate, by induction on $a$, a tree $\text{Tree}(a)$: $\text{Tree}(a)$ always contains the empty sequence, and $\text{Tree}(s(u))$ contains $n \sim \sigma$ if $\sigma$ is in $\text{Tree}(u_n)$.
Dire que la définition est inductive, c'est dire que tout ordinal est construit en utilisant les règles indiquées.

Dans un cadre constructif, nous pouvons abandonner les machines de Turing et remplacer la calculabilité de Turing par la calculabilité intuitive (non définie). Dans ce cas, la principale différence entre les ordinaux de Brouwer et ceux de Martin-Löf est que les ordinaux de Martin-Löf, étant définis de manière «parallèle» plutôt que de manière «séquentielle», sont plus généraux : pour toute suite d'ordinaux bien définis $(\alpha_n)$ on peut construire le supremum des successeurs des ordinaux $\alpha_n$. Un inconvénient est qu'il n'existe aucun moyen d'associer à un ordinal de Martin-Löf un ensemble bien fondé totalement ordonné avec le même type d'ordre. Par exemple, si les $\alpha_n$ sont tous égaux à $0$ ou $1$, il est à priori impossible de décider si le supremum des successeurs des $\alpha_n$ est égal à $1$ ou $2$.

## Les ordinaux vus comme des arbres

Martin-Löf propose de visualiser un ordinal $\alpha$ comme un arbre bien fondé avec des branchements finis ou dénombrables. L'ordinal $\alpha$ est donné avec un ensemble d'indexeurs noté $\text{In}_\alpha$ ; dans la suite, ce sera un élément de l'ensemble $\mathfrak{F}_2$ constitué de $\mathbb{N}$ et de ses sous-ensembles finis $\mathbb{N}_k$.

- L'arbre avec seulement sa racine représente $0$.

- Si $(t_i)_{i \in \text{In}_\alpha}$ est une famille d'arbres ordinaux pour une famille d'ordinaux $(\alpha_i)_{i \in \text{In}_\alpha}$, le supremum $\alpha = \text{s}(\alpha_i)_{i \in \text{In}_\alpha}$ des successeurs des $\alpha_i$ est donné par l'arbre ordinal pour lequel il y a $\#\text{In}_\alpha$ branches au-dessus de la racine et une copie de $t_i$ est jointe à la branche indexée par $i \in \text{In}_\alpha$.

Considérez les arbres de la figure 1.

Si $n \in \mathbb{N}$, l'ordinal $\underline{n}$ peut être représenté par l'arbre avec $n$ branchements unaires successifs aux $n$ nœuds, de sorte qu'il a $n+1$ nœuds.

Le premier ordinal infini $\omega$ peut être représenté par l'arbre qui a un embranchement dénombrable au-dessus de la racine, les branches portant les arbres précédents (représentant $\underline{n}$, $n \in \mathbb{N}$).

Son successeur, noté $\omega + \underline{1}$, peut être représenté par l'arbre à ramification unaire au-dessus de la racine, la branche portant l'arbre précédent.

L'ordinal $\omega + \underline{2}$ peut être représenté par l'arbre à ramification unaire au-dessus de la racine, la branche portant l'arbre précédent.

L'ordinal $\omega + \omega$ peut être représenté par l'arbre qui a une ramification dénombrable au-dessus de la racine, les branches portant les arbres représentant $\omega + \underline{n}$, $n \in \mathbb{N}$.

<figure><img src="image_4.png" /><figcaption>FIGURE 1 – Arbres ordinaux.</figcaption></figure>

Plus formellement, un tel arbre peut être défini comme l'ensemble de ses nœuds, ou points de branchement, convenablement nommés. On peut considérer l'ensemble $\text{Lst}(\mathbb{N})$ de listes finies d'éléments de $\mathbb{N}$. Soit $n \in \mathbb{N}$ et $\ell, \ell' \in \text{Lst}(\mathbb{N})$. On note $n \sim \ell$ la liste $[n, \ell_1, \dots, \ell_k]$, où $\ell = [\ell_1, \dots, \ell_k]$, $\ell \sim n$ la liste $[\ell_1, \dots, \ell_k, n]$, et $\ell \sim \ell'$ la concaténation des listes $\ell$ et $\ell'$.

<footnote>permet de tenir compte du cas de la suite vide d'ordinaux, qui a pour borne supérieure l'ordinal $0$. Mais hormis ce cas, il s'agit bien de la borne supérieure des successeurs des $\alpha_n$. Nous préfèrerons donc la notation $s_{n \in \mathbb{N}}(\alpha_n)$.</footnote>
This set $\text{Tree}(a)$ does not contain any infinite branch: if $f$ is a numerical function we can always find $n$ such that $[f(0), \dots, f(n-1)]$ is not in $\text{Tree}(a)$. This is proved directly by induction on $a$. In other words, the tree $\text{Tree}(a)$ is well-founded. The fact that we get in this way all well-founded trees is the content of Brouwer's bar theorem, which holds neither in Bishop's set theory nor in dependent type theory. This follows from the fact that both systems have an interpretation in recursive mathematics, while the bar theorem does not hold in recursive mathematics, as shown by an example due to Kleene [Kleene and Vesley, 1965].

We define next what an atomic formula is: a formula of the form $a < b$ or $a \le b$.

Finally, we can define when a sequent $\Gamma$ is provable, where $\Gamma$ is a finite set of atomic formulae. The formulation is quite elegant!

$$ \frac{\Gamma, a \le u_n}{\Gamma, a < s(u)} \qquad \frac{\dots \Gamma, u_n < b \dots}{\Gamma, s(u) \le b} $$

Note that there is a direct proof of $0 \le b$ by the second rule.

The intuitive meaning of a sequent is the classical disjunction of the atomic formulae it contains.

Martin-Löf shows that we can prove for instance $a < b, b \le a$ by induction on $b$ and $a$. He also shows that the following rule is admissible by induction on $a$:

$$ \frac{\Gamma, a < a}{\Gamma} $$

which implies in particular that $a < a$ is not provable.

Let us give an example of such proofs by induction.

**Lemma 5.3.** *The sequents $a \le a$ and $a < s(a)$ are provable for all $a$.*

*Proof.* We prove $a \le a$ by induction on $a$. If $a = s(u)$ we have to show $u_n < s(u)$ for all $n$, which follows from $u_n \le u_n$, which holds by induction.

It follows that we have $a < s(a)$ by the first derivation rule. $\square$

### 5.2.2 Comparison with our system

Let us explain now why this definition does not coincide with ours by giving an example of the form $a < b$ which is provable in this sequent calculus but implies **LPO** in our system.

Let us return to Example 3.18: define $a = s(\underline{a})$, where $u$ is a nondecreasing sequence $(u_n)$ of 0's and 1's, and $b = s(\underline{v})$, where $v$ is the sequence $(v_n)$, $v_n = u_n+1$.

**Lemma 5.4.** $a < b$ is provable.
On remarque que $\text{Lst}(\mathbb{N})$ peut être énuméré de manière naturelle<fnref n="2" /> et que la notion de famille $\mathbb{N}$-indexée dans $\text{Lst}(\mathbb{N})$ correspond, via une telle énumération, à la notion de base (non définie) de fonction de $\mathbb{N}$ dans $\mathbb{N}$.

Un arbre bien fondé avec des branchements finis ou dénombrables peut alors être décrit comme un sous-ensemble détachable $T$ de $\text{Lst}(\mathbb{N})$ qui est construit inductivement selon le processus indiqué précédemment. $T$ est clos par segments initiaux : si $\ell \in \text{Lst}(\mathbb{N})$, $p \in \mathbb{N}$ et $\ell \sim p \in T$, alors $\ell \in T$. Ainsi, à chaque ordinal $\alpha$, nous associons un arbre, défini comme un sous-ensemble approprié de $\text{Lst}(\mathbb{N})$, noté $\text{Tree}(\alpha)$.

Si $n \in \mathbb{N}$, l'ordinal $\underline{n}$ peut être décrit par la suite finie de $n + 1$ listes $[]$, $[0]$, $[0,0]$, ..., $[0, \dots, 0]$.

Le premier ordinal infini $\omega$ peut être décrit par le sous-ensemble de $\text{Lst}(\mathbb{N})$ énuméré par la suite infinie $[]$, $[0]$, $[1]$, $[1,0]$, $[2]$, $[2,0]$, $[2,0,0]$, $[3]$, $[3,0]$, $[3,0,0]$, $[3,0,0,0]$, etc.

L'ordinal $\omega + \underline{1}$ peut être décrit par la suite infinie $[]$, $[0]$, $[0,0]$, $[0,1]$, $[0,1,0]$, $[0,2]$, $[0,2,0]$, $[0,2,0,0]$, $[0,3]$, $[0,3,0]$, $[0,3,0,0]$, $[0,3,0,0,0]$, etc.

L'ordinal $\omega + \underline{2}$ peut être décrit par la suite infinie $[]$, $[0]$, $[0,0]$, $[0,0,0]$, $[0,0,1]$, $[0,0,1,0]$, $[0,0,2]$, $[0,0,2,0]$, $[0,0,2,0,0]$, $[0,0,3]$, $[0,0,3,0]$, $[0,0,3,0,0]$, $[0,0,3,0,0,0]$, etc.

L'ordinal $\omega + \omega$ peut être décrit par la suite doublement infinie $[]$, $[0]$, $[0,0]$, $[0,1]$, $[0,1,0]$, $[0,2]$, $[0,2,0]$, $[0,2,0,0]$, $[0,3]$, $[0,3,0]$, $[0,3,0,0]$, $[0,3,0,0,0]$, etc., $[1]$, $[1,0]$, $[1,0,0]$, $[1,0,1]$, $[1,0,1,0]$, $[1,0,2]$, $[1,0,2,0]$, $[1,0,2,0,0]$, $[1,0,3]$, $[1,0,3,0]$, $[1,0,3,0,0]$, $[1,0,3,0,0,0]$, etc., $[2]$, $[2,0]$, $[2,0,0]$, $[2,0,0,0]$, $[2,0,0,1]$, $[2,0,0,1,0]$, $[2,0,0,2]$, $[2,0,0,2,0]$, $[2,0,0,2,0,0]$, $[2,0,0,3]$, $[2,0,0,3,0]$, $[2,0,0,3,0,0]$, $[2,0,0,3,0,0,0]$, etc., etc.

Ces arbres, vus comme des sous-ensembles définis par induction de $\text{Lst}(\mathbb{N})$, forment un ensemble bien défini dans le contexte des mathématiques constructives intuitives. On peut le noter **ord$_2$** (voir la définition 3.1). Notons que d'un point de vue constructif, **ord$_2$** est un ensemble discret si, et seulement si, le principe de Markov est valide. Cet ensemble **ord$_2$** est un «ensemble des noms d'ordinaux» chez Martin-Löf. Et l'ensemble des ordinaux de Martin-Löf, $\text{Ord}_2^{\text{ML}}$, est un quotient de **ord$_2$** par une relation d'équivalence correctement démontrée. L'ensemble $\text{Ord}_2^{\text{ML}}$ et notre ensemble $\text{Ord}_2$ sont discrets si, et seulement si, le petit principe d'omniscience LPO est valide. Voir la section 5.2 pour plus de précisions.

***

Nous donnons dans cet article une théorie constructive des ordinaux similaire à la théorie de Martin-Löf, mais basée uniquement sur les deux relations «$x \le y$» et «$x < y$», c'est-à-dire sans considérer les séquents dont le sens intuitif est une disjonction classique. Dans notre cadre, l'opération «supremum d'une famille d'ordinaux» joue un rôle important à travers ses interactions avec les relations «$x \le y$» et «$x < y$». Cela permet d'approcher autant que possible la notion d'ordre total lorsque la propriété «$\alpha \le \beta$ ou $\beta \le \alpha$» n'est prouvable qu'en logique classique. Notre objectif est de donner une définition formelle correspondant à l'intuition et de démontrer que nos ordinaux constructifs satisfont de manière constructive toutes les propriétés souhaitables. Notons qu'en ajoutant la logique classique, on retrouverait les ordinaux des mathématiques classiques usuelles, au prix d'une perte de la calculabilité pour la plupart des énoncés donnés sous la forme usuelle.

***

La première étape dans la section 2 est de décrire ces propriétés souhaitables.

## 2 Ensembles presque totalement ordonnés associés à un ensemble d'indexeurs

Nous définissons dans cette section la structure d'ordre (presque) total associée à un ensemble $\mathfrak{F}$ d'indexeurs : la structure de $\mathfrak{F}$-ordre en abrégé.

<footnote n="2">2. Par exemple, pour $\ell = [\ell_1, \dots, \ell_k] \in \text{Lst}(\mathbb{N})$, on pose $\mu(\ell) = \sum_{i=1}^k (\ell_i + 1)$ et on énumère les listes par $\mu(\ell)$ croissants.</footnote>
*Proof.* We have to prove $a < s(v)$.

By the second rule, it is enough to show $a < s(v)$, $a \le v_0$. And for this we have to show $u_n < v_0$, $a < s(v)$ for all $n$. We fix $n$ and we show $u_n < v_0$, $a < s(v)$

If we do have $u_n < v_0 = s(u_0)$ this is fine. Note that we can *test* whether or not $u_n < v_0$ holds or not since both $u_n$ and $v_0$ are of the form 0 or 1 or 2.

Otherwise we get explicitly $n$ such that $u_n \ge s(u_0)$ and we have then $u_m \le u_n$ and so $u_m < v_n$ for all $m$. We can prove $u_n < v_0$, $a < s(v)$ by $u_n < v_0$, $a \le v_n$ which holds since $u_n < v_0$, $u_m < v_n$ holds for all $m$. $\square$

Note that we prove $a < s(v)$ by proving $a < s(v)$, $a \le v_0$, and we have to “keep” $a < s(v)$: maybe $a \le v_0$ does not hold (it may happen that the sequence $(u_n)$ takes the value 1 and $v_0 = 1$).

In Example 3.18, we note that $a < b$ implies **LPO** in our system. Therefore, in the set $\text{Ord}_2^{\text{ML}}$ of Martin-Löf ordinals, the equality is coarser than in the set $\text{Ord}_2$, though both are based on the set $\text{ord}_2$.

## References

* Nicolas Bourbaki. *Elements of mathematics: theory of sets*. Hermann, Paris and Addison-Wesley, Reading, 1968. Translated from the French. 2

* L. E. J. Brouwer. Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil: Allgemeine Mengenlehre. *Verh. Nederl. Akad. Wetensch. Afd. Natuurk, Sect. I*, 12(5):3–43, 1918. 24

* L. E. J. Brouwer. Zur Begründung der intuitionistischen Mathematik. III. *Math. Ann.*, 96:451–488, 1926. https://eudml.org/doc/159181. 3, 24

* Alonzo Church. The constructive second number class. *Bull. Amer. Math. Soc.*, 44(4):224–232, 1938. doi:10.1090/S0002-9904-1938-06720-1. 3

* Patrick Dehornoy. *La théorie des ensembles: introduction à une théorie de l'infini et des grands cardinaux*. Number 106 in Tableau Noir. Calvage et Mounet, Paris, 2017. 2

* Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. *Math. Ann.*, 112:493–565, 1936. http://eudml.org/doc/159839. Translation by M. Szabo: ‘The consistency of elementary number theory’, in Szabo 1969, 132–201. 3

* A. Heyting. Infinitistic methods from a finitist point of view. In *Infinitistic methods: proceedings of the symposium on foundations of mathematics, Warsaw, 2–9 September 1959*, pages 185–192. Pergamon, Oxford and Państwowe Wydawnictwo Naukowe, Warsaw, 1961. Review by G. Kreisel: MR0144822. 3, 25
### 2.1 Ensemble d'indexeurs

Nous avons besoin pour cela d'un ensemble $\mathfrak{F}$ d'indexeurs. Un indexeur sera noté $I, J, K, I'$, $I''$, $J'$, $I_a, I_b$, etc.

Un *indexeur* est simplement un ensemble qui peut servir d'ensemble d'indices pour les familles que l'on va considérer. Dans la suite, un sous-ensemble finiment énuméré de $A$ est toujours un sous-ensemble de $A$ défini à la Bishop par une application $N_k \to A$. Si $A$ est discret, un sous-ensemble finiment énuméré de $A$ est un sous-ensemble détachable.

**Propriétés pour l'ensemble des $\mathfrak{F}$-ordres.** On supposera que

- $\mathbb{N}$ et les ensembles finis $N_k = \{n \in \mathbb{N} | n < k\} (k \ge 0)$ sont des éléments de $\mathfrak{F}$;

- toute partie finiment énumérée d'un élément de $\mathfrak{F}$ est isomorphe<fnref n="3" /> à un élément de $\mathfrak{F}$;

- si $J \in \mathfrak{F}$, l'ensemble des parties finiment énumérées de $J$ est isomorphe à un élément de $\mathfrak{F}$;

- $\mathfrak{F}$ est stable par réunions disjointes indexées dans $\mathfrak{F}$ : on notera $I+J$ une réunion disjointe de $I$ et $J$, et $\sum_{i \in I} J_i$ une réunion disjointe de la famille $(J_i)_{i \in I}$.

Nous considérons les réunions disjointes au sens des sommes directes dans la catégorie des ensembles. Une réunion disjointe $J = \sum_{i \in I} J_i$ est donnée avec une famille d'applications injectives $\iota_\ell: J_\ell \to J$ qui réalisent $J$ comme la somme directe des $J_i$ dans la catégorie des ensembles.

Pour les ordinaux de la seconde classe (les ordinaux dénombrables), on peut prendre pour $\mathfrak{F}$ l'ensemble

$$ \mathfrak{F}_2 = \{ \mathbb{N}_k | k \in \mathbb{N}, k \ge 0 \} \cup \{ \mathbb{N} \} $$

muni d'opérations convenables pour l'ensemble des sous-ensembles finis d'un $I \in \mathfrak{F}$ et pour les réunions disjointes d'éléments de $\mathfrak{F}$ indexés par un élément de $\mathfrak{F}$. Tout autre ensemble d'indexeurs $\mathfrak{F}$ contiendra au moins l'ensemble $\mathfrak{F}_2$ qui sert à définir les ordinaux dénombrables.

Si $E$ est un ensemble, une famille indexée dans $\mathfrak{F}$ d'éléments de $E$ est simplement une famille $(x_i)_{i \in I}$ pour un $I \in \mathfrak{F}$, avec les $x_i \in E$. L'ensemble des familles indexées dans $\mathfrak{F}$ d'éléments de $E$ sera noté $\text{Fam}(\mathfrak{F}, E)$.

Nous utilisons des indices «en bas» uniquement comme ci-dessus pour les ordinaux. Nous utiliserons des indices «en haut» pour tous les autres cas.

### 2.2 Les axiomes

Une structure de $\mathfrak{F}$-ordre sur un ensemble $(E, =)$ est $(E, <, \leq, 0_E, \sup, \text{s}), \text{où}$

- $< \text{ et } \leq \text{ sont des relations binaires définies sur l'ensemble } (E, =);$

- $0_E$ est un élément de $E$; on note $E^* = \{ \alpha \in E | 0_E < \alpha \}$;

- $\sup$ est une fonction de $\text{Fam}(\mathfrak{F}, E^*)$ dans $E^*$ : à partir d'un élément $(\alpha_i)_{i \in I}$ de $\text{Fam}(\mathfrak{F}, E^*)$, elle construit un élément de $E^*$ noté $\alpha = \sup_{i \in I} \alpha_i$;

- $\text{s}$ est une fonction de $E$ vers $E^*$ : à partir d'un élément $\beta \in E$, elle construit un élément de $E^*$ noté $\text{s}(\beta)$, appelé le successeur de $\beta^4$.

**Définition 2.1.** Pour écrire les axiomes avec des sup finis, nous définissons $\sup(\alpha, \beta)$ pour $\alpha, \beta \in E$ comme suit (en utilisant implicitement l'axiome 15) : tout d'abord $\sup(0_E, \alpha) = \alpha = \sup(\alpha, 0_E)$; et si $\alpha, \beta \in E^*$, $\sup(\alpha, \beta)$ est déjà défini.

Ces données doivent vérifier les propriétés suivantes.

**Axiomes pour les $\mathfrak{F}$-ordres.**

1. $\alpha = \beta$ si, et seulement si, $\alpha \leq \beta$ et $\beta \leq \alpha$ (réflexivité et antisymétrie);

2. $0_E \leq \alpha$;

<footnote n="3">3. Dans la catégorie des ensembles.</footnote>

<footnote n="4">4. Nous disons dans ce cas que $s$ est la fonction unaire «successeur». Mais plus loin nous utilisons le même symbole $s$ pour une fonction infinitaire (définition et proposition 2.6).</footnote>
S. C. Kleene. On notation for ordinal numbers. *J. Symb. Log.*, 3:150–155, 1938. https://www.jstor.org/stable/2267778. 3

Stephen Cole Kleene and Richard Eugene Vesley. *The foundations of intuitionistic mathematics, especially in relation to recursive functions*. North-Holland, Amsterdam, 1965. 26

Jean-Louis Krivine. *Théorie des ensembles*. Cassini, Paris, 1998. 2

Per Martin-Löf. *Notes on constructive mathematics*. Almqvist & Wiksell, Stockholm, 1970. 1, 3, 25

Ray Mines, Fred Richman, and Wim Ruitenburg. *A course in constructive algebra*. Universitext. Springer-Verlag, New York, 1988. doi:10.1007/978-1-4419-8640-5.2

Manfred E. Szabo, editor. *The collected papers of Gerhard Gentzen*. (*Studies in Logic and the Foundations of Mathematics*). North-Holland, Amsterdam, 1969. 27

A. S. Troelstra. *Principles of intuitionism: lectures presented at the summer conference on Intuitionism and Proof theory (1968) at SUNY at Buffalo, N.Y*. Lecture Notes in Mathematics, Vol. 95. Springer-Verlag, Berlin, 1969. 24

The Univalent Foundations Program. *Homotopy type theory: univalent foundations of mathematics*. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013. 3
3. si $\alpha < \alpha$ alors $0_E = \beta$ (irréflexivité);

4. si $\alpha < \beta$ alors $\alpha \le \beta$;

5. si $\alpha \le \beta$ et $\beta \le \gamma$, alors $\alpha \le \gamma$ (transitivité 1);

6. si $\alpha < \beta$ et $\beta \le \gamma$, alors $\alpha < \gamma$ (transitivité 2);

7. si $\alpha \le \beta$ et $\beta < \gamma$, alors $\alpha < \gamma$ (transitivité 3);

8. $\alpha < s(\beta)$ si, et seulement si, $\alpha \le \beta$ (en utilisant l'axiome 1 on obtient $\alpha < s(\alpha)$);

9. $s(\beta) \le \alpha$ si, et seulement si, $\beta < \alpha$;

10. si $\alpha < \gamma$ et $\beta < \gamma$, alors $\sup(\alpha, \beta) < \gamma$;

11. si $\alpha < \sup(\alpha, \beta)$ alors $\alpha < \beta$;

12. si $\gamma < \alpha$ et $\alpha \le \sup(\beta, \gamma)$, alors $\alpha \le \beta$;

13. pour $(\alpha_i)_{i \in I} \in \text{Fam}(\mathfrak{F}, E^*)$ et $\beta \in E$, on a

$$ \alpha_i \le \beta \text{ pour tout } i \in I \text{ si, et seulement si, } \sup(\alpha_i)_{i \in I} \le \beta $$

(propriété caractéristique de sup);

14. si $\gamma < \beta$ pour tout $\gamma < \alpha$, alors $\alpha \le \beta$;

15. $\alpha \le 0_E$ ou $0_E < \alpha$.

La catégorie des $\mathfrak{F}$-ordres est définie par ses morphismes

$$ (E, <_E, \leq_E, 0_E, \sup_E, s_E) \to (F, <_F, \leq_F, 0_F, \sup_F, s_F), $$

qui sont les fonctions de $E$ dans $F$ qui préservent la structure (au sens usuel évident).

**Commentaire.** 1) Soit $\gamma \in E$ et $(\alpha_n)_{n \in \mathbb{N}}$ avec $\alpha_n = \gamma$ ou $\alpha_n = s(\gamma)$ pour tout $n$. Alors l'élément $\sup_{n \in \mathbb{N}} \alpha_n$ «hésite» à priori entre $s(\gamma)$ et $s(s(\gamma))$. Il n'y a donc aucun espoir que la disjonction «$\alpha \le \beta$ ou $\beta < \alpha$» puisse être explicite dans le cas d'éléments $\alpha, \beta \ne 0_E$. En conséquence, on a introduit la fonction $\sup$ avec les axiomes correspondants que l'on peut réaliser de manière constructive, de façon à mieux décrire en quoi l'ordre peut être considéré comme «total». Mais ce n'est peut-être pas optimal (il peut manquer des axiomes raisonnables, qui sont satisfaites dans l'ensemble $\text{Ord}_2$ des ordinaux dénombrables construit dans la section 3 et qui ne résultent pas de ceux donnés ici).

2) L'irréflexivité est donnée sous une forme qui, au lieu d'affirmer une négation, permet à $E$ de se réduire à un singleton. Cela se produit si, et seulement si, $0_E = s(0_E)$, ce qui implique $0_E < 0_E$ en utilisant l'axiome 8.

3) L'axiome 15 exprime que $\{0_E\}$ est détachable. Cela contraste avec le fait qu'aucun élément autre que $0_E$ ne définit un singleton détachable. On a défini $\sup$ sur $E^*$ plutôt que sur $E$ en vue de satisfaire constructivement la disjonction de l'axiome 15.

4) La propriété caractéristique de sup montre que cette loi est idempotente et satisfait les propriétés d'associativité et commutativité généralisées. ◇

## 2.3 Quelques propriétés

**Proposition et définition 2.2** (généralisation de la définition 2.1).

Pour $\alpha^1, \dots, \alpha^r \in E$ nous posons

$$ \sup(\alpha^1, \dots, \alpha^r) \stackrel{\text{def}}{=} \begin{cases} 0_E & \text{si } \alpha^1 = \dots = \alpha^r = 0_E \\ \sup \text{ des } \alpha^k \ne 0_E & \text{sinon.} \end{cases} $$

La propriété caractéristique de sup est satisfaite :

$$ \alpha^1 \le \beta \text{ et } \dots \text{ et } \alpha^r \le \beta \text{ si, et seulement si, } \sup(\alpha^1, \dots, \alpha^r) \le \beta. $$

**Fait 2.3.** Soient $\alpha, \beta$ des éléments de $E$.
— s(α) < s(β) si, et seulement si, α < β.

— s(α) ≤ s(β) si, et seulement si, α ≤ β.

**Démonstration.** Utiliser les axiomes 8 et 9.

☐

**Fait 2.4.** Les axiomes 10 à 12 et 14 sont en fait des équivalences :

10. on a $\alpha < \gamma$ et $\beta < \gamma$ si, et seulement si, $\sup(\alpha, \beta) < \gamma$;

11. on a $\alpha < \sup(\alpha, \beta)$ si, et seulement si, $\alpha < \beta$;

12. l'implication si $\gamma < \alpha$, alors $\alpha \leqslant \sup(\beta, \gamma)$ a lieu si, et seulement si, $\alpha \leqslant \beta$;

14. on a $\alpha \leqslant \beta$ si, et seulement si, $\gamma < \beta$ pour tout $\gamma < \alpha$.

**Démonstration.** Utiliser les transitivités et la propriété caractéristique de sup.

☐

**Fait 2.5** (la fonction successeur commute avec les sup finis, notation comme dans la proposition et définition 2.2). On a $\sup(s(\alpha), s(\beta)) = s(\sup(\alpha, \beta))$ et plus généralement $\sup(s(\alpha^1), \dots, s(\alpha^r)) = s(\sup(\alpha^1, \dots, \alpha^r))$.

En particulier, si $\alpha^1 < \gamma, \dots, \alpha^r < \gamma$, alors $\sup(\alpha^1, \dots, \alpha^r) < \gamma$.

**Démonstration.** Il suffit de démontrer $s(\sup(\alpha, \beta)) = \sup(s(\alpha), s(\beta))$. On a la chaîne d'équivalences suivantes : $s(\sup(\alpha, \beta)) \leqslant \gamma \iff \sup(\alpha, \beta) < \gamma \iff (\alpha < \gamma \text{ et } \beta < \gamma) \iff (s(\alpha) \leqslant \gamma \text{ et } s(\beta) \leqslant \gamma) \iff \sup(s(\alpha), s(\beta)) \leqslant \gamma$. ☐

**Proposition et définition 2.6** (définition d'une fonction s infinitaire, sa propriété caractéristique). Pour tout $(\alpha_i)_{i \in J} \in \text{Fam}(\mathfrak{F}, E)$, on définit $s(\alpha_i)_{i \in J} = \sup(s(\alpha_i))_{i \in J}$. On a alors l'équivalence suivante :

$$ \alpha_i < \beta \text{ pour tout } i \in J \text{ si, et seulement si, } s(\alpha_i)_{i \in J} \leqslant \beta. $$

**Démonstration.** Utiliser les axiomes 9 et 13.

☐

Nous écrivons $F \subseteq_f I$ pour exprimer le fait que $F$ est une partie finiment énumérée de $I$.

**Fait 2.7.** Soit $\alpha, \beta^1, \dots, \beta^m \in E$.

1. Supposons que $\alpha = s(\alpha_i)_{i \in J}$ avec $(\alpha_i)_{i \in J} \in \text{Fam}(\mathfrak{F}, E)$ et que $\alpha_i < \sup(\beta^1, \dots, \beta^m)$ pour tout $i \in J$. Alors $\alpha \leqslant \sup(\beta^1, \dots, \beta^m)$.

2. Supposons que $\beta^k = s((\beta^k)_i)_{i \in J_k}$ avec $((\beta^k)_i)_{i \in J_k} \in \text{Fam}(\mathfrak{F}, E)$ pour $k \in [1..m]$. Soit $F_1 \subseteq_f J_1, \dots, F_m \subseteq_f J_m$ non tous vides. Si

$$ \alpha \leqslant \sup((\beta^k)_j)_{k \in [1..m]}, \quad j \in F_k, $$

$$ \text{alors } \alpha < \sup(\beta^1, \dots, \beta^m). $$

**Démonstration.** 1. C'est la proposition et définition 2.6.

2. Supposons par exemple $F_1$ non vide. Alors $\alpha \leqslant \sup((\beta^1)_j)_{j \in F_1} < \beta^1 \leqslant \sup(\beta^1, \dots, \beta^m)$. L'inégalité stricte résulte du fait 2.5 parce que tous les $(\beta^1)_j$ sont $< \beta^1$ d'après la proposition et définition 2.6. ☐

# 3 Construction inductive d'ensembles d'ordinaux

Dans les sections 3 et 4, l'ensemble d'indexeurs $\mathfrak{F}$ est fixé mais est rarement mentionné explicitement.
Nous allons définir un ensemble d'ordinaux **Ord** (plus précisément **Ord<sub>F</sub>**) et nous prouverons que c'est un objet initial dans la catégorie des F-ordres.

Nous définissons d'abord un ensemble **ord** (plus précisément **ord<sub>F</sub>**) de noms pour les ordinaux F-indexés au moyen d'une définition inductive. La définition inductive la plus simple d'un ensemble infini est celle de $\mathbb{N}$ : l'ensemble possède un élément 0 et une application successeur $x \mapsto s(x) : \mathbb{N} \to \mathbb{N}$. La définition inductive de **ord** est très semblable à celle de $\mathbb{N}$. Dans $\mathbb{N}$, chaque élément est soit 0 soit un $s(x)$ pour un $x \in \mathbb{N}$. De même, dans **ord**, chaque élément est soit 0 soit le s d'une famille F-indexée d'éléments de **ord** ; on note $\mathbf{ord}^*$ l'ensemble des éléments de ce deuxième type.

**Définition 3.1.** L'ensemble **ord** (plus précisément **ord<sub>F</sub>**) est défini par induction : il admet un élément distingué 0 et il a une application

$$s: \mathrm{Fam}(\mathfrak{F}, \mathrm{ord}) \to \mathrm{ord}.$$

N. B. : La seule contrainte dans cette définition inductive est que s est bien une application de Fam($\mathfrak{F}$, **ord**) vers **ord**.

Un élément de **ord** sera appelé un [nom d'un] ordinal dans la suite.

Quand $\mathfrak{F} = \mathfrak{F}_2$, nous obtenons l'ensemble des noms d'ordinaux dénombrables, noté $\mathbf{ord}_2$.

*Remarque 3.2.* Tout élément $\alpha \in \mathbf{ord}^*$ est donné avec :

- l'indexeur utilisé dans la définition de $\alpha$ : il sera noté $\mathrm{In}_\alpha$;

- la famille $\chi_{\mathbf{ord}}(\alpha, i)_{i \in \mathrm{In}_\alpha}$ de ses sous-ordinaux définitionnels, i. e. l'élément de Fam($\mathfrak{F}$, **ord**) tel que $\alpha = s(\chi_{\mathbf{ord}}(\alpha, i))_{i \in \mathrm{In}_\alpha}$.

Ainsi, la définition inductive de **ord** implique l'existence d'une fonction $\alpha \mapsto \mathrm{In}_\alpha : \mathbf{ord}^* \to \mathfrak{F}$ et l'existence d'une famille dépendante $(\alpha, i) \mapsto \chi_{\mathbf{ord}}(\alpha, i)$ définie pour $\alpha \in \mathbf{ord}^*$ et $i \in \mathrm{In}_\alpha$. Pour simplifier l'exposé on commettra dans la suite un léger abus de notation en sous-entendant la construction de la famille dépendante $\chi_{\mathbf{ord}}$ et en notant $\alpha_i$ pour $\chi_{\mathbf{ord}}(\alpha, i)$. On écrira donc selon cette convention d'écriture $\alpha = s(\alpha_i)_{i \in \mathrm{In}_\alpha}$. $\diamond$

$$\text{Pour } \alpha^1, \dots, \alpha^r \in \mathbf{ord} \text{ on définit } s(\alpha^1, \dots, \alpha^r) = s(\alpha^i)_{i \in \llbracket 1..r \rrbracket}.$$

En particulier, si $\alpha \in \mathbf{ord}$, son successeur immédiat $s(\alpha)$ est l'élément $\beta = s(\beta_i)_{i \in \mathrm{In}_\beta}$, où $\mathrm{In}_\beta = \mathbb{N}_1 = \{0\}$ et $\beta_0 = \alpha$. La suite $(\underline{m})_{m \in \mathbb{N}}$ dans **ord** est définie par récurrence par $\underline{m} + 1 = s(\underline{m})$. Puis nous définissons $\omega = s(\underline{n})_{n \in \mathbb{N}}$.

Pour démontrer une propriété de $\alpha = s(\alpha_i)_{i \in \mathrm{In}_\alpha}$, il suffit de démontrer la propriété pour chaque $\alpha_i$. De la même manière, on peut construire par induction une fonction dont le domaine de définition est **ord**, ou définir un prédicat sur **ord** par induction. C'est le cas par exemple dans les définitions 3.3 et 3.6 et plus généralement dans toute la suite de l'article.

## 3.1 Sous-ordinaux

Voici une définition inductive précise.

**Définition 3.3.** Étant donné $\alpha = s(\alpha_i)_{i \in \mathrm{In}_\alpha} \in \mathbf{ord}^*$, un élément $\beta$ de **ord** est appelé un sous-ordinal définitionnel de $\alpha$ lorsque $\beta = \alpha_i$ pour un $i \in \mathrm{In}_\alpha$. On note alors $\beta \ll_1 \alpha$. L'élément $\gamma$ est un sous-ordinal de $\alpha$ s'il est un sous-ordinal définitionnel de $\alpha$ ou un sous-ordinal d'un sous-ordinal définitionnel de $\alpha$. On note alors $\gamma \ll \alpha$.

Ainsi $\emptyset$ est le seul élément de **ord** qui n'a pas de sous-ordinal.

Le fait suivant prend acte du fait que la définition des relations $\cdot \ll_1 \cdot$ et $\cdot \ll \cdot$ est une définition inductive correcte sur **ord**.

**Fait 3.4.** Les relations $\cdot \ll_1 \cdot$ et $\cdot \ll \cdot$ sont bien fondées sur **ord**.

En conséquence « il n'y a pas de branches infinies dans l'arbre des sous-ordinaux d'un élément de **ord** », au sens suivant.
**Fait 3.5.** Une suite $(\alpha^j)_{j=1,2,...}$ dans ord où chaque $\alpha^{j+1}$ est un sous-ordinal de $\alpha^j$ aboutit en un nombre fini d'étapes à $\alpha^r = \emptyset$.

Notons que pour faire une construction (ou une démonstration) par $\leq_1$-induction (ou par $\leq$-induction), le cas $\emptyset$ doit être traité à part car il n'a pas de sous-ordinal. Cependant, jusqu'à l'arithmétique des ordinaux page F17, nous allons pouvoir nous passer de cette distinction de cas.

## 3.2 Définition de la loi sup

### Définition 3.6.

1. La loi sup: $\text{Fam}(\mathfrak{F}, \text{ord}^*) \to \text{ord}^*$ est définie comme suit.

Soit $(\alpha^j)_{j \in J}$ une famille dans $\text{ord}^*$ avec $J \in \mathfrak{F}$. Si $\alpha^j = s((\alpha^j)_i)_{i \in I_j}$, alors $\sup(\alpha^j)_{j \in J}$ est l'élément $\varepsilon = s(\varepsilon_k)_{k \in K}$, où

- $K$ est la réunion disjointe des $I_j$;

- $(\varepsilon_k)_{k \in K}$ est la famille définie par $\varepsilon_k = (\alpha^j)_i$ si $\iota_j(i) = k$

(ici $\iota_j: I_j \to K$ est l'injection de $I_j$ dans la réunion disjointe des $I_j$). On notera $\sup(\alpha^j)_{j \in [1..r]} = \sup(\alpha^1, \dots, \alpha^r)$.

2. Le sup d'une famille finie dans $\text{ord}$ est défini comme suit.

$$ \sup(\alpha^1, \dots, \alpha^r) \stackrel{\text{def}}{=} \begin{cases} \emptyset & \text{si } \alpha^1 = \dots = \alpha^r = \emptyset \\ \text{le sup des } \alpha^k \in \text{ord}^* \text{ sinon.} \end{cases} $$

Notons que le point 2 est formellement inclus dans le point 1 si nous adoptons la convention $\text{In}_{\emptyset} = \mathbb{N}_0$. Par contre cela ne permettrait pas de définir des sup arbitraires de familles $\mathfrak{F}$-indexées d'éléments de $\text{ord}$.

## 3.3 Définitions de $\leq$ et $<$

Le principal du travail reste à faire, à savoir définir deux prédicats binaires $\leq$ et $<$ sur ord qui satisfont les propriétés attendues. Plus précisément :

- la relation « $\alpha \leq \beta$ et $\beta \leq \alpha$» doit être une relation d'équivalence (on note **Ord** l'ensemble quotient),

- les prédicats $\leq$ et $<$ et les fonctions sup et s doivent passer au quotient (on ne change pas leurs noms),

- et la structure obtenue doit être une structure de $\mathfrak{F}$-ordre.

Pour faire ce travail on définit par induction deux relations asymétriques entre d'une part un élément de **ord** et d'autre part une *liste finie non vide* (à permutation près$^5$) d'éléments de **ord** :

$$ \alpha \leq \beta^1, \dots, \beta^m \text{ et } \alpha < \beta^1, \dots, \beta^m \quad (m \geq 1). $$

**Conventions.** — Les lettres $\alpha, \beta, \gamma, \varepsilon$ éventuellement munies d'exposants, d'indices ou de primes, désignent des éléments de **ord**.

- Si $\alpha$ est un élément de **ord** et si $F$ est une liste finie, éventuellement vide, dans $\text{In}_\alpha$, on note $\alpha_F$ la liste des $\alpha_i$ pour les $i$ dans $F$.

Les définitions inductives simultanées des deux relations sont les suivantes.

Les cas particuliers pour $\emptyset$ sont évités en posant par convention $\text{In}_{\emptyset} = \mathbb{N}_0$. Soit $m$ un entier $\geq 1$.

$\alpha \leq \beta^1, \dots, \beta^m$ est défini par $\alpha_i < \beta^1, \dots, \beta^m$ pour tout $i \in \text{In}_\alpha$.

$\alpha < \beta^1, \dots, \beta^m$ est défini par il existe $F_1 \subseteq_f \text{In}_{\beta^1}, \dots, F_m \subseteq_f \text{In}_{\beta^m}$ non toutes vides telles que $\alpha \leq \beta^1_{F_1}, \dots, \beta^m_{F_m}$.

<footnote n="5">5. On dit aussi un *multiensemble* non vide.</footnote>
Le fait que ces définitions sont correctement posées tient à ce que les éléments de ord sont définis de manière inductive et à ce que le couple des deux définitions est inductif.

Sans la convention concernant $\text{In}_0 = \mathbb{N}_0$ le fait 3.8 ci-dessous devrait faire partie de la définition. Cette convention est «un petit miracle» qui nous permet, dans les démonstrations qui suivront, de ne pas à avoir à raisonner au cas par cas selon que $\alpha = \emptyset$ ou $\alpha \in \text{ord}^*$.

La signification de ces deux relations est $\alpha \le \sup(\beta^1, \dots, \beta^m)$ et $\alpha < \sup(\beta^1, \dots, \beta^m)$.

**Lemme 3.7.** On a $\alpha < \beta^1, \dots, \beta^m$ si, et seulement si, $\alpha < \sup(\beta^1, \dots, \beta^m)$.

De la même manière $\alpha \le \beta^1, \dots, \beta^m$ si, et seulement si, $\alpha \le \sup(\beta^1, \dots, \beta^m)$.

*Démonstration.* Écrivons

$\alpha < \beta^1, \dots, \beta^m$ pour $\alpha < \sup(\beta^1, \dots, \beta^m)$,

$\alpha \le \beta^1, \dots, \beta^m$ pour $\alpha \le \sup(\beta^1, \dots, \beta^m)$.

Soit $\varepsilon = \sup(\beta^1, \dots, \beta^m)$. Alors $\alpha < \beta^1, \dots, \beta^m$ si, et seulement si, $\alpha \le \varepsilon_F$ avec $F$ un sous-ensemble finiment énuméré non vide de la réunion disjointe $K$ des $\text{In}_{\beta j}$ et $\varepsilon_k = (\beta^j)_i$ si $k$ est l'image de $i$ dans $K$; en posant $F_j = F \cap \text{In}_{\beta j}$, les $F_j$ ne sont pas tous vides et cela peut être réécrit comme $\alpha \le \beta^1, \dots, \beta^m$.

On a $\alpha \le \beta^1, \dots, \beta^m$ si, et seulement si, pour tout $i \in \text{In}_\alpha$, $\alpha_i < \varepsilon$, i. e. $\alpha_i < \beta^1, \dots, \beta^m$, i. e. $\alpha_i < \beta^1, \dots, \beta^m$; cela a lieu si, et seulement si, $\alpha \le \beta^1, \dots, \beta^m$. $\square$

La relation $\alpha = \text{Ord}$ $\beta$ est définie comme signifiant «$\alpha \le \beta$ et $\beta \le \alpha$».

On montrera dans la section 4 que la relation $\cdot = \text{Ord}$ est une relation d'équivalence et on définira l'ensemble **Ord** comme le quotient de **ord** par cette relation.

Notons que jusqu'au théorème 4.8, le symbole $=$ entre deux éléments de **ord** est l'égalité dans **ord** et n'a pas la signification de $=_{\text{Ord}}$. Néanmoins, une fois que l'on aura montré que les relations et les lois de **ord** «passent au quotient» dans **Ord**, les énoncés contenant le symbole $=$ seront également valables avec le symbole $=_{\text{Ord}}$.

## 3.4 Ordinaux finis, ordinaux bornés

Nous commençons avec quelques propriétés de $\emptyset$.

**Fait 3.8.** Soit $m$ un entier $\ge 1$, $\alpha, \beta^1, \dots, \beta^m \in \text{ord}$, et $\gamma \in \text{ord}^*$. On a

1. $\emptyset \le \beta^1, \dots, \beta^m$;

2. $\emptyset < \gamma, \beta^2, \dots, \beta^m$;

3. $\alpha < \underbrace{\emptyset, \dots, \emptyset}_{m \text{ fois}}$ est impossible.

*Démonstration.* Conséquence immédiate des définitions. $\square$

*Remarque 3.9.* L'axiome 15 sera satisfait dans **Ord** car tout élément de **ord** est donné ou bien sous la forme $\emptyset$ ou bien sous la forme d'un élément $\gamma \in \text{ord}^*$, de sorte qu'on a toujours $\emptyset < \gamma$ d'après le point 2 du fait 3.8. $\diamond$

**Fait 3.10.** Soit $m, n \in \mathbb{N}$. Alors

1. $m \le n$ si, et seulement si, $\underline{m} \le \underline{n}$;

2. $m < n$ si, et seulement si, $\underline{m} < \underline{n}$;

3. $\underline{m} \le \underline{n}$ et $\underline{n} < \underline{m}$ sont incompatibles.

*Démonstration.* Pour les implications directes dans 1 et 2, on écrit $n = m + r$ et l'on fait une récurrence sur $r$. Pour les implications réciproques, on a déjà vu les cas $m = 0$ et $n = 0$. On vérifie ensuite que $\underline{m} + 1 \le \underline{n} + 1$ implique $\underline{m} \le \underline{n}$, et que $\underline{m} + 1 < \underline{n} + 1$ implique $\underline{m} < \underline{n}$. Cela permet de conclure par récurrence sur $m$.

Le point 3 découle des points 1 et 2. $\square$
Un $\alpha \in \mathbf{ord}$ est dit fini si $\alpha =_{\mathbf{Ord}} \underline{\mathbf{m}}$ pour un $m \in \mathbb{N}$, il est dit borné s'il est majoré par un ordinal fini. Les ordinaux bornés sont « beaucoup plus complexes » que les ordinaux finis (voir les exemples 3.17 et 3.18).

Dans la Section 3.7, nous discuterons ce que les relations $\leq$ et $<$ sur l'ensemble $\mathbf{ord}_\mathfrak{F}$ deviennent en mathématiques classiques.

## 3.5 Premières conséquences

Le fait suivant montre que lorsqu'on sera passé au quotient, sur l'ensemble **Ord**, la loi s vérifiera la propriété caractéristique donnée dans l'axiome 13.

**Fait 3.11 (sdef).** On a $\alpha \leq \beta$ si, et seulement si, pour tout $i \in \text{In}_\alpha$, $\alpha_i < \beta$.

*Démonstration.* Cette propriété est tautologique : il s'agit simplement de la définition de $\alpha \leq \beta$.

☐

De la même manière, le fait suivant montre que la loi sup satisfera la propriété caractéristique donnée dans l'axiome 13 quand nous montrerons qu'elle passe au quotient dans **Ord**.

**Fait 3.12 (supdef).** Soit $(\alpha^j)_{j \in J}$ une famille dans $\mathbf{ord}^*$ avec $J \in \mathfrak{F}$, $\gamma = \sup(\alpha^j)_{j \in J}$, et $\beta \in \mathbf{ord}$. On a $\gamma \leq \beta$ si, et seulement si, $\alpha^j \leq \beta$ pour tout $j \in J$. En particulier, $\sup(\alpha, \beta) \leq \beta$ si, et seulement si, $\alpha \leq \beta$.

N. B. : Le résultat est également vrai pour le sup d'une famille finie dans **ord**.

*Démonstration.* Encore une tautologie linguistique. On a $\alpha^j = s_{i \in I_j}(\alpha^j)_i$ pour un $I_j \in \mathfrak{F}$. Par définition de $\gamma$ et de $\leq$, l'inégalité $\gamma \leq \beta$ signifie que pour tout $j \in J$ et tout $i \in I_j$, on a $(\alpha^j)_i < \beta$, i. e. que pour tout $j \in J$, on a $\alpha^j \leq \beta$. ☐

☐

Le fait suivant montre que lorsqu'on sera passé au quotient, sur l'ensemble **Ord**, les axiomes 8 et 9 seront satisfaits.

**Fait 3.13.** 1. ax8. On a $\alpha < s(\beta)$ si, et seulement si, $\alpha \leq \beta$.

2. ax9. On a $\beta < \alpha$ si, et seulement si, $s(\beta) \leq \alpha$.

*Démonstration.* Rappelons que l'élément $\gamma = s(\beta)$ est défini par $\text{In}_\gamma = \{0\}$ et $\gamma_0 = \beta$.

1. Par définition, $\alpha < \gamma$ signifie que $\alpha \leq \gamma_F$ pour une liste non vide $F \subseteq_f \{0\}$. Cela force $F = [0]$ et $\gamma_F = \beta$.

2. Par définition, $\gamma \leq \alpha$ signifie que $\gamma_0 < \alpha$, i. e. $\beta < \alpha$.

En bref, mieux que des équivalences, ce sont des tautologies. ☐

☐

La fait suivant nous permettra de raccourcir certaines démonstrations par induction.

**Fait 3.14.**

a. On a une inégalité $\alpha \leq \beta$ si, et seulement si, pour tout $i \in \text{In}_\alpha$, il existe un $F_i \subseteq_f \text{In}_\beta$ non vide tel que $\alpha_i \leq \beta_{F_i}$.

b. On a une inégalité $\alpha < \beta$ si, et seulement si, il existe un $F \subseteq_f \text{In}_\beta$ non vide tel que pour tout $i \in \text{In}_\alpha$ on a $\alpha_i < \beta_F$.

*Démonstration.* Directe d'après les définitions. ☐

☐

Nous quittons maintenant les démonstrations tautologiques pour aborder les premières démonstrations par induction.
**Fait 3.15** (affaiblissement et contraction).

— **affaiblissement.** Si $\alpha \le \beta^1, \dots, \beta^m$, alors pour tout $\beta$ on a $\alpha \le \beta, \beta^1, \dots, \beta^m$.

— **contraction.** Si $\alpha \le \beta^1, \beta^1, \beta^2, \dots, \beta^m$ alors $\alpha \le \beta^1, \beta^2, \dots, \beta^m$.

— Mêmes propriétés avec $<$ à la place de $\le$.

**Démonstration.** Démonstrations par induction, immédiates d'après les définitions. □

Le lemme suivant est un corolaire du lemme 3.14. Le point 1 (resp. 2) impliquera que la fonction $s$ (resp. $\sup$) passe au quotient dans **Ord** (resp. **Ord**"). Le point 3 impliquera que les relations $\le$ et $=$ sont réflexives dans **Ord**, les points 5 et 7 impliqueront les axiomes 3 et 14 pour **Ord**.

**Lemme 3.16.**

1. s0. Soit $\alpha, \beta \in \mathbf{ord}$ avec $\mathrm{In}_\alpha = \mathrm{In}_\beta$ et $\alpha_i \le \beta_i$ pour tout $i \in \mathrm{In}_\alpha$. Alors $\alpha \le \beta$.

2. sup0. Soit $\alpha, \beta \in \mathbf{ord}^*$ avec $\mathrm{In}_\alpha = \mathrm{In}_\beta$ et $\alpha_i \le \beta_i$ pour tout $i \in \mathrm{In}_\alpha$. Alors

$$ \sup(\alpha_i)_{i \in \mathrm{In}_\alpha} \le \sup(\beta_i)_{i \in \mathrm{In}_\beta}. $$

Le résultat vaut aussi pour les sup finis dans **ord**.

3. rfl. Pour tout $\alpha \in \mathbf{ord}$, on a $\alpha \le \alpha$. À fortiori, $\alpha \le \alpha, \beta^1, \dots, \beta^m$.

4. s1. Pour tout $\alpha \in \mathbf{ord}^*$ et tout $i \in \mathrm{In}_\alpha$, on a $\alpha_i < \alpha$. À fortiori, $\alpha_i < \alpha, \beta^1, \dots, \beta^m$.

5. irfl. Pour tout $\alpha \in \mathbf{ord}$, $\alpha < \alpha$ est impossible.

6. $\alpha < s(\alpha)$.

7. ax14. Si $\gamma < \beta$ pour tout $\gamma < \alpha$, alors $\alpha \le \beta$.

**Démonstration.** 1. Direct d'après le fait 3.14a. On prend $F = \{i\}$.

2. Soit $\gamma = \sup(\alpha_i)_{i \in \mathrm{In}_\alpha}$ et $\epsilon = \sup(\beta_i)_{i \in \mathrm{In}_\beta}$. D'après le fait 3.14a, pour tout $j \in \mathrm{In}_{\alpha_i}$ il existe un $F_{i,j} \subseteq_f \mathrm{In}_{\beta_i}$ non vide tel que $(\alpha_i)_j \le (\beta_i)_{F_{i,j}}$; $F_{i,j}$ est à fortiori dans la réunion disjointe des $\mathrm{In}_{\beta_i}$, de sorte que $(\alpha_i)_j < \epsilon$ par définition de $\epsilon$. Par définition, $\alpha_i \le \epsilon$, de sorte que d'après le fait 3.12 on a $\gamma \le \epsilon$.

3. Par induction : nous utilisons le fait 3.14a, on prend $F = \{i\}$ et $\alpha \le \alpha$ se réduit à $\alpha_i \le \alpha_i$.

4. Par induction : nous utilisons le fait 3.14b, on prend $F = \{i\}$ et $\alpha_i < \alpha$ se réduit à $(\alpha_i)_j < \alpha_i$.

5. Par induction : nous utilisons fait 3.14b, on prend $F = \{i\}$ et « $\alpha < \alpha$ est impossible» se réduit à : «$\alpha_i < \alpha_i$ est impossible».

6. Appliquer s1 à $\beta = s(\alpha)$.

7. Si $\alpha = 0$, la conclusion est claire. Si $\alpha = s(\alpha_i)_{i \in I}$, comme $\alpha_i < \alpha$ pour chaque $i \in \mathrm{In}_\alpha$ (point 4), l'hypothèse que $\gamma < \beta$ pour tout $\gamma < \alpha$ montre que $\alpha_i < \beta$ pour tout $i \in \mathrm{In}_\alpha$. Nous concluons par le fait 3.11 que $\alpha \le \beta$. □

## 3.6 Ordinaux et principes d'omniscience limités

*Exemple 3.17.* Soit $(v_n)_{n \in \mathbb{N}}$ une suite dans $\{0,1\}$ qui prend au moins une fois la valeur 1. Le principe **LLPO** dit que nous avons

$$ \exists k \in \{0,1\} \ \forall n \ (v_n = 1 \Rightarrow n \equiv k \ \mathrm{mod} \ 2). \quad (*) $$

Pour une telle suite $(v_n)_{n \in \mathbb{N}}$ définissons $\epsilon$, $\epsilon^1$ et $\epsilon^2 \in \mathbf{ord}$ comme suit :

$$ \epsilon = s(\underline{v_n})_{n \in \mathbb{N}}, \quad \epsilon^1 = s(\underline{v_{2m}})_{m \in \mathbb{N}}, \quad \epsilon^2 = s(\underline{v_{2m+1}})_{m \in \mathbb{N}}. $$

Alors on a $\epsilon \le \sup(\epsilon^1, \epsilon^2)$. Mais $\epsilon \le \epsilon^1$ donne $k = 0$ dans (*) et $\epsilon \le \epsilon^2$ donne $k = 1$ dans (*). Donc la disjonction $\epsilon \le \epsilon^1$ ou $\epsilon \le \epsilon^2$ n'a pas de démonstration constructive : supposer la disjonction pour une suite $(v_n)$ arbitraire implique **LLPO**.
Exemple 3.18. Soit $(u_n)_{n \in \mathbb{N}}$ une suite croissante (au sens large) dans $\{0, 1\}$. Le principe LPO dit qu'une telle suite est stationnaire :

$$ \exists n \in \mathbb{N} \forall m \in \mathbb{N} u_m \le u_n. \quad (*) $$

Pour une telle suite $(u_n)_{n \in \mathbb{N}}$ définissons $\alpha$ et $\beta \in \mathbf{ord}$ comme suit :

$$ \alpha = s(u_n)_{n \in \mathbb{N}}, \quad \beta = s(u_n + 1)_{n \in \mathbb{N}}. $$

Nous notons que l'inégalité stricte $\alpha < \beta$ est équivalente (d'après les faits 3.10 et 3.14 et le lemme 3.7) à

$$ \exists n \in \mathbb{N} \forall m \in \mathbb{N} u_m < u_n + 1, $$

ce qui revient à $(*)$. En fait, $\alpha$ hésite entre 1 et 2, $\beta$ hésite entre 2 et 3, et l'inégalité $\alpha < \beta$ est valide si nous supposons **LPO**. Mais affirmer $\alpha < \beta$ pour toutes les suites $(u_n)$ implique **LPO** en mathématiques constructives. Ici nous voyons que l'hésitation entre 1 et 2 pour une suite infinie donne le même sentiment qu'hésiter (dans un contexte classique) entre une suite bornée ou non bornée d'entiers naturels : ajouter 1 aux termes d'une telle suite n'augmente sa borne supérieure que si la suite est bornée.

## 3.7 En mathématiques classiques

La proposition 3.19 montre que le principe du tiers exclu (**LEM**) simplifie et/ou obscurcit dramatiquement l'étude de la structure de $\mathbf{ord}_\mathfrak{F}$ par rapport aux relations $<$ et $\leq$.

**Proposition 3.19.** *Supposons LEM. Alors pour $\alpha, \beta \in \mathbf{ord}$, on a $\alpha \leq \beta$ ou $\beta < \alpha$. En outre, si $\beta < \alpha$, il existe un $i \in \text{In}_\alpha$ tel que $\beta \leq \alpha_i$.*

*Démonstration.* On prouve par induction simultanée les deux propriétés suivantes.

$$ \langle \alpha \leq \beta \text{ ou } \beta < \alpha \rangle \text{ et } \langle \beta \leq \alpha \text{ ou } \alpha < \beta \rangle. $$

Par hypothèse d'induction, on a pour tout $i \in \text{In}_\alpha$ et tout $j \in \text{In}_\beta$, $\langle \alpha \leq \beta_j \text{ ou } \beta_j < \alpha \rangle$, et aussi $\langle \beta \leq \alpha_i \text{ ou } \alpha_i < \beta \rangle$.

La première disjonction implique par **LEM** que ou bien $\beta_j < \alpha$ pour tout $j \in \text{In}_\beta$ ou bien on a un $j \in \text{In}_\beta$ tel que $\alpha \leq \beta_j$. Dans le premier cas on a $\beta \leq \alpha$ par définition de $\cdot < \dots$. Dans le second cas on a $\alpha < \beta$ par définition de $\cdot < \dots$, avec pour $F \subseteq_f \text{In}_\beta$ la liste $[j]$.

Raisonnement symétrique pour la deuxième disjonction. $\square$

N. B. : Pour les ordinaux dénombrables le principe limité d'omniscience (**LPO**) suffit pour démontrer la proposition.

**Corolaire 3.20.** *Supposons LEM. Tout ordinal $\alpha \neq \emptyset$ est ou bien un successeur immédiat, ou bien le sup des ordinaux $\gamma < \alpha$.*

*Démonstration.* Considérons $\alpha = s(\alpha_i)_{i \in \text{In}_\alpha}$ et comparons $\alpha$ avec $\sup(\alpha_i)_{i \in \text{In}_\alpha}$. Les détails sont laissés à la lectrice. $\square$

**Corolaire 3.21.** *Supposons LEM. Tout ordinal borné est fini.*

*Démonstration.* Laissé au lecteur : utiliser le fait 3.13. $\square$

# 4 Résultats fondamentaux

## 4.1 Ord$_\mathfrak{F}$ est un objet initial dans la catégorie des $\mathfrak{F}$-ordres

**Lemme 4.1.** Soient $\alpha^1, \dots, \alpha^r$ dans ord ($r \geq 1$). On a

$$ \sup(\alpha^j)_{j \in \llbracket 1..r \rrbracket} < s(\alpha^j)_{j \in \llbracket 1..r \rrbracket}. $$
**Démonstration.** Montrons e. g. que $\epsilon = \sup(\alpha, \beta) < \gamma = \text{s}(\alpha, \beta)$. On a $\text{In}_\epsilon = \text{In}_\alpha + \text{In}_\beta$, avec $\epsilon_k = \alpha_i \text{ si } \iota_1(i) = k$, et $\epsilon_k = \beta_j \text{ si } \iota_2(j) = k$. On a $\text{In}_\gamma = \{1,2\}$ avec $\gamma_1 = \alpha$ et $\gamma_2 = \beta$. Nous appliquons le fait 3.14b avec $F = \{1,2\}$. Pour un $k$ arbitraire dans $\text{In}_\epsilon$, on a $\epsilon_k < \alpha, \beta$ car $\epsilon_k$ est $\alpha_i$ ou $\beta_j$ et, par s1, on a $\alpha_i < \alpha$ (à fortiori $\alpha_i < \alpha, \beta$) et $\beta_j < \beta$ (à fortiori $\beta_j < \alpha, \beta$). $\square$

Notons que la démonstration précédente repose sur le fait que les définitions $\leqslant$ et $<$ ont été données avec des listes sur le côté droit.

**Lemme 4.2 (transitivités).**

1. **trans1.** Si $\alpha \leqslant \beta^1, \dots, \beta^m$ et, pour tout $j \in [1..m]$, $\beta^j \leqslant \gamma^1, \dots, \gamma^r$, alors $\alpha \leqslant \gamma^1, \dots, \gamma^r$.

2. **trans2.** Si $\alpha < \beta^1, \dots, \beta^m$ et, pour tout $j \in [1..m]$, $\beta^j \leqslant \gamma^1, \dots, \gamma^r$, alors $\alpha < \gamma^1, \dots, \gamma^r$.

3. **trans3.** Si $\alpha \leqslant \beta^1, \dots, \beta^m$ et, pour tout $j \in [1..m]$, $\beta^j < \gamma^1, \dots, \gamma^r$, alors $\alpha < \gamma^1, \dots, \gamma^r$.

Comme cas particuliers, les axiomes 5 à 7 seront valides quand nous passerons au quotient dans **Ord** :

- si $\alpha \leqslant \beta$ et $\beta \leqslant \gamma$ alors $\alpha \leqslant \gamma$;

- si $\alpha < \beta$ et $\beta \leqslant \gamma$ alors $\alpha < \gamma$;

- si $\alpha \leqslant \beta$ et $\beta < \gamma$ alors $\alpha < \gamma$.

**Démonstration.** Les trois transitivités vont être démontrées par induction simultanée.

Pour démontrer **trans1**, on note que l'hypothèse signifie que l'on a $\alpha_i < \beta^1, \dots, \beta^m$ pour tout $i \in \text{In}_\alpha$. Fixons un tel $i$. On utilise **trans2** avec cet $\alpha_i$ à la place de $\alpha$, on obtient $\alpha_i < \gamma^1, \dots, \gamma^r$. Comme c'est vrai pour tout $i \in \text{In}_\alpha$, cela donne la conclusion souhaitée $\alpha \leqslant \gamma^1, \dots, \gamma^r$.

Pour démontrer **trans2**, on note que l'hypothèse implique que l'on a des $G_j \subseteq_f \text{In}_{\beta j}$ non tous vides tels que $\alpha \leqslant \beta_{G_1}^1, \dots, \beta_{G_m}^m$. On a aussi, pour $j \in [1..m]$ et pour tout $h \in \text{In}_{\beta j}$, $\beta_h^j < \gamma^1, \dots, \gamma^r$. À fortiori, cela est vrai pour les $h \in G_j$. On utilise alors **trans3** avec ces $\beta_h^j$ à la place des $\beta^j$. On obtient la conclusion souhaitée $\alpha < \gamma^1, \dots, \gamma^r$.

Pour démontrer **trans3**, on note que l'hypothèse implique (utiliser l'affaiblissement) que l'on a des $F_k \subseteq_f \text{In}_{\gamma k}$ non tous vides tels que $\beta^j \leqslant \gamma_{F_1}^1, \dots, \gamma_{F_r}^r$ pour $j \in [1..m]$. Cette fois-ci on utilise **trans1** avec des $\gamma_\ell^k$ à la place des $\gamma^k$, on en déduit que $\alpha \leqslant \gamma_{F_1}^1, \dots, \gamma_{F_r}^r$, ce qui implique $\alpha < \gamma^1, \dots, \gamma^r$. $\square$

Le lemme suivant montre que lorsqu'on sera passé au quotient sur **Ord**, l'axiome 4 sera satisfait.

**Lemme 4.3 (ax4).** Soit $\alpha, \beta^1, \dots, \beta^m \in \text{ord}$. Si $\alpha < \beta^1, \dots, \beta^m$, alors $\alpha \leqslant \beta^1, \dots, \beta^m$.

**Démonstration.** Démonstration par induction sur $\alpha$. On a $\alpha < \beta^1, \dots, \beta^m$ si, et seulement si, il existe des $F_k \subseteq_f \text{In}_{\beta k}$ non tous vides tels que, pour chaque $i \in \text{In}_\alpha$, on a $\alpha_i \leqslant \beta_{F_1}^1, \dots, \beta_{F_m}^m$. Fixons un $i \in \text{In}_\alpha$. Pour $j \in F_k$, on a $\beta_j^k < \beta^k$, et en affaiblissant $\beta_j^k < \beta^1, \dots, \beta^m$. Par **trans3**, on obtient $\alpha_i < \beta^1, \dots, \beta^m$. Enfin, comme c'est vrai pour tout $i \in \text{In}_\alpha$, on a $\alpha \leqslant \beta^1, \dots, \beta^m$. $\square$

Le lemme suivant montre que lorsqu'on sera passé au quotient sur **Ord**, l'axiome 10 sera satisfait.

**Lemme 4.4 (ax10).** Si $\alpha < \gamma$ et $\beta < \gamma$, alors $\sup(\alpha, \beta) < \gamma$.

**Démonstration.** Par définition, on a $\text{s}(\alpha, \beta) \leqslant \gamma$. Le lemme 4.1 donne $\sup(\alpha, \beta) < \text{s}(\alpha, \beta)$. Par transitivité, on obtient $\sup(\alpha, \beta) < \gamma$. $\square$

**Lemme 4.5.** Soient $n > 0$ et $\alpha^1, \dots, \alpha^n \in \text{ord}$. Il est impossible que, pour chaque $i \in [1..n]$, on ait $\alpha^i < \alpha^1, \dots, \alpha^n$.
Démonstration. On raisonne par induction. En utilisant l'affaiblissement, l'hypothèse donne des listes finies non toutes vides

$$
F_1 \subseteq_f \text{In}_{\alpha_1}, \dots, F_n \subseteq_f \text{In}_{\alpha_n},
$$

telles que

$$
\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n \text{ pour } i \in [1..m].
$$

En particulier, pour $j \in F_i$ (si $F_i$ est non vide) on a

$$
\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_n}^n.
$$

On est ramené à l'hypothèse avec la liste non vide $\alpha_{F_1}^1, \dots, \alpha_{F_n}^n$ qui remplace la liste $\alpha^1, \dots, \alpha^n$. $\square$

**Lemme 4.6.** Soient $\alpha^1, \dots, \alpha^n, \beta^1, \dots, \beta^m \in \text{ord} (n, m \ge 1)$.

1. Si $\alpha^i < \alpha^1, \dots, \alpha^n, \beta^1, \dots, \beta^m$ pour $i \in [1..n]$, alors $\alpha^i < \beta^1, \dots, \beta^m$ pour chaque $i$.

2. Soient $F_1 \subseteq_f \text{In}_{\alpha_1}, \dots, F_n \subseteq_f \text{In}_{\alpha_n}$. Si $\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m$ pour $i \in [1..n]$, alors $\alpha^i \le \beta^1, \dots, \beta^m$ pour chaque $i$.

Démonstration. 1. En utilisant l'affaiblissement, l'hypothèse donne des listes finies non toutes vides

$$
F_1 \subseteq_f \text{In}_{\alpha^1}, \dots, F_n \subseteq_f \text{In}_{\alpha^n}, G_1 \subseteq_f \text{In}_{\beta^1}, \dots, G_m \subseteq_f \text{In}_{\beta^m},
$$

telles que

$$
\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m \text{ pour } i \in [1..n]. \quad (*)
$$

On a alors pour $i \in [1..n]$ et $j \in \text{In}_{\alpha_i}$

$$
\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m.
$$

Fixons $i$ et $j$ : à fortiori, avec $F'_i = F_i \cup \{j\}$

$$
\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta_{G_1}^1, \dots, \beta_{G_m}^m.
$$

On a aussi par affaiblissement, pour $k \in [1..n]$ et $\ell \in F_k$,

$$
\alpha_{\ell}^{k} < \alpha_{F_1}^{1}, \dots, \alpha_{F_{i}}^{i}, \dots, \alpha_{F_{n}}^{n}, \beta_{G_1}^{1}, \dots, \beta_{G_{m}}^{m}.
$$

Donc par induction $\alpha_j^i < \beta_{G_1}^1, \dots, \beta_{G_m}^m$. Puisque $j$ est arbitraire, nous obtenons $\alpha^i \le \beta_{G_1}^1, \dots, \beta_{G_m}^m$. Ceci donne la conclusion cherchée, $\alpha^i < \beta^1, \dots, \beta^m$, si au moins une liste $G_k$ est non vide, Pour un $i \in [1..n]$ arbitraire. Si ce n'est pas le cas, (*) donne $\alpha^i \le \alpha_{F_1}^1, \dots, \alpha_{F_n}^n$ pour $i \in [1..n]$, avec des listes $F_i$ non toutes vides. Par définition, cela implique $\alpha^i < \alpha^1, \dots, \alpha^n$ pour $i \in [1..n]$, ce qui est impossible d'après le lemme 4.5.

2. On a pour $i \in [1..n]$ et $j \in \text{In}_{\alpha^i}$

$$
\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m.
$$

Fixons $i$ et $j$ : à fortiori, avec $F'_i = F_i \cup \{j\}$,

$$
\alpha_j^i < \alpha_{F_1}^1, \dots, \alpha_{F_i}^i, \dots, \alpha_{F_n}^n, \beta^1, \dots, \beta^m.
$$

On a aussi par affaiblissement, pour $k \in [1..n]$ et $\ell \in F_k$,

$$
\alpha_{\ell}^{k} < \alpha_{F_1}^{1}, \dots, \alpha_{F_{i}}^{i}, \dots, \alpha_{F_{n}}^{n}, \beta^{1}, \dots, \beta^{m}.
$$

Le point 1 donne alors $\alpha_j^i < \beta^1, \dots, \beta^m$. Comme $j$ est arbitraire, nous obtenons ce que nous voulons : $\alpha^i \le \beta^1, \dots, \beta^m$ pour un $i \in [1..n]$ arbitraire. $\square$

Le résultat suivant montre que les axiomes **11** et **12** seront valides quand on passera au quotient **Ord**.