NF is Consistent
Logic
2025-06-23 v23
Abstract
In this paper we will present a proof of the consistency of Quine's set theory "New Foundations" (hereinafter NF), so-called after the title of the 1937 paper in which it was introduced. This version takes the approach of building a model of tangled type theory rather than a model of the usual set theory without choice with a tangled web of cardinals; further, details of the construction are refined due to interaction with the now complete verification in Lean by the second author.
Keywords
Cite
@article{arxiv.1503.01406,
title = {NF is Consistent},
author = {M. Randall Holmes and Sky Wilshaw},
journal= {arXiv preprint arXiv:1503.01406},
year = {2025}
}
Comments
The latest version of these documents is always visible on my home page http://randall-holmes.github.io and it will be updated there more often then here