3
$\begingroup$

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".

$\endgroup$
  • $\begingroup$ Somewhat related: mathoverflow.net/questions/325876/… $\endgroup$ – Gro-Tsen Apr 26 at 12:58
  • $\begingroup$ In a different world this would not be a research-level question. $\endgroup$ – Andrej Bauer Apr 26 at 13:23
  • 3
    $\begingroup$ @AndrejBauer, I'm sure it's clear to some, but not to me. What does your comment mean? That this should be common knowledge but isn't? $\endgroup$ – LSpice Apr 26 at 13:56
  • $\begingroup$ What does Cantor normal form have to do with decidability of $\leq$? $\endgroup$ – Ville Salo Apr 26 at 13:58
  • 1
    $\begingroup$ Does this answer your question? Ordinals in constructive mathematics ? (references) $\endgroup$ – Matt F. Apr 26 at 14:19
4
$\begingroup$

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)$.

| cite | improve this answer | |
$\endgroup$
  • 1
    $\begingroup$ OK, what about the representations I proposed in my question? $\endgroup$ – ogogmad Apr 26 at 20:32
  • 1
    $\begingroup$ From what I understand about your description of an application, you are not looking for any constructive ordinals. Are you familiar with general notions of convergence, such as net convergence and filter convergence? That's where you should be looking, as far as I can tell. $\endgroup$ – Andrej Bauer Apr 26 at 22:21
  • 1
    $\begingroup$ The purpose of using the ordinal numbers in my example was to define a transfinite sequence, not to define any kind of limit. That said, now I can see that I don't need the well-ordering property of the ordinals, and can just as well use any totally ordered set $\endgroup$ – ogogmad Apr 27 at 16:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.