nLab plump ordinal

Plump ordinals

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Plump ordinals

Idea

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

Definition

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.

References

  • 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 February 23, 2014 at 07:43:56. See the history of this page for a list of all contributions to it.