basic constructions:
strong axioms
further
The ordinal numbers admit two inequalities: a strict one $\lt$ and a non-strict one $\le$. When the ordinals are defined in material set theory in the von Neumann style as “the set of all smaller ordinals”, these relations are identified with $\in$ (set membership?) and $\subseteq$ (containment). And when ordinals are defined in a structural theory as certain well-ordered sets, the relation $\le$ refers to inclusion as an initial subset? (a simulation) while $A\lt B$ refers to such an inclusion as the strict slice $\{ y | y \lt x \}$ of some element $x$ of $B$.
In classical mathematics, $\lt$ and $\le$ are definable in terms of each other’s negation: $A\lt B$ if and only if $\neg(B\le A)$, and similarly $A\le B$ if and only if $\neg(B\lt A)$. However, in constructive mathematics this is no longer true. This phenomenon occurs for other ordered structures as well; for instance, for the real numbers. (For the most commonly used notions of real number, $\le$ is definable as the negation of $\gt$, but not conversely.) In general, there are certain laws we may expect such a pair of inequalities to satisfy, such as:
For the constructive ordinal numbers, these are all satisfied except for the last one. In fact, it’s easy to see that if $x\le y\lt z$ implies $x\lt z$ for all $x,y,z$, then excluded middle holds: consider $z = 2 = \{0,1\}$ and $y = 1 = \{0\}$ and $x = \{0 | P\}$ for some proposition $P$.
However, Paul Taylor (Taylor) realized that this last property can be recovered by essentially “restricting to the subclass of ordinals $z$ for which it holds hereditarily”. These are the plump ordinals.
An ordinal $A$ is plump if
It is not obvious that this definition is sound (i.e. non-circular), but it can be shown to be so based on a well-founded relation (other than $A$ itself). It does, however, require the existence of power sets, so it is not obviously sensible in predicative mathematics which denies the existence of those.
Paul Taylor, Intuitionistic sets and ordinals, Journal of Symbolic Logic, 61:705-744, 1996, available here
See also Section 6.7 of Paul Taylor, Practical Foundations of Mathematics, here.