How do set theories base on Intuitionistic Logic deal with ordinals?

Question

In my opinion, the notion of ordinals plays a key role in ZF set theory. A lot of important notions are defined by recursive on ordinals, like von Neumann hierarchy, Gödel's constructible universe. This makes me think that a set theory without the full force of ordinals will not be very useful. However, I also notice that in developing properties of ordinals the use of the law of excluded middle is crucial. Since Intuitionistic Logic reject the rule of excluded middle, I'm a bit curious that how do those set theories that are based on Intuitionistic Logic deal with ordinals?

Answer 1

In constructive set theory the most fruitful definition of ordinal is "a transitive set $x$ such that for all $y \in x$, y is also transitive." Note that in $\mathbf{ZF}$ this agrees with the usual definition. It's important to note that in intuitionistic set theory one still has $\in$-induction and can use it to define operations by recursion on ordinals.

Often in $\mathbf{ZF}$ definitions by recursion on ordinals are defined by splitting into two cases depending on whether an ordinal is a successor or a limit. However, this is often unnecessary and both cases can be combined into one. For example, in classical logic, one defines addition $\alpha + \beta$ by $\alpha + (\beta + 1) := (\alpha + \beta) + 1$ for successor and $\alpha + \lambda := \bigcup_{\beta < \lambda} (\alpha + \lambda)$ for limit. But you can also define $\alpha + \beta$ by $\alpha + \beta := \bigcup_{\gamma \in \beta} ((\alpha + \gamma) + 1)$. This works in intuitionistic logic and is equivalent to the usual definition in $\mathbf{ZF}$.

Alternatively, it is possible to use inductive definitions in place of ordinals for many proofs.

See Aczel and Rathjen, Constructive Set Theory. Ordinals are in section 9.4 and inductive definitions are in chapter 12.