Brouwer Ordinal

Definition

A Brouwer ordinal is an element of the quotient inductive type $\mathrm{Ord}$ defined by three constructors:

• $\mathsf{zero}:\mathrm{Ord}$, representing the ordinal $0$
• $\mathsf{suc}:\mathrm{Ord}\to \mathrm{Ord}$, representing the successor $\alpha +1$
• $\mathsf{lim}:(f:\mathbb{N}{\to }^{<}\mathrm{Ord})\to \mathrm{Ord}$, representing the supremum of a strictly monotone.

The $\mathsf{lim}$ constructor allows limit ordinals to be formed as the supremum of any countable sequence $f:\mathbb{N}\to \mathrm{Ord}$. For example, $\omega =\mathsf{lim}(\lambda n.\overline{n})$, where $\overline{n}$ denotes the $n$-fold application of $\mathsf{suc}$ to $\mathsf{zero}$.

Introduction Rules

$$\frac{}{\mathrm{Ord}:\mathcal{U}}\frac{\alpha ,\beta :\mathrm{Ord}}{\alpha \le \beta :\mathrm{Prop}}$$ $$\frac{}{0:\mathrm{Ord}}\frac{\alpha :\mathrm{Ord}}{{\alpha }^{+}:\mathrm{Ord}}\frac{\zeta :\mathbb{N}\to \mathrm{Ord}\forall i:\mathbb{N}.{\gamma }_i^{+}\le {\gamma }_{i+1}}{\zeta :\mathbb{N}{\to }^{<}\mathrm{Ord}}\frac{\zeta :\mathbb{N}{\to }^{<}\mathrm{Ord}}{{\lim }_i{\gamma }_i:\mathrm{Ord}}$$

For $\alpha ,\beta ,\gamma :\mathrm{Ord};\zeta ,\xi :\mathbb{N}{\to }^{<}\mathrm{Ord}$

$$\frac{}{0\le \alpha }\frac{\alpha \le \beta \beta \le \gamma }{\alpha \le \gamma }\frac{\alpha \le \beta }{{\alpha }^{+}\le {\beta }^{+}}$$ $$\frac{k:\mathbb{N}\alpha \le {\zeta }_k}{\alpha \le {\lim }_i\zeta }\frac{\forall i:\mathbb{N}.{\zeta }_i\le \alpha }{{\lim }_i\zeta \le \alpha }$$ $$\frac{\zeta ,\xi :\mathbb{N}{\to }^{<}\mathrm{Ord}\forall i.\exists j.:\mathbb{N}.{\zeta }_i\le {\xi }_j}{{\lim }_i{\zeta }_i\le {\lim }_i{\xi }_i}\frac{\alpha \le \beta \beta \le \alpha }{\alpha =\beta }$$

Algebra

An algebra on Brouwer Oridinals is given To prove a property $P:\mathrm{Ord}\to \mathcal{U}$ for all Brouwer ordinals, it suffices to provide:

• a proof of $P(\mathsf{zero})$
• a function $(\alpha :\mathrm{Ord})\to P(\alpha )\to P(\mathsf{suc}\alpha )$
• a function $(f:\mathbb{N}{\to }^{<}\mathrm{Ord})\to ((n:\mathbb{N})\to P(fn))\to P(\mathsf{lim}f)$

Relationship to Set-Theoretic Ordinals

Brouwer ordinals are an ordinal notation system rather than the von Neumann ordinals of classical set theory. They represent the countable ordinals (those below ${\omega }_1$, the first uncountable ordinal), but the representation is not unique: distinct terms can denote the same ordinal. For example, $\mathsf{lim}(\lambda n.\overline{n})$ and $\mathsf{lim}(\lambda n.\overline{n+1})$ both denote $\omega$.

Related Concepts

• Ordinal
• W Type
• Inductive Type
• Natural Number
• Equivalence Relation
• Constructive Mathematics