Content deleted Content added
No edit summary |
|||
Line 444:
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.
== The Axiom of Counting and subversion of stratification ==
We now have two different implementations of the natural numbers in [[NFU]] (though
they are the same in [[ZFC]]: finite ordinals and finite cardinals. Each of these
supports the T operation in [[NFU]]. It is easy to prove that <math>T(n)</math> is
a natural number in [[NFU]] + Infinity + Choice (and so <math>|N|</math> and the first
infinite ordinal <math>\omega</math> are cantorian) but it is not possible to prove in
this theory that <math>T(n)=n</math>. However, common sense indicates that this should
be true, and we adopt this as an axiom:
*<strong>Rosser's Axiom of Counting</strong>: For each natural number n, <math>T(n)=n</math>.
One natural consequence of this axiom (and indeed its original formulation) is
*<math>|\{1,\ldots,n\}| = n</math> for each natural number n.
All that can be proved in [[NFU]] without Counting is <math>|\{1,\ldots,n\}| = T^2(n)</math>.
A consequence of Counting is that N is a strongly cantorian set (again, this is an equivalent
assertion).
Strongly cantorian sets have important properties which we review. The type of any variable
restricted to a strongly cantorian set A can be raised or lowered as desired by replacing
references to <math>a \in A</math> with references to <math>\bigcup f(a)</math> (type of a raised)
or <math>f^{-1}(\{a\}</math> (type of a lowered) where <math>f(a) = \{a\}</math> for all <math>a \in A</math>. Any subset of a strongly cantorian set is strongly cantorian. The power set of a strongly
cantorian set is strongly cantorian. The cartesian product of two strongly cantorian sets is strongly cantorian.
| |||