From a constructive perspective, what are the ordinal numbers?

Question

From a constructive and computational perspective, what are the ordinal numbers?

On the one hand, it seems you can represent ordinal numbers symbolically using something like Cantor Normal Form notation. Then the ordinals are discrete, symbolic entities, and things like "$\leq$" become decidable.

On the other hand, you can represent the ordinals recursively as monotonically nondecreasing sequences of smaller ordinals, and then define an undecidable $\leq$ relation: An ordinal $(\alpha_i)$ is greater than or equal to $(\beta_i)$ if for every element of $\beta_j$ there is an element $\alpha_i$ such that $\alpha_i \geq \beta_j$. I struggle to see how this could be useful though.

nLab also mentions the Plump Ordinals, but I'm not sure what they are.

---

For an application, let $\mathrm{On}$, denote the class of all ordinals. Let $\alpha : \mathrm{On} \to \mathbb{R}$ be a mapping from $\mathrm{On}$ to real numbers. For any finite set $S = \{i_1, \ldots, i_n\} \subseteq \mathrm{On}$ where $i_1 < \cdots < i_n$, define the quantity $${\mathcal K}_S(\alpha) = \sqrt{\alpha_{i_1}^{2^1} + \sqrt{\alpha_{i_2}^{2^2} + \cdots \sqrt{\alpha_{i_n}^{2^n}}} }$$ Say that a real $\mathcal{K}(\alpha)$ is the limit of $S \mapsto \mathcal{K}_S(\alpha)$ when for every $\epsilon > 0$ there exists a finite $S \subseteq \mathrm{On}$ such that for all finite $T \subseteq \mathrm{On}$, if $S \subseteq T$ then $|\mathcal{K}_S(\alpha) - \mathcal{K}(\alpha)| < \epsilon$.

Examples:

• if $\alpha_n = 2$ then $\mathcal{K}(\alpha) = \sqrt{2^{2^1} + \sqrt{2^{2^2} + \sqrt{2^{2^3} + \dotsb}}} = 2\phi$ where $\phi$ is the Golden ratio.

• given $x \in \mathbb{R}$, take $$\alpha_n = \begin{cases} 1 & \text{if $n \neq \omega$,}\\ x & \text{if $n = \omega$} \end{cases}$$ Then $\mathcal{K}(\alpha)$ is the limit if the sequence $x, \sqrt{1+x^2}, \sqrt{1+\sqrt{1+x^4}}, \sqrt{1+\sqrt{1+\sqrt{1+x^8}}}, \ldots$. This is a continued radical which is "transfinite".

Answer 1

The ordinals in constructive mathematics are not as well-behaved as in classical mathematics. For example, if they are linearly ordered the excluded middle holds. There are appropriate substitutes, such as well-founded orders and inductive types. If you told us what you need the constructive ordinals for, we might be able to tell you what to use instead.

There are several possible definitions of ordinals which are classically equivalent but are intuitionistically distinct. For further reading I recommend the material available on Paul Taylor's web page summarizing his work on induction, recursion, replacement and the ordinals. Plump ordinals were defined in "Intuitionistic Sets and Ordinals", available on the web page.

Supplemental: If I understand your application correctly, then it has nothing to do with ordinal notations, ordinal representations, or intuitionistic ordinals. It is a case of the limit of a net from topology. Specifically, let $D$ be the set of all finite subsets of the index set $I$ of ordinals (from your application), ordered by $\subseteq$. Then $D$ is a directed set, and the number $\mathcal{K}(\alpha)$ is precisely the limit of the map $f : D \to \mathbb{R}$ defined by $f(S) = \mathcal{K}_S(\alpha)$.