nLab plump ordinal

Plump ordinals




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Plump ordinals


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<BA\lt B refers to such an inclusion as the strict slice {y|y<x}\{ y | y \lt x \} of some element xx of BB.

In classical mathematics, <\lt and \le are definable in terms of each other’s negation: A<BA\lt B if and only if ¬(BA)\neg(B\le A), and similarly ABA\le B if and only if ¬(B<A)\neg(B\lt A). However, in constructive mathematics this is no longer true (although \leq can still be defined from <\lt in a more round-about way). 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:

  • xxx\le x.
  • Not x<xx \lt x.
  • If xyzx\le y\le z, then xzx\le z.
  • If x<yx\lt y, then xyx\le y.
  • If x<y<zx\lt y\lt z, then x<zx\lt z.
  • If x<yzx\lt y\le z, then x<zx\lt z.
  • If xy<zx\le y\lt z, then x<zx\lt z.

For the constructive ordinal numbers, these are all satisfied except for the last one. In fact, it’s easy to see that if xy<zx\le y\lt z implies x<zx\lt z for all x,y,zx,y,z, then excluded middle holds: consider z=2={0,1}z = 2 = \{0,1\} and y=1={0}y = 1 = \{0\} and x={0|P}x = \{0 | P\} for some proposition PP.

However, Paul Taylor (Taylor) realized that this last property can be recovered by essentially “restricting to the subclass of ordinals zz for which it holds hereditarily”. These are the plump ordinals.


An ordinal AA is plump if

  1. every ordinal B<AB\lt A is plump, and
  2. whenever CB<AC\le B\lt A and CC is a plump ordinal, then C<AC\lt A.

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


0=0 = \varnothing is trivially plump.

Since 00 is plump, 1=𝒫0={0}1 = \mathcal{P}0 = \{0\} is also plump.

More generally, any subset of 11 (which may be thought of as a truth value) is a plump ordinal.

But 2={0,1}2 = \{0,1\} (the set of classical truth values) with 0<10 \lt 1 is plump if and only if excluded middle holds.

In contrast, Ω=𝒫1\Omega = \mathcal{P}1 (the set of all truth values) with 0<10 \lt 1 (as the only instance of <{\lt}) is plump. So Ω\Omega is the plump version of 22, equal to 22 iff excluded middle holds.

The plump version of 33 may be quite large; it consists of all lower sets (downwards-closed collections) of truth values. So it includes 00, 11, and Ω\Omega, the other truth values between 00 and 11, the downset p{\downarrow}p (the lower set generated by pp) of any given truth value pp (not just 1=01 = {\downarrow}0 and Ω=1\Omega = {\downarrow}1), the lower set generated by two not-necessarily-comparable truth values pp and qq, etc. But if excluded middle holds, then it's just {0,1,2}\{0,1,2\}.

Generalizing most of these examples, if α\alpha is a plump ordinal, then the successor α +\alpha^+, consisting of all lower sets of α\alpha, is also a plump ordinal. This is bigger than α+1=α{α}\alpha + 1 = \alpha \cup \{\alpha\}, in that if 0<α0 \lt \alpha and α +=α+1\alpha^+ = \alpha + 1, then excluded middle holds.

Any downwards-closed subset of a plump ordinal is also a plump ordinal.


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

Last revised on September 23, 2023 at 03:18:47. See the history of this page for a list of all contributions to it.