New Foundations Explorer Home Page  First > Last > 

Mirrors > Home > NFE Home > Th. List 
New Foundations (Wikipedia [external], Stanford Encyclopedia of Philosophy [external]) is an alternative set theory to the ZermeloFraenkel set theory presented in the regular Metamath Proof Explorer. Unlike the ZermeloFraenkel system with the Axiom of Choice (known as ZFC), New Foundations is a direct derivative of the set theory originally presented in Principia Mathematica. 
Contents of this page  Related pages External links 
In Principia Mathematica, Russell and Whitehead used a typing system to avoid the paradoxes of naive set theory, rather than restrict the size of sets (as ZermeloFraenkel theory does). This typing system was eventually refined by Russell down to Typed Set Theory (TST). In TST, unlimited comprehension is allowed (approximately, A ∈ V is a theorem). TST avoids the standard paradoxes by being a multisorted system. That is, there are variables of type 0, 1, 2,... The WFFs are restricted so that you must say x[n] = y[n] and x[n] ∈ y[n+1], where n is a variable type. This means, among other things, that x ∈ x is not a wellformed formula, so we can't even sensibly speak of the Russell class. Thus TST counters Russell's Paradox.
Now, consider introducing virtual classes into this theory. You need to say things like V[n] = { x[n]  x[n] = x[n] } for each type n. This leads to a "hall of mirrors" type situation: each named object is duplicated for each type.
Quine noticed this and proposed collapsing the whole theory into a onesorted set theory, where the comprehension axiom is restricted to formulas where you could theoretically introduce subscripts to make the formula a WFF of TST. Quine described this approach in a paper titled "New Foundations for Mathematical Logic," so this approach is now called "New Foundations" (NF) [Quine2]. For more details, see the Wikipedia article on NF.
The axioms begin with traditional axioms for classical first order logic with equality. See the regular Metamath Proof Explorer for discussions about these axioms and some of their implications.
The key axioms specific to NF are extensionality (two sets are identical if they contain the same elements) and a comprehension schema. Extensionality is formally defined as:
Name  Ref  Expression 

Axiom of Extensionality  axext  ⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y) 
The comprehension schema is stated using the concept of stratified formula; the approach is the Stratification Axiom from [Quine2]. In short, a wellformed formula using only propositional symbols, predicate symbols, and ∈ is "stratified" iff you can make a (metalogical) mapping from the variables to the natural numbers such that any formulas of the form x = y have the same number, and any formulas of the form x ∈ y have x as one less than y. Quine's stratification axiom states that there is a set corresponding to any stratified formula. We use Hailperin's axioms and prove existence of stratified sets using Hailperin's algorithm. Thus the stratification axiom of [Quine2] is implemented in this formalization using the axioms P1 through P9 from [Hailperin] and the Axiom of Singleton axsn:
Name  Ref  Expression (see link for any distinct variable requirements) 
Axiom of AntiIntersection (P1)  axnin  ⊢ ∃z∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y)) 
Axiom of Singleton Image (P2)  axsi  ⊢ ∃y∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x) 
Axiom of Singleton (not directly stated in Hailperin)  axsn  ⊢ ∃y∀z(z ∈ y ↔ z = x) 
Axiom of Insertion Two (P3)  axins2  ⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) 
Axiom of Insertion Three (P4)  axins3  ⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, w⟫ ∈ x) 
Axiom of Cross Product (P5)  axxp  ⊢ ∃y∀z(z ∈ y ↔ ∃w∃t(z = ⟪w, t⟫ ∧ t ∈ x)) 
Axiom of Type Lowering (P6)  axtyplower  ⊢ ∃y∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x) 
Axiom of Converse (P7)  axcnv  ⊢ ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x) 
Axiom of Cardinal One (P8)  ax1c  ⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)) 
Axiom of Subset Relationship (P9)  axsset  ⊢ ∃x∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z)) 
The usual definition of the ordered pair, first proposed by Kuratowski in 1921 and used in the regular Metamath Proof Explorer, has a serious drawback for NF and related theories that use stratification. The Kuratowski ordered pair is defined as << x , y >> = { { x } , { x , y } }. This leads to the ordered pair having a type two greater than its arguments. For example, z in << << x , y >> , z >> would have a different type than x and y, which makes multiargument functions extremely awkward to work with. Operations such as "1st" and complex "+" would not form sets in NF with the Kuratowski ordered pairs.
In contrast, the Quine definition of ordered pairs, defined in definition dfop, is type level. That is, <. x , y >. has the same type as x and y, which means that the same holds of <. <. x , y >. , z >. This means that "1st" is a set with the Quine definition, as is complex "+". The Kuratowski ordered pair is defined (as dfopk), because it is a simple definition that can be used by the set construction axioms that follow it, but for typical uses the Quine definition of ordered pairs dfop is used instead.
Perhaps one of the most remarkable aspects of NF is that the Axiom of Choice (an axiom of the widelyused ZFC system) can be disproven in NF, a result proven in [Specker]. As a corollary, NF proves infinity.
There are several systems related to NF. In particular, NFU is a small modification of NF that also allows urelements (multiple distinct objects lacking members). NFU corresponds to a modified type theory TSTU, where type 0 has urelements, not just a single empty set. NFU is consistent with both Infinity and Choice, so both can be added to NFU. NFU + Infinity + Choice has the same consistency strength as the theory of types with the Axiom of Infinity. NFU + Infinity + Choice has been extended further, e.g., with various strong axioms of infinity (similar to ways that ZFC has been extended). Randall Holmes states that "Extensions of NFU are adequate vehicles for mathematics in a basically familiar style". NFU is not further discussed here.
A fair amount of the definitions and theorems (notably the ones on boolean set operations) are taken verbatim from the regular Metamath Proof Explorer source file set.mm (based on ZFC). This also follows the development in [Rosser] fairly closely. An unusual aspect is the stratified Traising function TcFn. The work to specifically formalize New Foundations in metamath was originally created by Scott Fenton. Those who are interested in New Foundations may want to look at the New Foundations home page, as well as a proof of the consistency of New Foundations by Randall Holmes. The descriptions given here are based on a discussion on the metamath mailing list.
This
page was last updated on 28May2018. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 