New Foundations home page

Note, added June 8, 2020: After a further fifteen years of neglect, a great deal of dusting and rearranging needs to be done in this space before it is usable! June 10: I am done with preliminary administrative repair (links to resources and persons are as accurate as I can make them) but there remains the more delicate task of reporting on changes in our view of the mathematical content.

For new information about the mailing list, look in the Mailing List and Links to NF Fans section.

Contents

• Introduction
• Mailing List and Links to NF Fans
• Definition
• The Paradoxes
• The Big Problem
• Consistent Subsystems
• Thomas Forster's Exhaustive Bibliography (new version set up in HTML by Paul West)

The subject of the home page which is developing here is the set theory "New Foundations", first introduced by W. V. O. Quine in 1937. This is a refinement of the simple typed theory of sets (which is not really Russell's type theory, though for the rest of this document I will follow my own old incorrect usage and call it that) based on the observation that the types in Russell's theory look the same, as far as one can apparently prove.

To see Thomas Forster's master bibliography for the entire subject, as updated and HTML'ed by Paul West, click here. References in this page also refer to the master bibliography. We are very grateful to Thomas Forster for allowing us to use his bibliography. An all purpose reference for this field (best for NF) is Thomas Forster's "Set theory with a universal set", second edition, Oxford logic guides no. 31, 1995. An old but still good treatment is found in Rosser's "Logic for mathematicians" (second edition, Chelsea, 1978); the main text predates Specker's results about Choice and Infinity. The entire development in Rosser, including the treatment of Choice, can readily be adapted to NFU (by providing a type-level ordered pair as a primitive). I have written something which appears to be an elementary set theory textbook using NFU: for information look here

A corrected text for my book Elementary Set Theory with a Universal Set is now available online here (this is a PDF file) by permission of the publisher: a real second edition will appear online eventually in place of this ad hoc corrected version.

There is a theorem prover Watson whose higher order logic is an untyped lambda-calculus equivalent to an extension of Jensen's NFU. This is being developed by Randall Holmes. Source and documentation can be downloaded from the link given. In this connection, one should also mention the work of Thomas Jech and Warren Wood in which they apply the prover Otter to investigations of the system of untyped combinatory logic TRC defined by Holmes (and shown to be equivalent to NF). Here find the page describing a sequent prover using NFU as its logic, adapted from the sequent calculus for SF in Marcel's cut-elimination paper.

Back to contents

Mailing List and Links to NF fans

The Mailing List

Links to Fans

Thomas Forster is the author of the currently definitive tome on the subject (see above).

Marcel Crabbé (who is retired, and whose page now malfunctions) showed that subsystems of NF with predicativity restrictions are consistent and also showed that NFU (with no extensionality at all) enjoys cut-elimination.

Daniel Dzierzgowski 's home page is here .

Aldo Antonelli, mentioned here before, has passed on. May his memory be for a blessing.

Richard Kaye has worked on the theory KF which is a subtheory of both NF and standard set theory and has worked on fragments of NF in which comprehension is restricted to quantifier prefix classes.

Friederike Koerner is engaged in interesting work on consistency and independence results using permutation models of NF. I am not verifying mailing addresses as I fix this in 2020: I do not find a web page for Dr Koerner.

Randall Holmes is the author of this page; all flames concerning its contents should be addressed to him. He was and one hopes will be again the manager of the NF mailing list. His research is mostly on Jensen's NFU and extensions and on development and application of the Watson theorem prover, which uses a lambda-calculus equivalent to an extension of NFU as its higher order logic. This descrption of my program is outdated: look at my main page.

Flash Sheridan warns us that his page is mostly his Newton programming stuff.

Thomas Jech has worked on implementing the system of combinatory logic TRC defined by Randall Holmes in his Ph. D. thesis and a subsequent paper under the Otter theorem prover.

Paul West is an amateur reader of set theory who has done a good deal of work on improving this page. Look at his version of the exhaustive bibliography! Again, I am not verifying email addresses as I update in 2020.

Isaac Malitz, who did his thesis on positive set theory, has an e-mail link here. Again, not updated in 2020.

This is not an exhaustive list of current workers; it consists of those for whom I have links. In 2020, I think I should be soliciting information from a few new people. Workers are encouraged to send me their e-mail addresses or home pages so I can link them in! As of June 2020, I comment that I have checked these links and modified them in certain cases.

Back to contents

Definition

• extensionality: sets with the same elements are the same.
• "stratified" comprehension: the set { x | P } exists when P is a formula of first-order logic with equality and membership which can be obtained from a well-formed formula of Russell's type theory by ignoring the type indices (while ensuring that variables of different types do not become identified).
• Stratified comprehension is an axiom scheme, which can be replaced with finitely many of its instances (a result of Hailperin). Using the finite axiomatization removes the necessity of referring to types at all in the definition of this theory.

Back to contents

The Paradoxes

• Russell's paradox: "x is not an element of x" is not a stratified predicate. But the universe, V = { x | x = x }, does exist in NF and its subsystems known to be consistent (see below).
• The Burali-Forti paradox of the largest ordinal: Ordinals are defined in NF as equivalence classes of well-orderings. There is a set of all ordinals, and it has the usual natural order, and this order has an order type. So far, so good. But the order type of the set of ordinals less than an ordinal a does not need to be equal to a (this is proved in the usual set theory by transfinite induction on an unstratified condition!); the order type Omega of all the ordinals is an ordinal, but it is less than the largest ordinals. The order type Omega_2 of the ordinals less than Omega is less than Omega. There is an apparent descending sequence of ordinals Omega_i suggested here, but it is not a set because (you guessed it) its definition is not stratified (fortunately!).
• Cantor's paradox of the largest cardinal: Cardinal numbers are defined in NF as equivalence classes of sets of the same size. The form of Cantor's theorem which can be proven in Russell's type theory asserts that the cardinality of the set of one-element subsets of A is less than the cardinality of the power set of A. Note that the usual form (|A| < |P(A)|) doesn't even make sense in type theory. It makes sense in NF, but it isn't true in all cases: for example, it wouldn't do to have |V| < |P(V)|, and indeed this is not the case, though the set 1 of all one-element subsets of V is smaller than V (the obvious bijection x |-> {x} has an unstratified definition!).
• Sets with the property that the set P1(A) of one-element subsets of A is the same size as A are called "Cantorian" sets; sets with the stronger property that the restriction to A of the singleton "map" x |-> {x} exists are called "strongly Cantorian" sets. Cantorian and strongly Cantorian sets clearly satisfy Cantor's theorem in its usual unstratified form (|A| = |P1(A)| < |P(A)|). Strongly Cantorian (and to a lesser extent Cantorian) sets have properties more like those of the sets of the usual set theory than the general sets of NF (the same remarks apply in the subsystems); for example, the relative type of a variable restricted to a strongly Cantorian set can be freely raised and lowered, allowing limited subversion of stratification restrictions. The strongly Cantorian sets can be thought of as being "small enough" to act like the sets of ZFC. The set of natural numbers is provably Cantorian; the assumption that it is strongly Cantorian, known as Rosser's Axiom of Counting, is known to strengthen NF (if it is consistent -- one of the few independence results not obtained by permutation methods) and known to be consistent with NFU.
• Though NF is not known to be consistent, these solutions to the paradoxes are known to work: they work exactly the same way in NFU (New Foundations with urelements) which has well-understood models.

Back to contents

The Big Problem

• NF disproves the Axiom of Choice (Specker, 1953).
• NF proves Infinity (corollary of the previous point).
• NF is at least as strong as Russell's theory of types with the Axiom of Infinity (corollary of previous point and the definition of the theory).
• No evidence exists that NF is any stronger than the theory of types with the Axiom of Infinity.

• NFU: New Foundations with urelements. This system is consistent, consistent with Choice, and does not prove Infinity but is consistent with it ( Jensen, 1969). NFU + Infinity + Choice has the same consistency strength as the theory of types with the Axiom of Infinity. Its model theory is fairly simple and NFU can safely be extended as far as you think ZFC can be extended. The consistency of NFU, which has the full scheme of stratified comprehension, shows that the comprehension scheme and resulting presence of "big" sets is not the problem with NF. For an extended study of set theory in NFU, click here. Extensions of NFU are adequate vehicles for mathematics in a basically familiar style.
• Extensions of NFU: Robert Solovay has shown that the extension of NFU + Infinity + Choice with the axiom "all Cantorian sets are strongly Cantorian" (this axiom was proposed for NF by C. Ward Henson) has the exact strength of ZFC + "there is an n-Mahlo cardinal" for each concrete natural number n (unpublished). Solovay calls this system NFUA. Holmes has proposed stronger extensions whose status has now been settled by Solovay and Holmes. The system NFUB, which adds to NFUA an axiom scheme which asserts that each definable class of Cantorian ordinals is the intersection of some set with the class of Cantorian ordinals, has been shown by Solovay to have the exact strength of ZFC - Power Set + "there is a weakly compact cardinal". The system NFUM, which adds to NFUB the assertion that the iterated images of Omega (the order type of the natural order on the ordinals) is downward cofinal in the non-cantorian ordinals, is shown by Holmes to be equivalent to Kelley-Morse set theory plus the assertion that there is a measure on the proper class ordinal (the description of this theory requires care). My paper on these results has appeared in the JSL.

  Ali Enayat and Solovay have some new results relating the strength of NFU + "the universe is finite" and some of its extensions (analogues of NFUA, NFUB, and NFUM) to systems of arithmetic. Enayat has also shown that NFUA is equiconsistent with von Neumann-Godel-Bernays predicative class theory with the proper class ordinal weakly compact.

• NFI: described by Marcel Crabbé in 1983, restricts comprehension to those instances where no variable is mentioned in { x | P } of type more than one higher than that of x. This is a restriction on predicativity, but NFI is still mildly impredicative. The weaker system NFP (predicative NF) results if one additionally forbids variables one type higher than x from being bound in P. NFI has strong extensionality. Holmes has shown that strong extensions of NFI are consistent.
• NF3: described by Grishin in 1969, in which { x | P } exists if P can be typed using no more than three types.
• Other interesting fragments are mostly special subsets of those above. For example, NFO (NF with the formula P required to be open) is (although this is not obvious!) a subtheory of NF3.
• INF (intuitionistic NF) is being studied by Daniel Dzierzgowski at the Catholic University in Louvain-la-Neuve, but is not known to be consistent.
• Another interesting subtheory of NF (which is also a subtheory of the usual set theory) is KF, which is the theory which one obtains from Zermelo set theory by weakening comprehension to bounded (all quantifiers restricted to sets) stratified formulas. KF with Infinity is as strong as the theory of types with infinity and represents the intersection between bounded Zermelo set theory (MacLane set theory) and NF. Thomas Forster is the one to ask about this. Adding the assertion of the existence of the universal set to KF yields NF exactly.

Back to contents

Last revision June 10, 2020 (by Holmes).

Thanks to Paul West for refining Holmes's html code and putting bibliographies into HTML.

Please send all comments and corrections to holmes@math.boisestate.edu (Randall Holmes).