Editing New Foundations (section)

===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}}