New Foundations#Cartesian Closure
{{Short description|Axiomatic set theory devised by W.V.O. Quine}}
In mathematical logic, New Foundations (NF) is a non-well-founded, finitely axiomatizable set theory conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica.
Definition
The well-formed formulas of NF are the standard formulas of propositional calculus with two primitive predicates equality () and membership (). 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 to B.
- A restricted axiom schema of comprehension: exists for each stratified formula .
A formula is said to be stratified if there exists a function f from pieces of 's syntax to the natural numbers, such that for any atomic subformula of we have f(y) = f(x) + 1, while for any atomic subformula of , we have f(x) = f(y).
=Finite axiomatization=
NF can be finitely axiomatized.{{sfn|Hailperin|1944}} One advantage of such a finite axiomatization is that it eliminates the notion of 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}}
- Extensionality: If and are sets, and for each object , is an element of if and only if is an element of , then .{{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}}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)
- Singleton: For every object , the set exists, and is called the singleton of .{{sfn|Holmes|1998|p=25}}{{sfn|Fenton|2015|loc=ax-sn}}
- Cartesian Product: For any sets , , the set , called the Cartesian product of and , exists.{{sfn|Holmes|1998|p=27}} This can be restricted to the existence of one of the cross products or .{{sfn|Hailperin|1944|p=10|loc=Axiom P5}}{{sfn|Fenton|2015|loc=ax-xp}}
- Converse: For each relation , the set exists; observe that exactly if .{{sfn|Holmes|1998|p=31}}{{sfn|Hailperin|1944|p=10|loc=Axiom P7}}{{sfn|Fenton|2015|loc=ax-cnv}}
- Singleton Image: For any relation , the set , called the singleton image of , exists.{{sfn|Holmes|1998|p=32}}{{sfn|Hailperin|1944|p=10|loc=Axiom P2}}{{sfn|Fenton|2015|loc=ax-si}}
- Domain: If is a relation, the set , called the domain of , exists.{{sfn|Holmes|1998|p=31}} This can be defined using the operation of type lowering.{{sfn|Hailperin|1944|p=10}}
- Inclusion: The set exists.{{sfn|Holmes|1998|p=44}} Equivalently, we may consider the set .{{sfn|Hailperin|1944|p=10|loc=Axiom P9}}{{sfn|Fenton|2015|loc=ax-sset}}
- Complement: For each set , the set , called the complement of , exists.{{sfn|Holmes|1998|p=19}}
- (Boolean) Union: If and are sets, the set , called the (Boolean) union of and , exists.{{sfn|Holmes|1998|p=20}}
- Universal Set: exists. It is straightforward that for any set , .{{sfn|Holmes|1998|p=19}}
- Ordered Pair: For each , , the ordered pair of and , , exists; exactly if and . 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 and 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 exists, called the equality relation.{{sfn|Holmes|1998|p=30}}
- Set Union: If is a set all of whose elements are sets, the set , called the (set) union of , exists.{{sfn|Holmes|1998|p=24}}
- Relative Product: If , are relations, the set , called the relative product of and , exists.{{sfn|Holmes|1998|p=31}}
- Anti-intersection: exists. This is equivalent to complement and union together, with and .{{sfn|Fenton|2015|loc=ax-nin}}
- Cardinal one: The set of all singletons, , exists.{{sfn|Hailperin|1944|p=10|loc=Axiom P8}}{{sfn|Fenton|2015|loc=ax-1c}}
- Tuple Insertions: For a relation , the sets and exist.{{sfn|Hailperin|1944|p=10|loc=Axioms P3,P4}}{{sfn|Fenton|2015|loc=ax-ins2,ax-ins3}}
- Type lowering: For any set , the set 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 many-sorted theory, each variable and set is assigned a type. It is customary to write the type indices as superscripts: 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 {{Hair space}}is a formula, then the set exists. In other words, given any formula , the formula is an axiom where represents the set and is not free in . 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 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 and where
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
= NFU and other variants =
NF with urelements (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,
:
In this axiomatization, the comprehension schema is unchanged, although the set
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
- Sets: Only sets have members, i.e.
\forall x y. x \in y \to \mathrm{set}(y). - Extensionality: Two sets with the same elements are the same set, i.e.
\forall y z. (\mathrm{set}(y) \wedge \mathrm{set}(z) \wedge (\forall x. x \in y \leftrightarrow x \in z)) \to y = z. - Comprehension: The set
\{x \mid \phi(x) \} exists for each stratified formula\phi(x) , i.e.\exists A. \mathrm{set}(A) \wedge (\forall x. x \in A \leftrightarrow \phi(x)).
NF3 is the fragment of NF with full extensionality (no urelements) and those instances of comprehension which can be stratified using at most three types. NF4 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.
Constructions
This section discusses some problematic constructions in NF. 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.
= Ordered pairs =
Relations and functions are defined in TST (and in NF and NFU) as sets of ordered pairs in the usual way. For purposes of stratification, it is desirable that a relation or function is merely one type higher than the type of the members of its field. This requires defining the ordered pair so that its type is the same as that of its arguments (resulting in a type-level ordered pair). The usual definition of the ordered pair, namely
As an alternative approach, Holmes{{sfn|Holmes|1998}} takes the ordered pair (a, b) as a primitive notion, as well as its left and right projections
= Natural numbers and the axiom of infinity =
The usual form of the axiom of infinity is based on the von Neumann construction of the natural numbers, which is not suitable for NF, since the description of the successor operation (and many other aspects of von Neumann numerals) is necessarily unstratified. The usual form of natural numbers used in NF follows Frege's definition, i.e., the natural number n is represented by the set of all sets with n elements. Under this definition, 0 is easily defined as
Since inductive sets always exist, the set of natural numbers
Finite sets can then be defined as sets that belong to a natural number. However, it is not trivial to prove that
It may intuitively seem that one should be able to prove Infinity in NF(U) by constructing any "externally" infinite sequence of sets, such as
However, there are some cases where Infinity can be proven (in which cases it may be referred to as the theorem of infinity):
- In NF (without urelements), Specker{{sfn|Specker|1953}} has shown that the axiom of choice is false. Since it can be proved through induction that every finite set has a choice function (a stratified condition), it follows that
V is infinite. - In NFU with axioms asserting the existence of a type-level ordered pair,
V is equinumerous with its proper subsetV \times \{0\} , which implies Infinity.{{sfn|Holmes|1998|loc=sec. 12.1}} Conversely, NFU + Infinity + Choice proves the existence of a type-level ordered pair.{{Citation needed|date=July 2020|reason=I searched for quite a while and was unable to find a source for this statement. It is repeated in several online sources, but without proof or reference.}} NFU + Infinity interprets NFU + "there is a type-level ordered pair" (they are not quite the same theory, but the differences are inessential).{{Citation needed|date=March 2023|reason=What does the word "interpret" mean here?}}
Stronger axioms of infinity exist, such as that the set of natural numbers is a strongly Cantorian set, or NFUM = NFU + Infinity + Large Ordinals + Small Ordinals which is equivalent to Morse–Kelley set theory plus a predicate on proper classes which is a κ-complete nonprincipal ultrafilter on the proper class ordinal κ.{{cite journal |last1=Holmes |first1=M. Randall |title=Strong axioms of infinity in NFU |journal=Journal of Symbolic Logic |date=March 2001 |volume=66 |issue=1 |pages=87–116 |doi=10.2307/2694912 |jstor=2694912 |url=https://randall-holmes.github.io/Papers/nfumcorrected.pdf}}
= 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
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
A \sim B . Likewise, an ordinal number is an equivalence class of well-ordered sets.
= Cartesian closure =
The category whose objects are the sets of NF and whose arrows are the functions between those sets is not Cartesian closed;{{sfn|Forster|2007}} Since NF lacks Cartesian closure, not every function curries as one might intuitively expect, and NF is not a topos.
Resolution of set-theoretic paradoxes
NF 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
= Russell's paradox =
The resolution of Russell's paradox is trivial:
= Cantor's paradox and Cantorian sets =
Cantor's paradox boils down to the question of whether there exists a largest cardinal number, or equivalently, whether there exists a set with the largest cardinality. In NF, the universal set
Of course there is an injection from
This failure is not surprising since
The usual way to correct such a type problem is to replace
However, unlike in TST,
= {{Anchor|Burali-Forti paradox}}Burali-Forti paradox and the T operation =
The Burali-Forti paradox of the largest ordinal number is resolved in the opposite way: In NF, having access to the set of ordinals does not allow one to construct a "largest ordinal number". One can construct the ordinal
To formalize the Burali-Forti paradox in NF, it is necessary to first formalize the concept of ordinal numbers. In NF, ordinals are defined (in the same way as in naive set theory) as equivalence classes of well-orderings under isomorphism. This is a stratified definition, so the set of ordinals
However, the statement "
To correct such a type problem, one needs the T operation,
:The order type of the natural order on the ordinals
Both versions of this statement can be proven by transfinite induction; we assume the type level pair hereinafter. This means that
Another (stratified) statement that can be proven by transfinite induction is that T is a strictly monotone (order-preserving) operation on the ordinals, i.e.,
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. This is a philosophical question, not a question of what can be proved within the formal theory. Note that even within NFU it can be proven that any set model of NFU has non-well-ordered "ordinals"; NFU does not conclude that the universe
Consistency
Some mathematicians had questioned the consistency of NF, partly because it is not clear why it avoids the known paradoxes. A key issue was that Specker proved NF combined with the Axiom of Choice is inconsistent. The proof is complex and involves T-operations. However, since 2010, Holmes has claimed to have shown that NF is consistent relative to the consistency of standard set theory (ZFC). In 2024, Sky Wilshaw confirmed Holmes' proof using the Lean proof assistant.{{cite web |last1=Smith |first1=Peter |title=NF really is consistent |url=https://www.logicmatters.net/2024/04/21/nf-really-is-consistent/ |website=Logic Matters |date=21 April 2024 |access-date=21 April 2024}}
Although NFU resolves the paradoxes similarly to NF, it has a much simpler consistency proof. The proof can be formalized within Peano Arithmetic (PA), a theory weaker than ZF that most mathematicians accept without question. This does not conflict with Gödel's second incompleteness theorem because NFU does not include the Axiom of Infinity and therefore PA cannot be modeled in NFU, avoiding a contradiction. PA also proves that NFU with Infinity and NFU with both Infinity and Choice are equiconsistent with TST with Infinity and TST with both Infinity and Choice, respectively. Therefore, a stronger theory like ZFC, which proves the consistency of TST, will also prove the consistency of NFU with these additions.{{sfn|Jensen|1969}} In simpler terms, NFU is generally seen as weaker than NF because, in NFU, the collection of all sets (the power set of the universe) can be smaller than the universe itself, especially when urelements are included, as required by NFU with Choice.
= Models of NFU =
Jensen's proof gives 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
The domain of the model of NFU will be the nonstandard rank
It may now be proved that this actually is a model of NFU. Let
To see that weak Extensionality holds is straightforward: each nonempty element of
If
= 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
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
= 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
History
In 1914, Norbert Wiener showed how to code the ordered pair as a set of sets, making it possible to eliminate the relation types of Principia Mathematica in favor of the linear hierarchy of sets in TST. The usual definition of the ordered pair was first proposed by Kuratowski in 1921. Willard Van Orman Quine first proposed NF as a way to avoid the "disagreeable consequences" of TST in a 1937 article titled New Foundations for Mathematical Logic; hence the name. Quine extended the theory in his book Mathematical Logic, whose first edition was published in 1940. In the book, Quine introduced the system "Mathematical Logic" or "ML", an extension of NF that included proper classes as well as sets. The first edition's set theory 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 proved that the system was subject to the Burali-Forti paradox.{{sfn|Rosser|1942}} Hao Wang showed how to amend Quine's axioms for ML so as to avoid this problem.{{sfn|Wang|1950}} Quine included the resulting axiomatization in the second and final edition, published in 1951.
In 1944, Theodore Hailperin showed that Comprehension is equivalent to a finite conjunction of its instances,{{sfn|Hailperin|1944}} In 1953, Ernst Specker showed that the axiom of choice is false in NF (without urelements).{{sfn|Specker|1953}} In 1969, Jensen showed that adding urelements to NF yields a theory (NFU) that is provably consistent.{{sfn|Jensen|1969}} That same year, Grishin proved NF3 consistent.{{sfn|Grishin|1969}} Specker additionally showed that NF is equiconsistent with TST plus the axiom scheme of "typical ambiguity".{{cn|date=April 2024}} NF is also equiconsistent with TST augmented with a "type shifting automorphism", an operation (external to the theory) which raises type by one, mapping each type onto the next higher type, and preserves equality and membership relations.{{cn|date=April 2024}}
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.{{According to whom|date=April 2024}} Holmes has {{date?}} shown that NFP has the same consistency strength as the predicative theory of types of Principia Mathematica without the axiom of reducibility.
The Metamath database implemented Hailperin's finite axiomatization for New Foundations.{{sfn|Fenton|2015}} Since 2015, several candidate proofs by Randall Holmes of the consistency of NF relative to ZF were available both on arXiv and on the logician's home page. His proofs were based on demonstrating the equiconsistency of a "weird" variant of TST, "tangled type theory with λ-types" (TTTλ), with NF, and then showing that TTTλ is consistent relative to ZF with atoms but without choice (ZFA) by constructing a class model of ZFA which includes "tangled webs of cardinals" in ZF with atoms and choice (ZFA+C). These proofs were "difficult to read, insanely involved, and involve the sort of elaborate bookkeeping which makes it easy to introduce errors". In 2024, Sky Wilshaw formalized a version of Holmes' proof using the proof assistant Lean, finally resolving the question of NF's consistency.{{cite web |last1=Smith |first1=Peter |title=NF really is consistent |url=https://www.logicmatters.net/2024/04/21/nf-really-is-consistent/ |website=Logic Matters |date=21 April 2024 |access-date=21 April 2024}} Timothy Chow characterized Wilshaw's work as showing that the reluctance of peer reviewers to engage with a difficult to understand proof can be addressed with the help of proof assistants.{{cite web |last1=Chow |first1=Timothy |title=Timothy Chow on the NF consistency proof and Lean |url=https://www.logicmatters.net/2024/05/03/timothy-chow-on-the-nf-consistency-proof-and-lean/ |website=Logic Matters |date=3 May 2024 |access-date=3 May 2024}}
See also
Notes
{{Reflist}}
{{reflist|group=note}}
References
- {{cite journal | last1 = Crabbé | first1 = Marcel | year = 1982 | title = On the consistency of an impredicative fragment of Quine's NF | journal = The Journal of Symbolic Logic | volume = 47 | issue = 1| pages = 131–136 | doi=10.2307/2273386| jstor = 2273386 | s2cid = 42174966 }}
- {{cite web |last1=Fenton |first1=Scott |title=New Foundations Explorer Home Page |url=https://us.metamath.org/nfeuni/mmnf.html |website=Metamath |access-date=25 April 2024|date=2015}}
- {{cite web |url=http://www.dpmms.cam.ac.uk/~tf/cartesian-closed.pdf |title=Why the Sets of NF do not form a Cartesian-closed Category |first=Thomas |last=Forster |date=October 14, 2007 |website=www.dpmms.cam.ac.uk}}
- {{cite journal | last=Forster |first=T. E. |date=2008 | title = The iterative conception of set | journal = The Review of Symbolic Logic | volume = 1 | pages = 97–110 |doi=10.1017/S1755020308080064 |s2cid=15231169 |url=https://www.dpmms.cam.ac.uk/~tf/iterativeconception.pdf}}
- {{citation |mr=1166801 |last=Forster |first=T. E. |date=1992 |title=Set theory with a universal set. Exploring an untyped universe |series=Oxford Science Publications, Oxford Logic Guides |volume=20 |publisher=The Clarendon Press, Oxford University Press |place=New York |isbn=0-19-853395-0}}
- {{cite book |last=Forster | first=T. E. |date=2018 |article-url=http://plato.stanford.edu/entries/quine-nf/ |article=Quine's New Foundations |title=Stanford Encyclopedia of Philosophy}}
- {{cite journal | last = Grishin | first = V. N. | year = 1969 | title = Consistency of a fragment of Quine's NF system | journal = Dokl. Akad. Nauk SSSR | volume = 189 | number = 2 | pages = 41–243 | url = https://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=dan&paperid=35008&option_lang=eng }}
- {{cite journal | last1 = Hailperin | first1 = T | year = 1944| title = A set of axioms for logic | journal = Journal of Symbolic Logic | volume = 9 | issue = 1| pages = 1–19 | doi=10.2307/2267307| jstor = 2267307 | s2cid = 39672836 }}
- {{citation|mr=1759289
|last=Holmes|first= M. Randall
|title=Elementary set theory with a universal set
|series=Cahiers du Centre de Logique |volume= 10|publisher= Université Catholique de Louvain, Département de Philosophie|place= Louvain-la-Neuve|year= 1998|isbn= 2-87209-488-1|url=https://randall-holmes.github.io/head.pdf }}
- {{cite journal | doi = 10.1007/s11225-008-9107-8 | volume=88 | issue=2 | title=Symmetry as a Criterion for Comprehension Motivating Quine's 'New Foundations' | year=2008 | journal=Studia Logica | pages=195–213 | last1 = Holmes | first1 = M. Randall| s2cid=207242273 }}
- {{cite web
|last1=Holmes|first1=M. Randall
|last2=Wilshaw|first2=Sky
|title=New Foundations is consistent
|year=2024
|url=https://randall-holmes.github.io/Nfproof/maybedetangled2.pdf}}
- {{citation|author-link=Ronald Jensen|last=Jensen|first= R. B.|year= 1969|title=On the Consistency of a Slight(?) Modification of Quine's NF|journal=Synthese |volume=19|issue=1/2|pages= 250–63|jstor=20114640|doi=10.1007/bf00568059|s2cid=46960777}} With discussion by Quine.
- {{citation|title=New Foundations for Mathematical Logic
|first=W. V.|last= Quine
|journal=The American Mathematical Monthly|volume= 44|issue= 2 |year=1937|pages= 70–80
|publisher= Mathematical Association of America
|doi=10.2307/2300564
|jstor=2300564}}
- {{citation|mr=0002508
|last=Quine|first= Willard Van Orman
|title=Mathematical Logic|publisher= W. W. Norton & Co., Inc.|place=New York|year= 1940|edition=first}}
- {{citation|mr=0045661
|last=Quine|first= Willard Van Orman
|title=Mathematical logic
|edition=Revised |publisher= Harvard University Press|place= Cambridge, Mass.|year= 1951|isbn=0-674-55451-5 }}
- Quine, W. V., 1980, "New Foundations for Mathematical Logic" in From a Logical Point of View, 2nd ed., revised. Harvard Univ. Press: 80–101. The definitive version of where it all began, namely Quine's 1937 paper in the American Mathematical Monthly.
- {{cite book |last=Quine | first=Willard Van Orman |year=1987 |url=https://www.hup.harvard.edu/catalog.php?isbn=9780674798373 |chapter=The Inception of “New Foundations” |title=Selected Logic Papers - Enlarged Edition |isbn=9780674798373 |publisher=Harvard University Press}}
- {{citation|mr=0006327
|last=Rosser|first= Barkley
|title=The Burali-Forti paradox
|journal=Journal of Symbolic Logic|volume= 7|issue=1|year=1942|pages= 1–17|doi=10.2307/2267550|jstor=2267550|s2cid=13389728 }}
- {{cite journal |last=Specker |first=Ernst P. |author-link=Ernst Specker |date=1953 |title=The axiom of choice in Quine's new foundations for mathematical logic |journal=Proceedings of the National Academy of Sciences |volume=39 |number=9 |pages=972–975 |publisher=National Acad Sciences|doi=10.1073/pnas.39.9.972 |pmid=16589362 |pmc=1063889 |bibcode=1953PNAS...39..972S |doi-access=free }}
- {{citation|mr=0034733
|last=Wang|first= Hao
|title=A formal system of logic
|journal=Journal of Symbolic Logic|volume= 15|issue=1|year=1950|pages= 25–32|doi=10.2307/2268438|jstor=2268438|s2cid=42852449 }}
External links
- [http://math.stanford.edu/~feferman/papers/ess.pdf "Enriched Stratified systems for the Foundations of Category Theory"] by Solomon Feferman (2011)
- Stanford Encyclopedia of Philosophy:
- [http://plato.stanford.edu/entries/quine-nf Quine's New Foundations] — by Thomas Forster.
- [http://setis.library.usyd.edu.au/stanford/entries/settheory-alternative/ Alternative axiomatic set theories] — by Randall Holmes.
- Randall Holmes: [https://randall-holmes.github.io/nf.html New Foundations Home Page.]
- Randall Holmes: [https://randall-holmes.github.io/Bibliography/setbiblio.html Bibliography of Set Theory with a Universal Set.]
- Randall Holmes: [https://randall-holmes.github.io/Nfproof/newattempt.pdf A new pass at the NF consistency proof]
{{Set theory}}
{{Mathematical logic}}