New Foundations

New Foundations (NF) is a version of axiomatic set theory in which there is a set of all sets, but the comprehension axiom is restricted by a “stratification” condition.

The category of sets and functions in NF is known to not be cartesian closed, so it is not a topos, but can be equipped with finite limits and a subobject classifier. One can even construct a set of all functions between two sets, but there is no evaluation map A×B ABA\times B^A \to B making this an exponential in the category.

There are at least three proofs of this fact: one, due to Randall Holmes, doesn’t seem to have been made public; the others are due to McLarty and Forster, and derive contradictions (different in the two proofs) from assumptions on the behaviour of a pairing function used to construct binary products.

For a long time the (relative) consistency of NF was an open problem, although NF with urelements (NFU) was known to be consistent (relative to ZF plus some large cardinals). Recently there may be a proof of its consistency.


  • Wikipedia, New Foundations

  • Colin McLarty, Failure of cartesian closedness in NF, Journal of Symbolic Logic, 57 no 2 (1992) pp 555-556 (pdf)

  • Thomas Forster, Why the Sets of NF do not form a Cartesian-closed Category, (1997) (pdf)

Last revised on September 3, 2015 at 07:10:15. See the history of this page for a list of all contributions to it.