Implementation of mathematics in set theory: Difference between revisions

Revision as of 23:59, 21 December 2005

Revision as of 00:28, 22 December 2005

Line 440:

Now the usual theorems of cardinal arithmetic with the axiom of choice can be proved, including

<math>\kappa \cdot \kappa = \kappa</math>. From the case <math>|V|\cdot |V| = |V|</math>

we can derive the existence of a type level ordered pair: <math>|V| \cdot |V| = T^{-2}(|V \times V|)</math> is equal to <math>|V|</math> just in case <math>|V \times V| = T^2(|V|) = |P_1^2(V)|</math>, which would be witnessed by a one-to-one correspondence between Kuratowski pairs

we can derive the existence of a type level ordered pair.

<math>(a,b)</math> and double singletons <math>\{\{c\}\}</math>: redefine <math>(a,b)</math>

as the c such that <math>\{\{c\}\}</math> is associated with the Kuratowski <math>(a,b)</math>:

this is a type-level notion of ordered pair.