New Foundations home page

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

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.



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 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

There was until fairly recently a New Foundations mailing list, which I shall try to revive in some form (writing in June 2020)

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é (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


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