New Foundations home page

Note, added March 30, 2005 After systematic neglect for some years, I'm about to overhaul the page (done) and update the bibliography. Any comments from NFistes would be useful at this point...

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



This page is (permanently) under construction by Randall Holmes.

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

The address of the NF mailing list is now Randall Holmes manages the list and should be contacted at for inquiries. You can also send a message to the list server containing "subscribe nf" as text (not as subject line) to subscribe semiautomatically (Holmes approves subscriptions). A mail link to send a message to the new list is here.

Links to Fans

W. van Orman Quine originated NF.

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


The axioms of New Foundations (hereinafter NF) are

Back to contents

The Paradoxes

These don't seem to trouble NF, though the fact that it disproves AC (see below) is disturbing!

Back to contents

The Big Problem

NF is not known to be consistent. The following results are known: Back to contents

Consistent subsystems

Certain subsystems of New Foundations are known to be consistent. These include:

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 (Randall Holmes).