nLab New Foundations

Idea

New Foundations (NF) is a version of axiomatic set theory in which there is a set of all sets, but the axiom of comprehension 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\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.

Related concepts

• foundations of mathematics

• univalent foundations for mathematics

References

• Wikipedia, New Foundations

• Stanford Encyclopedia of Philosophy, Quine’s 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)