Content deleted Content added
Line 354:
order type of <math>W^{\iota}=\{(\{x\},\{y\})\mid xWy\}</math> for any <math>W \in \alpha</math> (it is easy to show that this does not depend on the choice of W; note that T raises type by one). Thus the order type of the ordinals less than
<math>\Omega</math> with the natural order is <math>T^4(\Omega)</math>, and <math>T^4(\Omega)<\Omega</math>. All uses of <math>T^4</math> here can be replaced with <math>T^2</math> if a type-level pair is used.
This shows that the T operation is nontrivial, which has a number of interesting consequences.
It follows immediately that the singleton map <math>x \mapsto \{x\}</math> is not a set, as otherwise
restrictions of this map would establish the similarity of W and <math>W^{\iota}</math> for any
well-ordering W. T is (externally) bijective and order-preserving. Because of this, the fact
<math>T^4(\Omega)</math> establishes that <math>\Omega > T(\Omega) > T^2(\Omega) \ldots</math>
is a "descending sequence" in the ordinals which cannot be a set.
Ordinals fixed by T are called <strong>cantorian</strong> ordinals, and ordinals which
dominate only cantorian ordinals (which are easily shown to be cantorian themselves) are said to be <strong>strongly cantorian</strong>. The motivation for these definitions will be clearer in the next section.
It is possible to reason about von Neumann ordinals in [[NFU]]. Recall that a von Neumann ordinal
is a transitive set A such that the restriction of membership to A is a strict well-ordering.
This is quite a strong condition in the [[NFU]] context, since the membership relation involves
a difference of type. A von Neumann ordinal A is not an ordinal in the sense of [[NFU]],
but <math>\in\lceil A</math> belongs to an ordinal <math>\alpha</math> which may be termed
the order type of (membership on) A.
| |||