Editing New Foundations (section)

== Definition ==

The [[well-formed formulas]] of NF are the standard formulas of [[propositional calculus]] with two primitive predicates [[Equality (mathematics)#In logic|equality]] (<math>=</math>) and [[Set (mathematics)#Membership|membership]] (<math>\in</math>).  NF can be presented with only two axiom schemata:
* [[Extensionality]]: Two objects with the same elements are the same object; formally, given any set ''A'' and any set ''B'', if for every set ''X'', ''X'' is a member of ''A'' [[if and only if]] ''X'' is a member of ''B'', then ''A'' is [[equal (math)|equal]] to ''B''.
* A restricted [[axiom schema of comprehension]]: <math>\{x \mid \phi \}</math> exists for each [[stratified formula]] <math>\phi</math>.

A formula <math>\phi</math> is said to be ''stratified'' if there exists a [[function (mathematics)|function]] ''f'' from pieces of <math>\phi</math>'s syntax to the natural numbers, such that for any atomic subformula <math>x \in y</math> of <math>\phi</math> we have ''f''(''y'') = ''f''(''x'') + 1, while for any atomic subformula <math>x=y</math> of <math>\phi</math>, we have ''f''(''x'') = ''f''(''y''). 

===Finite axiomatization===

NF can be [[Axiom schema#Finite axiomatization|finitely axiomatized]].{{sfn|Hailperin|1944}} One advantage of such a finite axiomatization is that it eliminates the notion of [[stratification (mathematics)|stratification]]. The axioms in a finite axiomatization correspond to natural basic constructions, whereas stratified comprehension is powerful but not necessarily intuitive. In his introductory book, Holmes opted to take the finite axiomatization as basic, and prove stratified comprehension as a theorem.{{sfn|Holmes|1998|loc=chpt. 8}} The precise set of axioms can vary, but includes most of the following, with the others provable as theorems:{{sfn|Holmes|1998}}{{sfn|Hailperin|1944}}
<!-- both -->
* Extensionality: If <math>A</math> and <math>B</math> are sets, and for each object <math>x</math>, <math>x</math> is an element of <math>A</math> if and only if <math>x</math> is an element of <math>B</math>, then <math>A = B</math>.{{sfn|Holmes|1998|p=16}} This can also be viewed as defining the equality symbol.{{sfn|Hailperin|1944|loc=Definition 1.02 and Axiom PId}}<ref>For example [[W. V. O. Quine]], ''Mathematical Logic'' (1981) uses "three primitive notational devices: membership, joint denial, and quantification", then defines = in this fashion (pp.134–136)</ref>
* Singleton: For every object <math>x</math>, the set <math>\iota(x) = \{x\} = \{y | y = x\}</math> exists, and is called the singleton of <math>x</math>.{{sfn|Holmes|1998|p=25}}{{sfn|Fenton|2015|loc=ax-sn}}
* Cartesian Product: For any sets <math>A</math>, <math>B</math>, the set <math>A \times B = \{(a, b) | a \in A \text{ and } b \in B\}</math>, called the Cartesian product of <math>A</math> and <math>B</math>, exists.{{sfn|Holmes|1998|p=27}} This can be restricted to the existence of one of the cross products <math>A \times V</math> or <math>V \times B</math>.{{sfn|Hailperin|1944|p=10|loc=Axiom P5}}{{sfn|Fenton|2015|loc=ax-xp}}
* Converse: For each relation <math>R</math>, the set <math>R^{-1} = \{(x, y) | (y,x) \in R\}</math> exists; observe that <math>x R^{-1} y</math> exactly if <math>y R x</math>.{{sfn|Holmes|1998|p=31}}{{sfn|Hailperin|1944|p=10|loc=Axiom P7}}{{sfn|Fenton|2015|loc=ax-cnv}}
* Singleton Image: For any relation <math>R</math>, the set <math>R\iota = \{(\{x\}, \{y\}) | (x,y) \in R\}</math>, called the singleton image of <math>R</math>, exists.{{sfn|Holmes|1998|p=32}}{{sfn|Hailperin|1944|p=10|loc=Axiom P2}}{{sfn|Fenton|2015|loc=ax-si}}
* Domain: If <math>R</math> is a relation, the set <math>\text{dom}(R) = \{x | \exists y. (x,y) \in R\}</math>, called the domain of <math>R</math>, exists.{{sfn|Holmes|1998|p=31}} This can be defined using the operation of type lowering.{{sfn|Hailperin|1944|p=10}}
* Inclusion: The set <math>[\subseteq] = \{(x, y) | x \subseteq y\}</math> exists.{{sfn|Holmes|1998|p=44}} Equivalently, we may consider the set <math>[\in] = [\subseteq] \cap (1 \times V) = \{(\{x\}, y) | x \in y\}</math>.{{sfn|Hailperin|1944|p=10|loc=Axiom P9}}{{sfn|Fenton|2015|loc=ax-sset}}

* Complement: For each set <math>A</math>, the set <math>A^c = \{x | x \notin A\}</math>, called the complement of <math>A</math>, exists.{{sfn|Holmes|1998|p=19}}
* (Boolean) Union: If <math>A</math> and <math>B</math> are sets, the set <math>A \cup B = \{x | x \in A \text{ or } x \in B \text{ or both}\}</math>, called the (Boolean) union of <math>A</math> and <math>B</math>, exists.{{sfn|Holmes|1998|p=20}}
* Universal Set: <math>V = \{x | x = x\}</math> exists. It is straightforward that for any set <math>x</math>, <math>x \cup x^c = V</math>.{{sfn|Holmes|1998|p=19}}
* Ordered Pair: For each <math>a</math>, <math>b</math>, the ordered pair of <math>a</math> and <math>b</math>, <math>(a, b)</math>, exists; <math>(a, b) = (c, d)</math> exactly if <math>a = c</math> and <math>b = d</math>. This and larger tuples can be a definition rather than an axiom if an ordered pair construction is used.{{sfn|Holmes|1998|pp=26-27}}
* Projections: The sets <math>\pi_1 = \{((x, y), x) | x, y \in V \}</math> and <math>\pi_2 = \{((x, y), y) | x, y \in V \}</math> exist (these are the relations which an ordered pair has to its first and second terms, which are technically referred to as its projections).{{sfn|Holmes|1998|p=30}}
* Diagonal: The set <math>[=] = \{(x, x) | x \in V \}</math> exists, called the equality relation.{{sfn|Holmes|1998|p=30}}
* Set Union: If <math>A</math> is a set all of whose elements are sets, the set <math>\bigcup [A] = \{x | \text{for some } B, x \in B \text{ and } B \in A\}</math>, called the (set) union of <math>A</math>, exists.{{sfn|Holmes|1998|p=24}}
* Relative Product: If <math>R</math>, <math>S</math> are relations, the set <math>(R|S) = \{(x, y) | \text{for some } z, x R z \text{ and } z S y\}</math>, called the relative product of <math>R</math> and <math>S</math>, exists.{{sfn|Holmes|1998|p=31}}

* Anti-intersection: <math>x|y = \{z : \neg(z \in x \land z \in y) \}</math> exists. This is equivalent to complement and union together, with <math>x^c = x|x</math> and <math>x \cup y =x^c|y^c</math>.{{sfn|Fenton|2015|loc=ax-nin}}
* Cardinal one: The set <math>1</math> of all singletons, <math>\{ x | \exists y : (\forall w : w \in x \leftrightarrow w = y) \}</math>, exists.{{sfn|Hailperin|1944|p=10|loc=Axiom P8}}{{sfn|Fenton|2015|loc=ax-1c}}
* Tuple Insertions: For a relation <math>R</math>, the sets <math>I_2(R) = \{ (z, w, t) : (z, t) \in R \}</math> and <math>I_3(R) = \{ (z, w, t) : (z, w) \in R \}</math> exist.{{sfn|Hailperin|1944|p=10|loc=Axioms P3,P4}}{{sfn|Fenton|2015|loc=ax-ins2,ax-ins3}}
* Type lowering: For any set <math>S</math>, the set <math>\text{TL}(S) = \{ z : \forall w : (w, \{z\}) \in S \}</math> exists.{{sfn|Hailperin|1944|p=10|loc=Axiom P6}}{{sfn|Fenton|2015|loc=ax-typlower}}

=== Typed Set Theory ===
New Foundations is closely related to '''Russellian unramified typed set theory''' ('''TST'''), a streamlined version of the theory of types of ''Principia Mathematica'' with a linear hierarchy of types.  In this [[Structure (mathematical logic)#Many-sorted structures|many-sorted]] theory, each variable and set is assigned a type. It is customary to write the ''type indices'' as superscripts: <math>x^n</math> denotes a variable of type ''n''. Type 0 consists of individuals otherwise undescribed. For each (meta-) [[natural number]] ''n'', type ''n''+1 objects are sets of type ''n'' objects; objects connected by identity have equal types and sets of type ''n'' have members of type ''n''-1. The axioms of TST are extensionality, on sets of the same (positive) type, and comprehension, namely that if <math>\phi(x^n)</math>{{Hair space}}is a formula, then the set <math>\{x^n \mid \phi(x^n)\}^{n+1}\!</math> exists. In other words, given any formula <math>\phi(x^n)\!</math>, the formula <math>\exists A^{n+1} \forall x^n [ x^n \in A^{n+1} \leftrightarrow \phi(x^n) ]</math> is an axiom where <math>A^{n+1}\!</math> represents the set <math>\{x^n \mid \phi(x^n)\}^{n+1}\!</math> and is not [[Free variables and bound variables|free]] in <math>\phi(x^n)</math>. This type theory is much less complicated than the one first set out in the ''Principia Mathematica'', which included types for [[Relation (mathematics)|relations]] whose arguments were not necessarily all of the same types.

There is a correspondence between New Foundations and TST in terms of adding or erasing type annotations. In NF's comprehension schema, a formula is stratified exactly when the formula can be assigned types according to the rules of TST. This can be extended to map every NF formula to a set of corresponding TST formulas with various type index annotations. The mapping is one-to-many because TST has many similar formulas. For example, raising every type index in a TST formula by 1 results in a new, valid TST formula.

=== Tangled Type Theory ===

Tangled Type Theory (TTT) is an extension of TST where each variable is typed by an ordinal rather than a natural number. The well-formed atomic formulas are <math>x^{n} = y^{n}</math> and <math>x^{m} \in y^{n}</math> where <math>m<n</math>. The axioms of TTT are those of TST where each variable of type <math>i</math> is mapped to a variable <math>s(i)</math> where <math>s</math> is an increasing function.

TTT is considered a "weird" theory because each type is related to ''each'' lower type in the same way. For example, type 2 sets have both type 1 members and type 0 members, and extensionality axioms assert that a type 2 set is determined uniquely by ''either'' its type 1 members or its type 0 members. Whereas TST has natural models where each type <math>i + 1</math> is the power set of type <math>i</math>, in TTT each type is being interpreted as the power set of each lower type simultaneously. Regardless, a model of NF can be easily converted to a model of TTT, because in NF all the types are already one and the same. Conversely, with a more complicated argument, it can also be shown that the consistency of TTT implies the consistency of NF.{{sfn|Holmes|Wilshaw|2024}}

=== NFU and other variants ===
'''NF with [[urelement]]s''' ('''NFU''') is an important variant of NF due to Jensen{{sfn|Jensen|1969}} and clarified by Holmes.{{sfn|Holmes|1998}} Urelements are objects that are not sets and do not contain any elements, but can be contained in sets. One of the simplest forms of axiomatization of NFU regards urelements as multiple, unequal empty sets, thus weakening the extensionality axiom of NF to:
* Weak extensionality: Two ''non-empty'' objects with the same elements are the same object; formally,
:<math display="block">\forall x y w. (w \in x) \to (x = y \leftrightarrow (\forall z. z \in x \leftrightarrow z \in y)))</math>
In this axiomatization, the comprehension schema is unchanged, although the set <math>\{x \mid \phi(x)\}</math> will not be unique if it is empty (i.e. if <math>\phi(x)</math> is unsatisfiable).

However, for ease of use, it is more convenient to have a unique, "canonical" empty set. This can be done by introducing a sethood predicate <math>\mathrm{set}(x)</math> to distinguish sets from atoms. The axioms are then:{{sfn|Holmes|2001}}
* Sets: Only sets have members, i.e. <math>\forall x y. x \in y \to \mathrm{set}(y).</math>
* Extensionality: Two ''sets'' with the same elements are the same set, i.e. <math>\forall y z. (\mathrm{set}(y) \wedge \mathrm{set}(z) \wedge (\forall x. x \in y \leftrightarrow x \in z)) \to y = z.</math>
* Comprehension: The ''set'' <math>\{x \mid \phi(x) \}</math> exists for each stratified formula <math>\phi(x)</math>, i.e. <math>\exists A. \mathrm{set}(A) \wedge (\forall x. x \in A \leftrightarrow \phi(x)).</math>

NF<sub>3</sub> is the fragment of NF with full extensionality (no urelements) and those instances of comprehension which can be stratified using at most three types.  NF<sub>4</sub> is the same theory as NF.

Mathematical Logic (ML) is an extension of NF that includes proper classes as well as sets. ML was proposed by Quine and revised by Hao Wang, who proved that NF and the revised ML are equiconsistent.