Content deleted Content added
No edit summary |
|||
Line 398:
With each infinite cardinal, many order types are associated for the usual reasons (in either
set theory).
Cantor's theorem shows (in both theories) that there are nontrivial distinctions between
infinite cardinal numbers. In [[ZFC]], one proves <math>|A|<|P(A)|</math>. In [[NFU]],
the usual form of Cantor's theorem is false (consider the case A=V), but Cantor's theorem
is an ill-typed statement. The correct form of the theorem in [[NFU]] is <math>|P_1(A)|<|P(A)|</math>, where <math>P_1(A)</math> is the set of one-element subsets of A.
<math>|P_1(V)|<|P(V)|</math> shows that there are "fewer" singletons than sets (the obvious
bijection <math>x \mapsto \{x\}</math> from <math>P_1(V)</math> to V has already been seen not
to be a set). It is actually provable in NFU + Choice that <math>|P_1(V)|<|P(V)|<<|V|</math>
(where << signals the existence of many intervening cardinals). We define a type-raising
T operation on cardinals analogous to the T operation on ordinals: <math>T(|A|) = |P_1(A)|</math>;
this is an external endomorphism of the cardinals just as the T operation on ordinals is an
external endomorphism of the ordinals.
The operations of cardinal arithmetic are defined in a set-theoretically motivated way in
Line 404 ⟶ 416:
one defines <math>|A|\cdot|B|</math> as <math>T^{-2}(|A \times B|)</math> because of the
type displacement of 2 between the pair and its projections, which implies a type displacement
of two between a cartesian product and its factors. It is
always exists (but requires attention because the inverse of T is not total).
Defining the exponential operation on cardinals requires T in an essential way: if we define <math>B^A</math>
as the collection of functions from A to B, we note that this is three types higher than A or B,
so it is reasonable to define <math>|B|^{|A|}</math> as <math>T^{-3}(|B^A|)</math> so that it
is the same type as A or B (<math>T^{-1}</math> replaces <math>T^{-3}</math> if we use a type-level pair). An effect of this is that the exponential operation is partial: for example, <math>2^|V|</math> is undefined.
Now the usual theorems of cardinal arithmetic with the axiom of choice can be proved, including
| |||