natural number n, . One natural consequence of this axiom (and indeed its original formulation) is for each natural number n. All that can be proved in NFU without Counting is . A consequence of Counting is that N is a strongly cantorian set (again, this is an equivalent assertion). Properties of strongly cantorian sets The type of any variable restricted to a strongly cantorian set A can be raised or lowered as desired by replacing references to with references to (type of a raised; this presupposes that it is known that a is a set; otherwise one must say "the element of " to get this effect) or (type of a lowered) where for all , so it is not necessary to assign types to such variables for purposes of stratification. 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. Introducing the Axiom of Counting means that types need not be assigned to variables restricted to N or to P(N), R (the set of reals) or indeed any set ever considered in classical mathematics outside of set theory. There are no analogous phenomena in ZFC. See the main New Foundations article for stronger axioms that can be adjoined to NFU to enforce "standard" behavior of familiar mathematical objects. Familiar number systems: positive rationals, magnitudes, and reals Represent positive fractions as pairs of positive natural numbers (0 is excluded): is represented by the pair . To make , introduce the relation defined by . It is provable that this is an equivalence relation: define positive rational numbers as equivalence classes of pairs of positive natural numbers under this relation. Arithmetic operations on positive rational numbers and the order relation on positive rationals are defined just as in elementary school and proved (with some effort) to have the expected properties. Represent magnitudes (positive reals) as nonempty proper initial segments of the positive rationals with no largest element. The operations of addition and multiplication on magnitudes are implemented by elementwise addition of the positive rational elements of the magnitudes. Order is implemented as set inclusion. Represent real numbers as differences of magnitudes: formally speaking, a real number is an equivalence class of pairs of magnitudes under the equivalence relation defined by . The operations of addition and multiplication on