New Foundations

Article Index for New

Website Links For New

Information About New Foundations

	CATEGORIES ABOUT NEW FOUNDATIONS
	mathematical logic
	systems of set theory
	urelements
	logic

	APPAREL
	BABY
	BEAUTY
	BOOKS
	CAR TOYS
	CELL PHONES
	DVD'S
	ELECTRONICS
	GOURMET FOOD
	GROCERIES
	HEALTH & PERSONAL
	HOME & GARDEN
	JEWELRY
	MUSIC
	MUSIC INSTRUMENTS
	OFFICE PRODUCTS
	SOFTWARE
	SPORTING GOODS
	TOOLS & HARDWARE
	TOYS
	VIDEO GAMES
	SHOPPING HOME
	MORE SHOPPING...

THE TYPE THEORY TST The streamlined version of the theory of types (which we call TST) has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed, while for each (meta-) natural number ''n'', type ''n''+1 objects are understood to be sets of type ''n'' objects. The primitive predicates of this theory are equality and membership. Typing rules for well-formed atomic sentences are succinctly summed up in the formulas $x^\{n\}\; =\; y^\{n\}$ and $x^\{n\}\; \backslash in\; y^\{n+1\}$ (notation to be improved). The original type theory of the Principia Mathematica of Bertrand Russell and Alfred North Whitehead implemented a much more complex type system including types of relations with possibly heterogeneous argument types. In 1914, Norbert Wiener discovered that the Ordered Pair can be coded as a set, and so it is possible to eliminate relation types in favor of a linear hierarchy of types of sets as described here. The usual definition of the Ordered Pair as a set is not that of Norbert Wiener but a later one due to Kuratowski . In NF, one frequently uses another definition of Ordered Pair due to Quine . The axioms of the theory TST are Extensionality (sets of the same (positive) type with the same members are equal) and a Comprehension Schema : :$\backslash \{x^n\; \backslash mid\; \backslash phi(x^n)\backslash \}^\{n+1\}$ exists for any Well-formed Formula $\backslash phi(x^n)$: i.e., for any such formula $\backslash phi(x^n)$ there is a set $A^\{n+1\}$ such that for all $x^n,\; x^n\; \backslash in\; A^\{n+1\}\; \backslash leftrightarrow\; \backslash phi(x^n)$. DEFINITION OF NEW FOUNDATIONS; STRATIFICATION New Foundations (NF) is obtained from this theory by abandoning the distinctions of type. The axioms of this theory are extensionality (two objects with the same elements are the same object) and all those instances of comprehension obtained by dropping type indices (without introducing new identifications between variables) from an instance of comprehension of the streamlined type theory. It might seem that the resulting comprehension scheme would be the inconsistent scheme of $\backslash \{x\; \backslash mid\; x$ ot\in x\} is not constructed because there is no way to assign types consistently to all occurrences of ''x'' to obtain an instance of comprehension of the type theory. It is traditional to describe the if there is a function ''f'' from variables (considered as pieces of syntax) to natural numbers such that for any atomic subformula $x\; \backslash in\; y$ of $\backslash phi$ we have ''f''(''y'') = ''f''(''x'') + 1, while for any atomic subformula $x=y$ of $\backslash phi$, we have ''f''(''x'') = ''f''(''y''). The comprehension scheme for NF is the schema :$\backslash \{x\; \backslash mid\; \backslash phi\; \backslash \}$ exists for each stratified formula $\backslash phi$. Even the indirect reference to types in the notion of Stratification can be eliminated: NF comprehension is equivalent to a finite conjunction of its instances, so NF can be finitely axiomatized without any reference to types at all. LARGE SETS APPEAR It is notable that NF (and the theory NFU + Infinity + Choice described below, which is known to be consistent) allow the construction of "big" sets. For example, $x=x$ is a is an equivalence class of sets under the relation $A\; \backslash sim\; B$ defined as "there is a bijection between ''A'' and ''B''" and an Ordinal Number is an equivalence class of well-orderings under similarity. These definitions cannot be used in Zermelo Set Theory or its extensions because these classes are "too large". THE CONSISTENCY PROBLEM AND RELATED PARTIAL RESULTS The outstanding problem with this theory is the problem as to whether it is consistent. It is known that NF disproves Choice, and so proves Infinity (Specker, 1953). But it is also known ( Jensen , 1969) that the minor(?) modification of allowing Urelement s (objects which have no elements but which are distinct from the empty set and from one another) produces a theory NFU which is known to be consistent (weaker than arithmetic) and consistent with Infinity and Choice as well. (This corresponds to a type theory TSTU in which positive types may contain urelements.) Some other variations are known to be consistent. Specker has shown that NF is equiconsistent with TST + Amb, where Amb is the axiom scheme of typical ambiguity which asserts $\backslash phi\; \backslash leftrightarrow\; \backslash phi^+$ for any formula $\backslash phi$, $\backslash phi^+$ being the formula obtained by raising every type index in $\backslash phi$ by one, and also with the theory TST augmented with a "type shifting automorphism", an operation which raises type by one, mapping each type onto the next higher type, and preserves equality and membership relations (and which cannot be used in instances of comprehension: it is external to the theory). The same results hold for various fragments of TST in relation to corresponding fragments of NF. In the same year (1969) that Jensen showed consistency of NFU, Grishin showed the consistency of $NF\_3$, the fragment of NF with full extensionality (no urelements) and those instances of the comprehension axiom which can be stratified using just three types. This theory is a very awkward medium for mathematics (though some efforts have been made to investigate ways to do things in this environment) largely because there is no obvious definition for an Ordered Pair . In spite of this awkwardness, $NF\_3$ is very interesting, because every infinite model of TST restricted to three types satisfies the ambiguity scheme of the previous paragraph, and so for every such model there is a model of $NF\_3$ with the same theory. This is already false for four types: $NF\_4$ is the same theory as NF, and we have no idea how to get an ambiguous model of TST with four types. In 1983, Marcel Crabbé showed the consistency of the system NFI with unrestricted extensionality and those instances of the stratified comprehension axiom in which no variable is assigned a type higher than that of the set asserted to exist. This is a 's Principia Mathematica without the Axiom Of Reducibility . RESOLVING THE PARADOXES IN NF(U) We review the paradoxes of set theory and their resolution in NF, noting that although the consistency of NF remains an open question, these solutions to the paradoxes can be seen to work in NFU, which is known to be consistent. Relations and functions are defined in NF or NFU as sets of Ordered Pairs in the usual way. The Kuratowski ordered pair can be defined in this theory, but has the disadvantage that it is two types higher than its projections in TST, which means that a function is three types higher than the elements of its domain and range for purposes of stratification. If one can define a pair the same type as its arguments, then relations and functions are just one type higher than the elements of their domains and ranges. Such a pair is definable in NF (see the pair attributed to Rosser and Quine in the article on Ordered Pairs ), the existence of such a pair implies Infinity, and NFU + Infinity interprets NFU + "there is a type level ordered pair" (they are not quite the same theory, but the differences are inessential). NFU + Infinity + Choice proves the existence of a type level ordered pair. The choice of pair only occasionally makes a difference here. The Russell Paradox is easy: $x$ ot\in x is not a stratified formula, so the existence of $\backslash \{x\; \backslash mid\; x$ ot\in x\} is not asserted by any comprehension axiom of NF.
	We Introduce Some Useful Notions Peculiar To This Kind Of Set Theory A Set <math>A</math> Which Satisfies The Intuitively Appealing <math>A	P_1(A)</math> is said to be <strong>cantorian</strong>: a cantorian set satisfies the usual form of Cantor's Theorem A set <math>A</math> which satisfies the further condition that <math>(x \mapsto \{x\})\lceil A</math>, the restriction of the singleton map to <math>A</math>, is a set is clearly cantorian and is said to be <strong>strongly cantorian</strong>
	To See How Natural Numbers Are Defined In NFU, See	"http://wwwinformationdelightinfo/encyclopedia/entry/set-theoretic_definition_of_natural_numbers" class="copylinks">Set-theoretic Definition Of Natural Numbers The original form of this axiom given by Rosser was "the set <math>\{m \mid 1 \leq m \leq n\}</math> has ''n'' members", for each natural number ''n''" This intuitively obvious assertion is unstratified: what is provable in NFU is "the set <math>\{m \mid 1 \leq m \leq n\}</math> has <math>T^2(n)</math> members" (where the T operation on cardinals is defined by <math>T(A) = P_1(A)</math> this raises the type of a cardinal by one) For any cardinal number (including natural numbers) to assert <math>T(A) = A</math> is equivalent to asserting that the sets ''A'' of that cardinality are cantorian (by a usual abuse, we refer to such cardinals as "cantorian cardinals") It is straightforward to show that the assertion that each natural number is cantorian is equivalent to the assertion that the set of all natural numbers is strongly cantorian

The Axiom of Counting implies immediately that one does not need to assign types to variables restricted to the set $N$ of natural numbers for purposes of stratification; it is a theorem that the power set of a strongly cantorian set is strongly cantorian, so it is further not necessary to assign types to variables restricted to any iterated power set of the natural numbers, or to such familiar sets as the set of real numbers, the set of functions from reals to reals, and so forth. The set-theoretical strength of the Axiom of Counting is less
important in practice than the convenience of not having to annotate variables known to have natural number values (or related kinds of values) with singleton brackets or applications of the T operation in order to get stratified set definitions.

The Axiom of Counting implies Infinity; each of the axioms below needs to be adjoined to NFU + Infinity to get the effect of strong axioms of infinity; Ali Enayat has investigated the strength of some of these axioms in models of NFU + "the universe is finite".

A model of the kind constructed above satisfies the Axiom of Counting just in case the automorphism ''j'' fixes all natural numbers in the underlying nonstandard model of Zermelo set theory.

The next strong axiom we consider is the

• Axiom of strongly cantorian separation: For any strongly cantorian set ''A'' and any formula $\backslash phi$ (not necessarily stratified!) the set $\backslash \{x\; \backslash in\; A\; \backslash mid\; \backslash phi\backslash \}$ exists.

Immediate consequences of this include Mathematical Induction for unstratified conditions (which is not a consequence of Counting; many but not all unstratified instances of induction on the natural numbers follow from Counting).

• = NFU + Counting + Strongly Cantorian Separation is the same as that of Zermelo set theory + $\backslash Sigma\_2$ Replacement.

This axiom holds in a model of the kind constructed above (with Choice) if the ordinals which are fixed by ''j'' and dominate only ordinals fixed by ''j'' in the underlying nonstandard model of Zermelo set theory are standard, and the
power set of any such ordinal in the model is also standard. This is a sufficient condition, not a necessary one.

Next is

• Axiom of Cantorian Sets: Every cantorian set is strongly cantorian.

This very simple and appealing assertion is extremely strong. Solovay has shown the precise equivalence of the consistency strength of the theory NFUA = NFU + Infinity + Cantorian Sets with that of ZFC + the scheme asserting the existence of an ''n''-Mahlo cardinal for each concrete natural number ''n''. Ali Enayat has shown that the theory of cantorian equivalence classes of well-founded extensional relations (which gives a natural picture of an initial segment of the cumulative hierarchy of ZFC ) interprets the extension of ZFC with ''n''-Mahlo cardinals directly; a permutation technique can be applied to a model of this theory to give a model in which the hereditarily strongly cantorian sets with the usual membership relation model the strong extension of
ZFC .

This axiom holds in a model of the kind constructed above (with Choice) just in case the ordinals fixed by ''j'' in the underlying nonstandard model of Zermelo theory are an initial (proper class) segment of the ordinals of the model.

Next consider the

• Axiom of Cantorian Separation: For any cantorian set A and any formula $\backslash phi$ (not necessarily stratified!) the set $\backslash \{x\; \backslash in\; A\; \backslash mid\; \backslash phi\backslash \}$ exists.

This combines the effect of the two preceding axioms and is actually even stronger (we do not know exactly how strong). There is a proof by unstratified mathematical induction that there are ''n''-Mahlo cardinals for every ''n'', given the Axiom of Cantorian Sets, which gives an extension of ZFC which is even stronger than the previous
one (which only asserts that there are ''n''-Mahlos for each concrete natural number, leaving open the possibility of nonstandard counterexamples).

This axiom will hold in a model of the kind described above if every ordinal fixed by ''j'' is standard and every power set of an ordinal fixed by ''j'' is also standard in the underlying model of Zermelo set theory. This is again a sufficient but not a necessary condition.

An ordinal is said to be cantorian if it is fixed by T and strongly cantorian if it dominates only cantorian ordinals (this implies that it is itself cantorian). In models of the kind constructed above, cantorian ordinals of NFU correspond to ordinals fixed by ''j'' (they are not the same objects because different definitions of ordinal numbers are used in the two theories).

Equal in strength to the Axiom of Cantorian Sets is the

• Axiom of Large Ordinals: For each noncantorian ordinal $\backslash alpha$, there is a natural number ''n'' such that .

Recall that $\backslash Omega$ is the order type of the natural order on all ordinals. This only implies Cantorian Sets if we have Choice (but is at that level of consistency strength in any case). It is remarkable that one can even define $T^n(\backslash Omega)$: this is the ''n''th term $s\_n$ of any finite sequence of ordinals ''s'' of length ''n'' such that $s\_0\; =\; \backslash Omega$, $s\_\{i+1\}\; =\; T(s\_i)$ for each appropriate i. Note that
this is a completely unstratified definition. The uniqueness of $T^n(\backslash Omega)$ can be proved (for those n for which it exists) and a certain amount of common-sense reasoning about this notion can be carried out; enough to show that the Axiom implies Cantorian Sets in the presence of Choice. In spite of the knotty formal statement of this axiom, it is a very natural assumption, amounting to making the action of T on the ordinals as simple as possible.

A model of the kind constructed above will satisfy Large Ordinals if the ordinals moved by ''j'' are exactly the ordinals which dominate some $j^\{-i\}(\backslash alpha)$ in the underlying nonstandard model of Zermelo set theory.

• Axiom of Small Ordinals: For any formula $\backslash phi$, there is a set ''A'' such that the elements of ''A'' which are strongly cantorian ordinals are exactly the strongly cantorian ordinals such that $\backslash phi$.

Solovay has shown the precise equivalence in consistency strength of NFUB = NFU + Infinity + Cantorian Sets + Small Ordinals with Kelley-Morse Set Theory plus the assertion that the proper class ordinal (the class of all ordinals) is a Weakly Compact Cardinal . This is very strong indeed! The theory NFUB- which omits Cantorian Sets from the above is easily seen to have the same strength.

A model of the kind constructed above will satisfy this axiom if every collection of ordinals fixed by ''j'' is the intersection of some set of ordinals with the ordinals fixed by ''j'', in the underlying nonstandard model of Zermelo set theory.

Even stronger is the theory NFUM = NFU + Infinity + Large Ordinals + Small Ordinals. This is equivalent to Kelley-Morse Set Theory with a predicate on the classes which is a $\backslash kappa$-complete nonprincipal ultrafilter on the proper class ordinal $\backslash kappa$; in effect, this is Kelley-Morse Set Theory + "the proper class ordinal is a Measurable Cardinal "!

The technical details here are not the main point. The point is that seemingly reasonable assertions which suggest themselves naturally in the context of NFU turn out to be equivalent in power to very strong axioms of infinity in the ZFC context. A reason for this is seen in the correlation between the existence of models of NFU of the kind described above which satisfy these axioms and the existence of models of Zermelo set theory with automorphisms with special properties.


SEE ALSO

• Axiomatic Set Theory


• Positive Set Theory


• Alternative Set Theory


• Implementation Of Mathematics In Set Theory

EXTERNAL LINKS

• Bibliography of Set Theory with a Universal Set


• [http://math.boisestate.edu/~holmes/holmes/nf.html New Foundations Home Page]


• [http://math.boisestate.edu/~holmes/holmes/head.pdf Elementary Set Theory with a Universal Set] This is the online version of Randall Holmes's elementary set theory text in NFU. Holmes has permission from the publishers to provide access to this on the web.