New Foundations home page

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 Russell's theory of types 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 Postscript file) by permission of the publisher: a real second edition will appear online eventually in place of this ad hoc corrected version.

Here (Postscript) and here (LaTeX source)) is the latest version of my paper on symmetry as a criterion for sethood which motivates NF. Here is the next to the last version: here (Postscript)) which contains useful notes on recent changes.

Find here (LaTeX source) or here (Postscript file) some now rather ancient slides for a talk in which I discuss results of Solovay relating the strength of the Axiom of Cantorian Sets to n-Mahlo cardinals. The results are Solovay's, but he is not responsible for any errors in the proofs given, which are mine.

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 SML source (version of Feb 5, 2004) for a sequent prover using NFU as its logic, adapted from the sequent calculus for SF in Marcel's cut-elimination paper. Here find the proof of Cantor's theorem (a theoretically human-readable text document of considerable size) recorded by the prover (this was generated as the result of dialogue between myself and the prover; it is not an automatically generated proof). The script of user commands which generates this proof is the body of the function proofsofar() at the end of the marcelsequent.sml source file.

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é 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 has nothing about NF on his page, alas, though he does put in a plug for "Non-Standard Set Theories" (and he has kindly added a link to this page).

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.

Randall Holmes is the author of this page; all flames concerning its contents should be addressed to him. He is also the manager of the NF mailing list (see above). 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. Here are my notes on forcing in NFU and NF. Here are the slides for the talk I gave at BEST on this subject.

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.

Warren Wood collaborated with Thomas Jech (link above) on the work with Otter. This link is not to a personal page but to his work applying the Otter theorem prover to Holmes's system TRC.

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!

Isaac Malitz, who did his thesis on positive set theory, has an e-mail link here.

This is not an exhaustive list of current workers; it consists of those for whom I have links. Workers are encouraged to send me their e-mail addresses or home pages so I can link them in! As of March 2005, 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 March 30, 2005 (by Holmes).

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

Please send all comments and corrections to [email protected] (Randall Holmes).