Content deleted Content added
Line 410:
this is an external endomorphism of the cardinals just as the T operation on ordinals is an
external endomorphism of the ordinals.
A set A is said to be <strong>cantorian</strong> just in case <strong>|A| = |P_1(A)| = T(|A|)</strong>; the cardinal <strong>|A|</strong> is also said to be a cantorian cardinal.
A set A is said to be <strong>strongly cantorian</strong> (and its cardinal to be strongly cantorian as well) just in case the restriction of
the singleton map to A (<math>(x \mapsto \{x\})\lceil A</math>)is a set. Well-orderings
of strongly cantorian sets are always strongly cantorian ordinals; this is not always true of
well-orderings of cantorian sets (though the shortest well-ordering of a cantorian set will
be cantorian). A cantorian set is a set which satisfies the usual form of Cantor's theorem.
The operations of cardinal arithmetic are defined in a set-theoretically motivated way in
Line 423 ⟶ 430:
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.
The exponential operation is total and behaves exactly as we expect on cantorian cardinals,
since T fixes such cardinals and it is easy to show that a function space between cantorian
sets is cantorian (as are power sets, cartesian products, and other usual type constructors).
Now the usual theorems of cardinal arithmetic with the axiom of choice can be proved, including
| |||