Set theory

From Wikipedia, the free encyclopedia

https://en.wikipedia.org/wiki/Set_theory 

A Venn diagram illustrating the intersection of two sets.

Set theory is a branch of mathematical logic that studies sets, which informally are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics. The language of set theory can be used to define nearly all mathematical objects.

The modern study of set theory was initiated by Georg Cantor and Richard Dedekind in the 1870s. After the discovery of paradoxes in naive set theory, such as Russell's paradox, numerous axiom systems were proposed in the early twentieth century, of which the Zermelo–Fraenkel axioms, with or without the axiom of choice, are the best-known.

Set theory is commonly employed as a foundational system for mathematics, particularly in the form of Zermelo–Fraenkel set theory with the axiom of choice. Beyond its foundational role, set theory is a branch of mathematics in its own right, with an active research community. Contemporary research into set theory includes a diverse collection of topics, ranging from the structure of the real number line to the study of the consistency of large cardinals.

History

Georg Cantor.

Mathematical topics typically emerge and evolve through interactions among many researchers. Set theory, however, was founded by a single paper in 1874 by Georg Cantor: "On a Property of the Collection of All Real Algebraic Numbers".

Since the 5th century BC, beginning with Greek mathematician Zeno of Elea in the West and early Indian mathematicians in the East, mathematicians had struggled with the concept of infinity. Especially notable is the work of Bernard Bolzano in the first half of the 19th century. Modern understanding of infinity began in 1870–1874 and was motivated by Cantor's work in real analysis. An 1872 meeting between Cantor and Richard Dedekind influenced Cantor's thinking and culminated in Cantor's 1874 paper. 

Cantor's work initially polarized the mathematicians of his day. While Karl Weierstrass and Dedekind supported Cantor, Leopold Kronecker, now seen as a founder of mathematical constructivism, did not. Cantorian set theory eventually became widespread, due to the utility of Cantorian concepts, such as one-to-one correspondence among sets, his proof that there are more real numbers than integers, and the "infinity of infinities" ("Cantor's paradise") resulting from the power set operation. This utility of set theory led to the article "Mengenlehre" contributed in 1898 by Arthur Schoenflies to Klein's encyclopedia.

The next wave of excitement in set theory came around 1900, when it was discovered that some interpretations of Cantorian set theory gave rise to several contradictions, called antinomies or paradoxes. Bertrand Russell and Ernst Zermelo independently found the simplest and best known paradox, now called Russell's paradox: consider "the set of all sets that are not members of themselves", which leads to a contradiction since it must be a member of itself and not a member of itself. In 1899 Cantor had himself posed the question "What is the cardinal number of the set of all sets?", and obtained a related paradox. Russell used his paradox as a theme in his 1903 review of continental mathematics in his The Principles of Mathematics.

In 1906 English readers gained the book Theory of Sets of Points by husband and wife William Henry Young and Grace Chisholm Young, published by Cambridge University Press. 

The momentum of set theory was such that debate on the paradoxes did not lead to its abandonment. The work of Zermelo in 1908 and the work of Abraham Fraenkel and Thoralf Skolem in 1922 resulted in the set of axioms ZFC, which became the most commonly used set of axioms for set theory. The work of analysts such as Henri Lebesgue demonstrated the great mathematical utility of set theory, which has since become woven into the fabric of modern mathematics. Set theory is commonly used as a foundational system, although in some areas—such as algebraic geometry and algebraic topology—category theory is thought to be a preferred foundation.

Basic concepts and notation

Set theory begins with a fundamental binary relation between an object o and a set A. If o is a member (or element) of A, the notation o ∈ A is used. A set is described by listing elements separated by commas, or by a characterizing property of its elements, within braces { }. Since sets are objects, the membership relation can relate sets as well.

A derived binary relation between two sets is the subset relation, also called set inclusion. If all the members of set A are also members of set B, then A is a subset of B, denoted A ⊆ B. For example, {1, 2} is a subset of {1, 2, 3} , and so is {2} but {1, 4} is not. As insinuated from this definition, a set is a subset of itself. For cases where this possibility is unsuitable or would make sense to be rejected, the term proper subset is defined. A is called a proper subset of B if and only if A is a subset of B, but A is not equal to B. Also 1, 2, and 3 are members (elements) of the set {1, 2, 3} but are not subsets of it; and in turn, the subsets, such as {1}, are not members of the set {1, 2, 3}.

Just as arithmetic features binary operations on numbers, set theory features binary operations on sets. The:

• Union of the sets A and B, denoted A ∪ B, is the set of all objects that are a member of A, or B, or both. The union of {1, 2, 3} and {2, 3, 4} is the set {1, 2, 3, 4} .
• Intersection of the sets A and B, denoted A ∩ B, is the set of all objects that are members of both A and B. The intersection of {1, 2, 3} and {2, 3, 4} is the set {2, 3} .
• Set difference of U and A, denoted U \ A, is the set of all members of U that are not members of A. The set difference {1, 2, 3} \ {2, 3, 4} is {1} , while, conversely, the set difference {2, 3, 4} \ {1, 2, 3} is {4} . When A is a subset of U, the set difference U \ A is also called the complement of A in U. In this case, if the choice of U is clear from the context, the notation A^c is sometimes used instead of U \ A, particularly if U is a universal set as in the study of Venn diagrams.
• Symmetric difference of sets A and B, denoted A △ B or A ⊖ B, is the set of all objects that are a member of exactly one of A and B (elements which are in one of the sets, but not in both). For instance, for the sets {1, 2, 3} and {2, 3, 4} , the symmetric difference set is {1, 4} . It is the set difference of the union and the intersection, (A ∪ B) \ (A ∩ B) or (A \ B) ∪ (B \ A).
• Cartesian product of A and B, denoted A × B, is the set whose members are all possible ordered pairs (a, b) where a is a member of A and b is a member of B. The cartesian product of {1, 2} and {red, white} is {(1, red), (1, white), (2, red), (2, white)}.
• Power set of a set A is the set whose members are all of the possible subsets of A. For example, the power set of {1, 2} is { {}, {1}, {2}, {1, 2} } .

Some basic sets of central importance are the empty set (the unique set containing no elements; occasionally called the null set though this name is ambiguous), the set of natural numbers, and the set of real numbers.

Some ontology

An initial segment of the von Neumann hierarchy.

A set is pure if all of its members are sets, all members of its members are sets, and so on. For example, the set {{}} containing only the empty set is a nonempty pure set. In modern set theory, it is common to restrict attention to the von Neumann universe of pure sets, and many systems of axiomatic set theory are designed to axiomatize the pure sets only. There are many technical advantages to this restriction, and little generality is lost, because essentially all mathematical concepts can be modeled by pure sets. Sets in the von Neumann universe are organized into a cumulative hierarchy, based on how deeply their members, members of members, etc. are nested. Each set in this hierarchy is assigned (by transfinite recursion) an ordinal number ${\displaystyle \alpha }$, known as its rank. The rank of a pure set ${\displaystyle X}$ is defined to be the least upper bound of all successors of ranks of members of ${\displaystyle X}$. For example, the empty set is assigned rank 0, while the set {{}} containing only the empty set is assigned rank 1. For each ordinal ${\displaystyle \alpha }$, the set ${\displaystyle V_{\alpha }}$ is defined to consist of all pure sets with rank less than ${\displaystyle \alpha }$. The entire von Neumann universe is denoted ${\displaystyle V}$.

Axiomatic set theory

Elementary set theory can be studied informally and intuitively, and so can be taught in primary schools using Venn diagrams. The intuitive approach tacitly assumes that a set may be formed from the class of all objects satisfying any particular defining condition. This assumption gives rise to paradoxes, the simplest and best known of which are Russell's paradox and the Burali-Forti paradox. Axiomatic set theory was originally devised to rid set theory of such paradoxes.

The most widely studied systems of axiomatic set theory imply that all sets form a cumulative hierarchy. Such systems come in two flavors, those whose ontology consists of:

• Sets alone. This includes the most common axiomatic set theory, Zermelo–Fraenkel set theory with the Axiom of Choice (ZFC). Fragments of ZFC include:
  • Zermelo set theory, which replaces the axiom schema of replacement with that of separation;
  • General set theory, a small fragment of Zermelo set theory sufficient for the Peano axioms and finite sets;
  • Kripke–Platek set theory, which omits the axioms of infinity, powerset, and choice, and weakens the axiom schemata of separation and replacement.
• Sets and proper classes. These include Von Neumann–Bernays–Gödel set theory, which has the same strength as ZFC for theorems about sets alone, and Morse–Kelley set theory and Tarski–Grothendieck set theory, both of which are stronger than ZFC.

The above systems can be modified to allow urelements, objects that can be members of sets but that are not themselves sets and do not have any members.

The New Foundations systems of NFU (allowing urelements) and NF (lacking them) are not based on a cumulative hierarchy. NF and NFU include a "set of everything, " relative to which every set has a complement. In these systems urelements matter, because NF, but not NFU, produces sets for which the axiom of choice does not hold.

Systems of constructive set theory, such as CST, CZF, and IZF, embed their set axioms in intuitionistic instead of classical logic. Yet other systems accept classical logic but feature a nonstandard membership relation. These include rough set theory and fuzzy set theory, in which the value of an atomic formula embodying the membership relation is not simply True or False. The Boolean-valued models of ZFC are a related subject.

An enrichment of ZFC called internal set theory was proposed by Edward Nelson in 1977.

Applications

Many mathematical concepts can be defined precisely using only set theoretic concepts. For example, mathematical structures as diverse as graphs, manifolds, rings, and vector spaces can all be defined as sets satisfying various (axiomatic) properties. Equivalence and order relations are ubiquitous in mathematics, and the theory of mathematical relations can be described in set theory.

Set theory is also a promising foundational system for much of mathematics. Since the publication of the first volume of Principia Mathematica, it has been claimed that most or even all mathematical theorems can be derived using an aptly designed set of axioms for set theory, augmented with many definitions, using first or second-order logic. For example, properties of the natural and real numbers can be derived within set theory, as each number system can be identified with a set of equivalence classes under a suitable equivalence relation whose field is some infinite set.

Set theory as a foundation for mathematical analysis, topology, abstract algebra, and discrete mathematics is likewise uncontroversial; mathematicians accept that (in principle) theorems in these areas can be derived from the relevant definitions and the axioms of set theory. Few full derivations of complex mathematical theorems from set theory have been formally verified, however, because such formal derivations are often much longer than the natural language proofs mathematicians commonly present. One verification project, Metamath, includes human-written, computer-verified derivations of more than 12,000 theorems starting from ZFC set theory, first-order logic and propositional logic.

Areas of study

Set theory is a major area of research in mathematics, with many interrelated subfields.

Combinatorial set theory

Combinatorial set theory concerns extensions of finite combinatorics to infinite sets. This includes the study of cardinal arithmetic and the study of extensions of Ramsey's theorem such as the Erdős–Rado theorem.

Descriptive set theory

Descriptive set theory is the study of subsets of the real line and, more generally, subsets of Polish spaces. It begins with the study of pointclasses in the Borel hierarchy and extends to the study of more complex hierarchies such as the projective hierarchy and the Wadge hierarchy. Many properties of Borel sets can be established in ZFC, but proving these properties hold for more complicated sets requires additional axioms related to determinacy and large cardinals.

The field of effective descriptive set theory is between set theory and recursion theory. It includes the study of lightface pointclasses, and is closely related to hyperarithmetical theory. In many cases, results of classical descriptive set theory have effective versions; in some cases, new results are obtained by proving the effective version first and then extending ("relativizing") it to make it more broadly applicable.

A recent area of research concerns Borel equivalence relations and more complicated definable equivalence relations. This has important applications to the study of invariants in many fields of mathematics.

Fuzzy set theory

In set theory as Cantor defined and Zermelo and Fraenkel axiomatized, an object is either a member of a set or not. In fuzzy set theory this condition was relaxed by Lotfi A. Zadeh so an object has a degree of membership in a set, a number between 0 and 1. For example, the degree of membership of a person in the set of "tall people" is more flexible than a simple yes or no answer and can be a real number such as 0.75.

Inner model theory

An inner model of Zermelo–Fraenkel set theory (ZF) is a transitive class that includes all the ordinals and satisfies all the axioms of ZF. The canonical example is the constructible universe L developed by Gödel. One reason that the study of inner models is of interest is that it can be used to prove consistency results. For example, it can be shown that regardless of whether a model V of ZF satisfies the continuum hypothesis or the axiom of choice, the inner model L constructed inside the original model will satisfy both the generalized continuum hypothesis and the axiom of choice. Thus the assumption that ZF is consistent (has at least one model) implies that ZF together with these two principles is consistent. 

The study of inner models is common in the study of determinacy and large cardinals, especially when considering axioms such as the axiom of determinacy that contradict the axiom of choice. Even if a fixed model of set theory satisfies the axiom of choice, it is possible for an inner model to fail to satisfy the axiom of choice. For example, the existence of sufficiently large cardinals implies that there is an inner model satisfying the axiom of determinacy (and thus not satisfying the axiom of choice).

Large cardinals

A large cardinal is a cardinal number with an extra property. Many such properties are studied, including inaccessible cardinals, measurable cardinals, and many more. These properties typically imply the cardinal number must be very large, with the existence of a cardinal with the specified property unprovable in Zermelo-Fraenkel set theory.

Determinacy

Determinacy refers to the fact that, under appropriate assumptions, certain two-player games of perfect information are determined from the start in the sense that one player must have a winning strategy. The existence of these strategies has important consequences in descriptive set theory, as the assumption that a broader class of games is determined often implies that a broader class of sets will have a topological property. The axiom of determinacy (AD) is an important object of study; although incompatible with the axiom of choice, AD implies that all subsets of the real line are well behaved (in particular, measurable and with the perfect set property). AD can be used to prove that the Wadge degrees have an elegant structure.

Forcing

Paul Cohen invented the method of forcing while searching for a model of ZFC in which the continuum hypothesis fails, or a model of ZF in which the axiom of choice fails. Forcing adjoins to some given model of set theory additional sets in order to create a larger model with properties determined (i.e. "forced") by the construction and the original model. For example, Cohen's construction adjoins additional subsets of the natural numbers without changing any of the cardinal numbers of the original model. Forcing is also one of two methods for proving relative consistency by finitistic methods, the other method being Boolean-valued models.

Cardinal invariants

A cardinal invariant is a property of the real line measured by a cardinal number. For example, a well-studied invariant is the smallest cardinality of a collection of meagre sets of reals whose union is the entire real line. These are invariants in the sense that any two isomorphic models of set theory must give the same cardinal for each invariant. Many cardinal invariants have been studied, and the relationships between them are often complex and related to axioms of set theory.

Set-theoretic topology

Set-theoretic topology studies questions of general topology that are set-theoretic in nature or that require advanced methods of set theory for their solution. Many of these theorems are independent of ZFC, requiring stronger axioms for their proof. A famous problem is the normal Moore space question, a question in general topology that was the subject of intense research. The answer to the normal Moore space question was eventually proved to be independent of ZFC.

Objections to set theory as a foundation for mathematics

From set theory's inception, some mathematicians have objected to it as a foundation for mathematics. The most common objection to set theory, one Kronecker voiced in set theory's earliest years, starts from the constructivist view that mathematics is loosely related to computation. If this view is granted, then the treatment of infinite sets, both in naive and in axiomatic set theory, introduces into mathematics methods and objects that are not computable even in principle. The feasibility of constructivism as a substitute foundation for mathematics was greatly increased by Errett Bishop's influential book Foundations of Constructive Analysis.

A different objection put forth by Henri Poincaré is that defining sets using the axiom schemas of specification and replacement, as well as the axiom of power set, introduces impredicativity, a type of circularity, into the definitions of mathematical objects. The scope of predicatively founded mathematics, while less than that of the commonly accepted Zermelo-Fraenkel theory, is much greater than that of constructive mathematics, to the point that Solomon Feferman has said that "all of scientifically applicable analysis can be developed [using predicative methods]".

Ludwig Wittgenstein condemned set theory philosophically for its connotations of Mathematical platonism. He wrote that "set theory is wrong", since it builds on the "nonsense" of fictitious symbolism, has "pernicious idioms", and that it is nonsensical to talk about "all numbers". Wittgenstein identified mathematics with algorithmic human deduction; the need for a secure foundation for mathematics seemed, to him, nonsensical. Moreover, since human effort is necessarily finite, Wittgenstein's philosophy required an ontological commitment to radical constructivism and finitism. Meta-mathematical statements — which, for Wittgenstein, included any statement quantifying over infinite domains, and thus almost all modern set theory — are not mathematics. Few modern philosophers have adopted Wittgenstein's views after a spectacular blunder in Remarks on the Foundations of Mathematics: Wittgenstein attempted to refute Gödel's incompleteness theorems after having only read the abstract. As reviewers Kreisel, Bernays, Dummett, and Goodstein all pointed out, many of his critiques did not apply to the paper in full. Only recently have philosophers such as Crispin Wright begun to rehabilitate Wittgenstein's arguments.

Category theorists have proposed topos theory as an alternative to traditional axiomatic set theory. Topos theory can interpret various alternatives to that theory, such as constructivism, finite set theory, and computable set theory. Topoi also give a natural setting for forcing and discussions of the independence of choice from ZF, as well as providing the framework for pointless topology and Stone spaces.

An active area of research is the univalent foundations and related to it homotopy type theory. Within homotopy type theory, a set may be regarded as a homotopy 0-type, with universal properties of sets arising from the inductive and recursive properties of higher inductive types. Principles such as the axiom of choice and the law of the excluded middle can be formulated in a manner corresponding to the classical formulation in set theory or perhaps in a spectrum of distinct ways unique to type theory. Some of these principles may be proven to be a consequence of other principles. The variety of formulations of these axiomatic principles allows for a detailed analysis of the formulations required in order to derive various mathematical results.

Set theory in mathematical education

As set theory gained popularity as a foundation for modern mathematics, there has been support for the idea of introducing basic theory, or naive set theory, early in mathematics education.

In the US in the 1960s, the New Math experiment aimed to teach basic set theory, among other abstract concepts, to primary grade students, but was met with much criticism. The math syllabus in European schools followed this trend, and currently includes the subject at different levels in all grades.

Set theory is used to introduce students to logical operators (NOT, AND, OR) and semantic or rule description (technically intensional definition) of sets, (e.g. "months starting with the letter A"). This may be useful when learning computer programming, as sets and boolean logic are basic building blocks of many programming languages.

Sets are commonly referred to when teaching about different types of numbers (N, Z, R, ...) and when defining mathematical functions as a relationship between two sets.

New Foundations

From Wikipedia, the free encyclopedia

https://en.wikipedia.org/wiki/New_Foundations 

 

In mathematical logic, New Foundations (NF) is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica. Quine first proposed NF in a 1937 article titled "New Foundations for Mathematical Logic"; hence the name. Much of this entry discusses NFU, an important variant of NF due to Jensen (1969) and exposited in Holmes (1998). In 1940 and in a revision of 1951, Quine introduced an extension of NF sometimes called "Mathematical Logic" or "ML", that included proper classes as well as sets.

New Foundations has a universal set, so it is a non-well-founded set theory. That is to say, it is an axiomatic set theory that allows infinite descending chains of membership such as … x_n ∈ x_n-1 ∈ … ∈ x₂ ∈ x₁. It avoids Russell's paradox by permitting only stratifiable formulas to be defined using the axiom schema of comprehension. For instance x ∈ y is a stratifiable formula, but x ∈ x is not (for details of how this works see below).

The type theory TST

The primitive predicates of Russellian unramified typed set theory (TST), a streamlined version of the theory of types, are equality (${\displaystyle =}$) and membership (${\displaystyle \in }$). TST has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed. For each (meta-) natural number n, type n+1 objects are sets of type n objects; sets of type n have members of type n-1. Objects connected by identity must have the same type. The following two atomic formulas succinctly describe the typing rules: ${\displaystyle x^{n}=y^{n}\!}$ and ${\displaystyle x^{n}\in y^{n+1}}$. (Quinean set theory seeks to eliminate the need for such superscripts.)

The axioms of TST are:

• Extensionality: sets of the same (positive) type with the same members are equal;
• An axiom schema of comprehension, namely:

If ${\displaystyle \phi (x^{n})}$ is a formula, then the set ${\displaystyle \{x^{n}\mid \phi (x^{n})\}^{n+1}\!}$ exists.

In other words, given any formula ${\displaystyle \phi (x^{n})\!}$, the formula ${\displaystyle \exists A^{n+1}\forall x^{n}[x^{n}\in A^{n+1}\leftrightarrow \phi (x^{n})]}$ is an axiom where ${\displaystyle A^{n+1}\!}$ represents the set ${\displaystyle \{x^{n}\mid \phi (x^{n})\}^{n+1}\!}$ and is not free in ${\displaystyle \phi (x^{n})}$.

This type theory is much less complicated than the one first set out in the Principia Mathematica, which included types for relations whose arguments were not necessarily all of the same type. In 1914, Norbert Wiener showed how to code the ordered pair as a set of sets, making it possible to eliminate relation types in favor of the linear hierarchy of sets described here.

Quinean set theory

Axioms and stratification

The well-formed formulas of New Foundations (NF) are the same as the well-formed formulas of TST, but with the type annotations erased. The axioms of NF are:

• Extensionality: Two objects with the same elements are the same object;
• A comprehension schema: All instances of TST Comprehension but with type indices dropped (and without introducing new identifications between variables).

By convention, NF's Comprehension schema is stated using the concept of stratified formula and making no direct reference to types. A formula ${\displaystyle \phi }$ is said to be stratified if there exists a function f from pieces of syntax to the natural numbers, such that for any atomic subformula ${\displaystyle x\in y}$ of ${\displaystyle \phi }$ we have f(y) = f(x) + 1, while for any atomic subformula ${\displaystyle x=y}$ of ${\displaystyle \phi }$, we have f(x) = f(y). Comprehension then becomes:

${\displaystyle \{x\mid \phi \}}$ exists for each stratified formula ${\displaystyle \phi }$.

Even the indirect reference to types implicit in the notion of stratification can be eliminated. Theodore Hailperin showed in 1944 that Comprehension is equivalent to a finite conjunction of its instances, so that NF can be finitely axiomatized without any reference to the notion of type. 

Comprehension may seem to run afoul of problems similar to those in naive set theory, but this is not the case. For example, the existence of the impossible Russell class ${\displaystyle \{x\mid x\not \in x\}}$ is not an axiom of NF, because ${\displaystyle x\not \in x}$ cannot be stratified.

Ordered pairs

Relations and functions are defined in TST (and in NF and NFU) as sets of ordered pairs in the usual way. The usual definition of the ordered pair, first proposed by Kuratowski in 1921, has a serious drawback for NF and related theories: the resulting ordered pair necessarily has a type two higher than the type of its arguments (its left and right projections). Hence for purposes of determining stratification, a function is three types higher than the members of its field. 

If one can define a pair in such a way that its type is the same type as that of its arguments (resulting in a type-level ordered pair), then a relation or function is merely one type higher than the type of the members of its field. Hence NF and related theories usually employ Quine's set-theoretic definition of the ordered pair, which yields a type-level ordered pair. Holmes (1998) takes the ordered pair and its left and right projections as primitive. Fortunately, whether the ordered pair is type-level by definition or by assumption (i.e., taken as primitive) usually does not matter.

The existence of a type-level ordered 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). Conversely, NFU + Infinity + Choice proves the existence of a type-level ordered pair.

Admissibility of useful large sets

NF (and NFU + Infinity + Choice, described below and known consistent) allow the construction of two kinds of sets that ZFC and its proper extensions disallow because they are "too large" (some set theories admit these entities under the heading of proper classes):

• The universal set V. Because ${\displaystyle x=x}$ is a stratified formula, the universal set V = {x | x=x} exists by Comprehension. An immediate consequence is that all sets have complements, and the entire set-theoretic universe under NF has a Boolean structure.
• Cardinal and ordinal numbers. In NF (and TST), the set of all sets having n elements (the circularity here is only apparent) exists. Hence Frege's definition of the cardinal numbers works in NF and NFU: a cardinal number is an equivalence class of sets under the relation of equinumerosity: the sets A and B are equinumerous if there exists a bijection between them, in which case we write ${\displaystyle A\sim B}$. Likewise, an ordinal number is an equivalence class of well-ordered sets.

Finite axiomatizability

New Foundations can be finitely axiomatized.

Cartesian closure

The category whose objects are the sets of NF and whose arrows are the functions between those sets is not Cartesian closed; Cartesian closure can be a useful property for a category of sets. Since NF lacks Cartesian closure, not every function curries as one might intuitively expect, and NF is not a topos.

The consistency problem and related partial results

For many years, the outstanding problem with NF has been that it has not conclusively been proved to be relatively consistent to any other well-known axiomatic system in which arithmetic can be modelled. NF disproves Choice, and thus proves Infinity (Specker, 1953). But it is also known (Jensen, 1969) that allowing urelements (multiple distinct objects lacking members) yields NFU, a theory that is consistent relative to Peano arithmetic; if Infinity and Choice are added, the resulting theory has the same consistency strength as type theory with infinity or bounded Zermelo set theory. (NFU corresponds to a type theory TSTU, where type 0 has urelements, not just a single empty set.) There are other relatively consistent variants of NF.

NFU is, roughly speaking, weaker than NF because in NF, the power set of the universe is the universe itself, while in NFU, the power set of the universe may be strictly smaller than the universe (the power set of the universe contains only sets, while the universe may contain urelements). In fact, this is necessarily the case in NFU+"Choice".

Specker has shown that NF is equiconsistent with TST + Amb, where Amb is the axiom scheme of typical ambiguity which asserts ${\displaystyle \phi \leftrightarrow \phi ^{+}}$ for any formula ${\displaystyle \phi }$, ${\displaystyle \phi ^{+}}$ being the formula obtained by raising every type index in ${\displaystyle \phi }$ by one. NF is also equiconsistent 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 the corresponding fragments of NF. 

In the same year (1969) that Jensen proved NFU consistent, Grishin proved ${\displaystyle NF_{3}}$ consistent. ${\displaystyle NF_{3}}$ is the fragment of NF with full extensionality (no urelements) and those instances of Comprehension which can be stratified using just three types. This theory is a very awkward medium for mathematics (although there have been attempts to alleviate this awkwardness), largely because there is no obvious definition for an ordered pair. Despite this awkwardness, ${\displaystyle NF_{3}}$ is very interesting because every infinite model of TST restricted to three types satisfies Amb. Hence for every such model there is a model of ${\displaystyle NF_{3}}$ with the same theory. This does not hold for four types: ${\displaystyle NF_{4}}$ is the same theory as NF, and we have no idea how to obtain a model of TST with four types in which Amb holds. 

In 1983, Marcel Crabbé proved consistent a system he called NFI, whose axioms are unrestricted extensionality and those instances of Comprehension in which no variable is assigned a type higher than that of the set asserted to exist. This is a predicativity restriction, though NFI is not a predicative theory: it admits enough impredicativity to define the set of natural numbers (defined as the intersection of all inductive sets; note that the inductive sets quantified over are of the same type as the set of natural numbers being defined). Crabbé also discussed a subtheory of NFI, in which only parameters (free variables) are allowed to have the type of the set asserted to exist by an instance of Comprehension. He called the result "predicative NF" (NFP); it is, of course, doubtful whether any theory with a self-membered universe is truly predicative. Holmes has  shown that NFP has the same consistency strength as the predicative theory of types of Principia Mathematica without the Axiom of reducibility.

Since 2015, several candidate proofs by Randall Holmes of the consistency of NF relative to ZF have been available both on arxiv and on the logician's home page. Holmes demonstrates the equiconsistency of a 'weird' variant of TST, namely TTT_λ - 'tangled type theory with λ-types' - with NF. Holmes next shows that TTT_λ is consistent relative to ZFA, that is, ZF with atoms but without choice. Holmes demonstrates this by constructing in ZFA+C, that is, ZF with atoms and choice, a class model of ZFA which includes 'tangled webs of cardinals' . The candidate proofs are all rather long, but no irrecoverable faults have been identified by the NF community as yet.

How NF(U) avoids the set-theoretic paradoxes

NF steers clear of the three well-known paradoxes of set theory. That NFU, a consistent (relative to Peano arithmetic) theory, also avoids the paradoxes may increase one's confidence in this fact.

The Russell paradox: An easy matter; ${\displaystyle x\not \in x}$ is not a stratified formula, so the existence of ${\displaystyle \{x\mid x\not \in x\}}$ is not asserted by any instance of Comprehension. Quine said that he constructed NF with this paradox uppermost in mind.

Cantor's paradox of the largest cardinal number exploits the application of Cantor's theorem to the universal set. Cantor's theorem says (given ZFC) that the power set ${\displaystyle P(A)}$ of any set ${\displaystyle A}$ is larger than ${\displaystyle A}$ (there can be no injection (one-to-one map) from ${\displaystyle P(A)}$ into ${\displaystyle A}$). Now of course there is an injection from ${\displaystyle P(V)}$ into ${\displaystyle V}$, if ${\displaystyle V}$ is the universal set! The resolution requires that one observes that ${\displaystyle |A|<|P(A)|}$ makes no sense in the theory of types: the type of ${\displaystyle P(A)}$ is one higher than the type of ${\displaystyle A}$. The correctly typed version (which is a theorem in the theory of types for essentially the same reasons that the original form of Cantor's theorem works in ZF) is ${\displaystyle |P_{1}(A)|<|P(A)|}$, where ${\displaystyle P_{1}(A)}$ is the set of one-element subsets of ${\displaystyle A}$. The specific instance of this theorem of interest is ${\displaystyle |P_{1}(V)|<|P(V)|}$: there are fewer one-element sets than sets (and so fewer one-element sets than general objects, if we are in NFU). The "obvious" bijection ${\displaystyle x\mapsto \{x\}}$ from the universe to the one-element sets is not a set; it is not a set because its definition is unstratified. Note that in all known models of NFU it is the case that ${\displaystyle |P_{1}(V)|<|P(V)|<<|V|}$; Choice allows one not only to prove that there are urelements but that there are many cardinals between ${\displaystyle |P(V)|}$ and ${\displaystyle |V|}$.

One can now introduce some useful notions. A set ${\displaystyle A}$ which satisfies the intuitively appealing ${\displaystyle |A|=|P_{1}(A)|}$ is said to be Cantorian: a Cantorian set satisfies the usual form of Cantor's theorem. A set ${\displaystyle A}$ which satisfies the further condition that ${\displaystyle (x\mapsto \{x\})\lceil A}$, the restriction of the singleton map to A, is a set is not only Cantorian set but strongly Cantorian.

The Burali-Forti paradox of the largest ordinal number goes as follows. Define (following naive set theory) the ordinals as equivalence classes of well-orderings under isomorphism. There is an obvious natural well-ordering on the ordinals; since it is a well-ordering it belongs to an ordinal ${\displaystyle \Omega }$. It is straightforward to prove (by transfinite induction) that the order type of the natural order on the ordinals less than a given ordinal ${\displaystyle \alpha }$ is ${\displaystyle \alpha }$ itself. But this means that ${\displaystyle \Omega }$ is the order type of the ordinals ${\displaystyle <\Omega }$ and so is strictly less than the order type of all the ordinals — but the latter is, by definition, ${\displaystyle \Omega }$ itself!

The solution to the paradox in NF(U) starts with the observation that the order type of the natural order on the ordinals less than ${\displaystyle \alpha }$ is of a higher type than ${\displaystyle \alpha }$. Hence a type level ordered pair is two types higher than the type of its arguments and the usual Kuratowski ordered pair four types higher. For any order type ${\displaystyle \alpha }$, we can define an order type ${\displaystyle \alpha }$ one type higher: if ${\displaystyle W\in \alpha }$, then ${\displaystyle T(\alpha )}$ is the order type of the order ${\displaystyle W^{\iota }=\{(\{x\},\{y\})\mid xWy\}}$. The triviality of the T operation is only a seeming one; it is easy to show that T is a strictly monotone (order preserving) operation on the ordinals. 

Now the lemma on order types may be restated in a stratified manner: the order type of the natural order on the ordinals ${\displaystyle <\alpha }$ is ${\displaystyle T^{2}(\alpha )}$ or ${\displaystyle T^{4}(\alpha )}$ depending on which pair is used (we assume the type level pair hereinafter). From this one may deduce that the order type on the ordinals ${\displaystyle <\Omega }$ is ${\displaystyle T^{2}(\Omega )}$, and thus ${\displaystyle T^{2}(\Omega )<\Omega }$. Hence the T operation is not a function; there cannot be a strictly monotone set map from ordinals to ordinals which sends an ordinal downward! Since T is monotone, we have ${\displaystyle \Omega >T^{2}(\Omega )>T^{4}(\Omega )\ldots }$, a "descending sequence" in the ordinals which cannot be a set.

One might assert that this result shows that no model of NF(U) is "standard", since the ordinals in any model of NFU are externally not well-ordered. One need not take a position on this, but can note that it is also a theorem of NFU that any set model of NFU has non-well-ordered "ordinals"; NFU does not conclude that the universe V is a model of NFU, despite V being a set, because the membership relation is not a set relation.

For a further development of mathematics in NFU, with a comparison to the development of the same in ZFC, see implementation of mathematics in set theory.

The system ML (Mathematical Logic)

ML is an extension of NF that includes proper classes as well as sets. The set theory of the 1940 first edition of Quine's Mathematical Logic married NF to the proper classes of NBG set theory, and included an axiom schema of unrestricted comprehension for proper classes. However J. Barkley Rosser (1942) proved that the system presented in Mathematical Logic was subject to the Burali-Forti paradox. This result does not apply to NF. Hao Wang (1950) showed how to amend Quine's axioms for ML so as to avoid this problem, and Quine included the resulting axiomatization in the 1951 second and final edition of Mathematical Logic.

Wang proved that if NF is consistent then so is the revised ML, and also showed that the revised ML can prove the consistency of NF, that is that NF and the revised ML are equiconsistent.

Models of NFU

There is a fairly simple method for producing models of NFU in bulk. Using well-known techniques of model theory, one can construct a nonstandard model of Zermelo set theory (nothing nearly as strong as full ZFC is needed for the basic technique) on which there is an external automorphism j (not a set of the model) which moves a rank ${\displaystyle V_{\alpha }}$ of the cumulative hierarchy of sets. We may suppose without loss of generality that ${\displaystyle j(\alpha )<\alpha }$. We talk about the automorphism moving the rank rather than the ordinal because we do not want to assume that every ordinal in the model is the index of a rank. 

The domain of the model of NFU will be the nonstandard rank ${\displaystyle V_{\alpha }}$. The membership relation of the model of NFU will be

• ${\displaystyle x\in _{NFU}y\equiv _{def}j(x)\in y\wedge y\in V_{j(\alpha )+1}.}$

It may now be proved that this actually is a model of NFU. Let ${\displaystyle \phi }$ be a stratified formula in the language of NFU. Choose an assignment of types to all variables in the formula which witnesses the fact that it is stratified. Choose a natural number N greater than all types assigned to variables by this stratification. 

Expand the formula ${\displaystyle \phi }$ into a formula ${\displaystyle \phi _{1}}$ in the language of the nonstandard model of Zermelo set theory with automorphism j using the definition of membership in the model of NFU. Application of any power of j to both sides of an equation or membership statement preserves its truth value because j is an automorphism. Make such an application to each atomic formula in ${\displaystyle \phi _{1}}$ in such a way that each variable x assigned type i occurs with exactly ${\displaystyle N-i}$ applications of j. This is possible thanks to the form of the atomic membership statements derived from NFU membership statements, and to the formula being stratified. Each quantified sentence ${\displaystyle (\forall x\in V_{\alpha }.\psi (j^{N-i}(x)))}$ can be converted to the form ${\displaystyle (\forall x\in j^{N-i}(V_{\alpha }).\psi (x))}$ (and similarly for existential quantifiers). Carry out this transformation everywhere and obtain a formula ${\displaystyle \phi _{2}}$ in which j is never applied to a bound variable. 

Choose any free variable y in ${\displaystyle \phi }$ assigned type i. Apply ${\displaystyle j^{i-N}}$ uniformly to the entire formula to obtain a formula ${\displaystyle \phi _{3}}$ in which y appears without any application of j. Now ${\displaystyle \{y\in V_{\alpha }\mid \phi _{3}\}}$ exists (because j appears applied only to free variables and constants), belongs to ${\displaystyle V_{\alpha +1}}$, and contains exactly those y which satisfy the original formula ${\displaystyle \phi }$ in the model of NFU. ${\displaystyle j(\{y\in V_{\alpha }\mid \phi _{3}\})}$ has this extension in the model of NFU (the application of j corrects for the different definition of membership in the model of NFU). This establishes that Stratified Comprehension holds in the model of NFU.

To see that weak Extensionality holds is straightforward: each nonempty element of ${\displaystyle V_{j(\alpha )+1}}$ inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.

The basic idea is that the automorphism j codes the "power set" ${\displaystyle V_{\alpha +1}}$ of our "universe" ${\displaystyle V_{\alpha }}$ into its externally isomorphic copy ${\displaystyle V_{j(\alpha )+1}}$ inside our "universe." The remaining objects not coding subsets of the universe are treated as urelements.

If ${\displaystyle \alpha }$ is a natural number n, one gets a model of NFU which claims that the universe is finite (it is externally infinite, of course). If ${\displaystyle \alpha }$ is infinite and the Choice holds in the nonstandard model of ZFC, one obtains a model of NFU + Infinity + Choice.

Self-sufficiency of mathematical foundations in NFU

For philosophical reasons, it is important to note that it is not necessary to work in ZFC or any related system to carry out this proof. A common argument against the use of NFU as a foundation for mathematics is that the reasons for relying on it have to do with the intuition that ZFC is correct. It is sufficient to accept TST (in fact TSTU). In outline: take the type theory TSTU (allowing urelements in each positive type) as a metatheory and consider the theory of set models of TSTU in TSTU (these models will be sequences of sets ${\displaystyle T_{i}}$ (all of the same type in the metatheory) with embeddings of each ${\displaystyle P(T_{i})}$ into ${\displaystyle P_{1}(T_{i+1})}$ coding embeddings of the power set of ${\displaystyle T_{i}}$ into ${\displaystyle T_{i+1}}$ in a type-respecting manner). Given an embedding of ${\displaystyle T_{0}}$ into ${\displaystyle T_{1}}$ (identifying elements of the base "type" with subsets of the base type), embeddings may be defined from each "type" into its successor in a natural way. This can be generalized to transfinite sequences ${\displaystyle T_{\alpha }}$ with care.

Note that the construction of such sequences of sets is limited by the size of the type in which they are being constructed; this prevents TSTU from proving its own consistency (TSTU + Infinity can prove the consistency of TSTU; to prove the consistency of TSTU+Infinity one needs a type containing a set of cardinality ${\displaystyle \beth _{\omega }}$, which cannot be proved to exist in TSTU+Infinity without stronger assumptions). Now the same results of model theory can be used to build a model of NFU and verify that it is a model of NFU in much the same way, with the ${\displaystyle T_{\alpha }}$'s being used in place of ${\displaystyle V_{\alpha }}$ in the usual construction. The final move is to observe that since NFU is consistent, we can drop the use of absolute types in our metatheory, bootstrapping the metatheory from TSTU to NFU.

Facts about the automorphism j

The automorphism j of a model of this kind is closely related to certain natural operations in NFU. For example, if W is a well-ordering in the nonstandard model (we suppose here that we use Kuratowski pairs so that the coding of functions in the two theories will agree to some extent) which is also a well-ordering in NFU (all well-orderings of NFU are well-orderings in the nonstandard model of Zermelo set theory, but not vice versa, due to the formation of urelements in the construction of the model), and W has type α in NFU, then j(W) will be a well-ordering of type T(α) in NFU. 

In fact, j is coded by a function in the model of NFU. The function in the nonstandard model which sends the singleton of any element of ${\displaystyle V_{j(\alpha )}}$ to its sole element, becomes in NFU a function which sends each singleton {x}, where x is any object in the universe, to j(x). Call this function Endo and let it have the following properties: Endo is an injection from the set of singletons into the set of sets, with the property that Endo( {x} ) = {Endo( {y} ) | y∈x} for each set x. This function can define a type level "membership" relation on the universe, one reproducing the membership relation of the original nonstandard model.

Strong axioms of infinity

In this section, the effect is considered of adding various "strong axioms of infinity" to our usual base theory, NFU + Infinity + Choice. This base theory, known consistent, has the same strength as TST + Infinity, or Zermelo set theory with Separation restricted to bounded formulas (Mac Lane set theory).

One can add to this base theory strong axioms of infinity familiar from the ZFC context, such as "there exists an inaccessible cardinal," but it is more natural to consider assertions about Cantorian and strongly Cantorian sets. Such assertions not only bring into being large cardinals of the usual sorts, but strengthen the theory on its own terms.

The weakest of the usual strong principles is:

• Rosser's Axiom of Counting. The set of natural numbers is a strongly Cantorian set.

To see how natural numbers are defined in NFU, see set-theoretic definition of natural numbers. The original form of this axiom given by Rosser was "the set {m|1≤m≤n} has n members", for each natural number n. This intuitively obvious assertion is unstratified: what is provable in NFU is "the set {m|1≤m≤n} has ${\displaystyle T^{2}(n)}$ members" (where the T operation on cardinals is defined by ${\displaystyle T(|A|)=|P_{1}(A)|}$; this raises the type of a cardinal by one). For any cardinal number (including natural numbers) to assert ${\displaystyle T(|A|)=|A|}$ is equivalent to asserting that the sets A of that cardinality are Cantorian (by a usual abuse of language, 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.

Counting is consistent with NFU, but increases its consistency strength noticeably; not, as one would expect, in the area of arithmetic, but in higher set theory. NFU + Infinity proves that each ${\displaystyle \beth _{n}}$ exists, but not that ${\displaystyle \beth _{\omega }}$ exists; NFU + Counting (easily) proves Infinity, and further proves the existence of ${\displaystyle \beth _{\beth _{n}}}$ for each n, but not the existence of ${\displaystyle \beth _{\beth _{\omega }}}$.

Counting implies immediately that one does not need to assign types to variables restricted to the set ${\displaystyle 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 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 to apply the T operation in order to get stratified set definitions.

Counting implies Infinity; each of the axioms below needs to be adjoined to NFU + Infinity to get the effect of strong variants 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 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 ${\displaystyle \phi }$ (not necessarily stratified!) the set {x∈A|φ} exists.

Immediate consequences 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). 

This axiom is surprisingly strong. Unpublished work of Robert Solovay shows that the consistency strength of the theory NFU* = NFU + Counting + Strongly Cantorian Separation is the same as that of Zermelo set theory + ${\displaystyle \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 condition is sufficient but not necessary.

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 + a schema 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 ZFC 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 ${\displaystyle \phi }$ (not necessarily stratified!) the set {x∈A|φ} exists.

This combines the effect of the two preceding axioms and is actually even stronger (precisely how is not known). Unstratified mathematical induction enables proving that there are n-Mahlo cardinals for every n, given Cantorian Sets, which gives an extension of ZFC that 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 ZFC. Again, this condition is sufficient but not necessary. 

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 Cantorian Sets is the

• Axiom of Large Ordinals: For each non-Cantorian ordinal ${\displaystyle \alpha }$, there is a natural number n such that ${\displaystyle T^{n}(\Omega )<\alpha }$.

Recall that ${\displaystyle \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 ${\displaystyle T^{n}(\Omega )}$: this is the nth term ${\displaystyle s_{n}}$ of any finite sequence of ordinals s of length n such that ${\displaystyle s_{0}=\Omega }$, ${\displaystyle s_{i+1}=T(s_{i})}$ for each appropriate i. This definition is completely unstratified. The uniqueness of ${\displaystyle T^{n}(\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 Large Ordinals 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 ${\displaystyle j^{-i}(\alpha )}$ in the underlying nonstandard model of ZFC.

• Axiom of Small Ordinals: For any formula φ, there is a set A such that the elements of A which are strongly Cantorian ordinals are exactly the strongly Cantorian ordinals such that φ.

Solovay has shown the precise equivalence in consistency strength of NFUB = NFU + Infinity + Cantorian Sets + Small Ordinals with Morse–Kelley 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! Moreover, NFUB-, which is NFUB with Cantorian Sets omitted, is easily seen to have the same strength as NFUB. 

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 ZFC.

Even stronger is the theory NFUM = NFU + Infinity + Large Ordinals + Small Ordinals. This is equivalent to Morse–Kelley set theory with a predicate on the classes which is a κ-complete nonprincipal ultrafilter on the proper class ordinal κ; in effect, this is Morse–Kelley set theory + "the proper class ordinal is a measurable cardinal"! 

The technical details here are not the main point, which is that reasonable and natural (in the context of NFU) assertions turn out to be equivalent in power to very strong axioms of infinity in the ZFC context. This fact is related to the correlation between the existence of models of NFU, described above and satisfying these axioms, and the existence of models of ZFC with automorphisms having special properties.