Home Page - New Foundations Explorer

Created by Scott Fenton

New Foundations Proof Explorer

New Foundations (Wikipedia [external], Stanford Encyclopedia of Philosophy [external]) is an alternative set theory to the Zermelo-Fraenkel set theory presented in the regular Metamath Proof Explorer. Unlike the Zermelo-Fraenkel 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 Stratification The axioms Some theorems Bibliography

Related pages Table of Contents and Theorem List Bibliographic Cross-Reference Definition List ASCII Equivalents for Text-Only Browsers Metamath database nf.mm (ASCII file) External links GitHub repository

Stratification

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 Zermelo-Fraenkel theory does). This typing system was eventually refined by Russell down to Typed Set Theory (TST). In TST, unlimited comprehension is allowed (approximately, A e. _V is a theorem). TST avoids the standard paradoxes by being a multi-sorted 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] e. y[n+1], where n is a variable type. This means, among other things, that x e. x is not a well-formed 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 one-sorted 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

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:

Extensionality

Name	Ref	Expression
Axiom of Extensionality	ax-ext	|- (A.z(z e. x <-> z e. 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 well-formed formula using only propositional symbols, predicate symbols, and e. 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 e. 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 ax-sn:

New Foundations Stratification Axioms

Name	Ref	Expression (see link for any distinct variable requirements)
Axiom of Anti-Intersection (P1)	ax-nin	|- E.zA.w(w e. z <-> (w e. x -/\ w e. y))
Axiom of Singleton Image (P2)	ax-si	|- E.yA.zA.w(<<{z}, {w}>> e. y <-> <<z, w>> e. x)
Axiom of Singleton (not directly stated in Hailperin)	ax-sn	|- E.yA.z(z e. y <-> z = x)
Axiom of Insertion Two (P3)	ax-ins2	|- E.yA.zA.wA.t(<<{{z}}, <<w, t>>>> e. y <-> <<z, t>> e. x)
Axiom of Insertion Three (P4)	ax-ins3	|- E.yA.zA.wA.t(<<{{z}}, <<w, t>>>> e. y <-> <<z, w>> e. x)
Axiom of Cross Product (P5)	ax-xp	|- E.yA.z(z e. y <-> E.wE.t(z = <<w, t>> /\ t e. x))
Axiom of Type Lowering (P6)	ax-typlower	|- E.yA.z(z e. y <-> A.w<<w, {z}>> e. x)
Axiom of Converse (P7)	ax-cnv	|- E.yA.zA.w(<<z, w>> e. y <-> <<w, z>> e. x)
Axiom of Cardinal One (P8)	ax-1c	|- E.xA.y(y e. x <-> E.zA.w(w e. y <-> w = z))
Axiom of Subset Relationship (P9)	ax-sset	|- E.xA.yA.z(<<y, z>> e. x <-> A.w(w e. y -> w e. 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 multi-argument 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 df-op, 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 df-opk), 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 df-op is used instead.

Perhaps one of the most remarkable aspects of NF is that the Axiom of Choice (an axiom of the widely-used 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 T-raising 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.

Some theorems

Proof of Principia Mathematica's version of 1+1=2

Proof of the Axiom of Infinity

Russell's Paradox

Proof that the universal class exists

Disproof of the Axiom of Choice

Bibliography   

1. [BellMachover] Bell, J. L., and M. Machover, A Course in Mathematical Logic, North-Holland, Amsterdam (1977) [QA9.B3953].
2. [ChoquetDD] Choquet-Bruhat, Yvonne and Cecile DeWitt-Morette, with Margaret Dillard-Bleick, Analysis, Manifolds and Physics, Elsevier Science B.V., Amsterdam (1982) [QC20.7.A5C48 1981].
3. [Eisenberg] Eisenberg, Murray, Axiomatic Theory of Sets and Classes, Holt, Rinehart and Winston, Inc., New York (1971) [QA248.E36].
4. [Enderton] Enderton, Herbert B., Elements of Set Theory, Academic Press, Inc., San Diego, California (1977) [QA248.E5].
5. [Gleason] Gleason, Andrew M., Fundamentals of Abstract Analysis, Jones and Bartlett Publishers, Boston (1991) [QA300.G554].
6. [Hailperin] Hailperin, Theodore, "A Set of Axioms for Logic," Journal of Symbolic Logic, 9:1-14 (1944) [BC1.J6].
7. [Hamilton] Hamilton, A. G., Logic for Mathematicians, Cambridge University Press, Cambridge, revised edition (1988) [QA9.H298 1988].
8. [Hitchcock] Hitchcock, David, The peculiarities of Stoic propositional logic, McMaster University; available at http://www.humanities.mcmaster.ca/~hitchckd/peculiarities.pdf (retrieved 3 Jul 2016).
9. [Holmes] Holmes, Robert, Elementary Set Theory With a Universal Set, Web. Accessed 23 Feb 2015. Link
10. [Jech] Jech, Thomas, Set Theory, Academic Press, San Diego (1978) [QA248.J42].
11. [KalishMontague] Kalish, D. and R. Montague, "On Tarski's formalization of predicate logic with identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:81-101 (1965) [QA.A673].
12. [Kunen] Kunen, Kenneth, Set Theory: An Introduction to Independence Proofs, Elsevier Science B.V., Amsterdam (1980) [QA248.K75].
13. [KuratowskiMostowski] Kuratowski, K. and A. Mostowski, Set Theory: with an Introduction to Descriptive Set Theory, 2nd ed., North-Holland, Amsterdam (1976) [QA248.K7683 1976].
14. [Levy] Levy, Azriel, Basic Set Theory, Dover Publications, Mineola, N.Y. (2002) [QA248.L398 2002].
15. [Lopez-Astorga] Lopez-Astorga, Miguel, "The First Rule of Stoic Logic and its Relationship with the Indemonstrables", Revista de Filosofía Tópicos (2016); available at http://www.scielo.org.mx/pdf/trf/n50/n50a1.pdf (retrieved 3 Jul 2016).
16. [Margaris] Margaris, Angelo, First Order Mathematical Logic, Blaisdell Publishing Company, Waltham, Massachusetts (1967) [QA9.M327].
17. [Megill] Megill, N., "A Finitely Axiomatized Formalization of Predicate Calculus with Equality," Notre Dame Journal of Formal Logic, 36:435-453 (1995) [QA.N914]; available at http://projecteuclid.org/euclid.ndjfl/1040149359 (accessed 11 Nov 2014); the PDF preprint has the same content (with corrections) but pages are numbered 1-22, and the database references use the numbers printed on the page itself, not the PDF page numbers.
18. [Mendelson] Mendelson, Elliott, Introduction to Mathematical Logic, 2nd ed., D. Van Nostrand (1979) [QA9.M537].
19. [Monk1] Monk, J. Donald, Introduction to Set Theory, McGraw-Hill, Inc. (1969) [QA248.M745].
20. [Monk2] Monk, J. Donald, "Substitutionless Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:103-121 (1965) [QA.A673].
21. [Pfenning] Pfenning, Frank, Automated Theorem Proving, Carnegie-Mellon University (April 13, 2004); available at http://www.cs.cmu.edu/~fp/courses/atp/handouts/atp.pdf and http://web.archive.org/web/20160304013704/http://www.cs.cmu.edu/~fp/courses/atp/handouts/atp.pdf (retrieved 7 Feb 2017).
22. [Quine] Quine, Willard van Orman, Set Theory and Its Logic, Harvard University Press, Cambridge, Massachusetts, revised edition (1969) [QA248.Q7 1969].
23. [Quine2] Quine, W.V., 1937a, "New Foundations for Mathematical Logic," American Mathematical Monthly, 44: 70-80 (1937) [QA1.A515].
24. [Rosser] Rosser, John B., Logic for Mathematicians, Dover Publications, Mineola, N.Y. (2008) [BC135.R58 2008].
25. [Sanford] Sanford, David H., If P, then Q: Conditionals and the Foundations of Reasoning, 2nd ed., Routledge Taylor & Francis Group (2003); ISBN 0-415-28369-8; available at https://books.google.com/books?id=h_AUynB6PA8C&pg=PA39#v=onepage&q&f=false (retrieved 3 Jul 2016).
26. [Schechter] Schechter, Eric, Handbook of Analysis and Its Foundations, Academic Press, San Diego (1997) [QA300.S339].
27. [Specker] Specker, E.P., "The axiom of choice in Quine's new foundations for mathematical logic," Proceedings of the National Academy of Sciences of the USA, 39:972-975 (1953) [Q11.N26]
28. [Stoll] Stoll, Robert R., Set Theory and Logic, Dover Publications, Inc. (1979) [QA248.S7985 1979].
29. [Suppes] Suppes, Patrick, Axiomatic Set Theory, Dover Publications, Inc. (1972) [QA248.S959].
30. [TakeutiZaring] Takeuti, Gaisi, and Wilson M. Zaring, Introduction to Axiomatic Set Theory, Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
31. [Tarski] Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79 (1965) [QA.A673].
32. [WhiteheadRussell] Whitehead, Alfred North, and Bertrand Russell, Principia Mathematica to *56, Cambridge University Press, Cambridge, 1962 [QA9.W592 1962].