TL;DR
This paper proves the consistency of Quine's set theory 'New Foundations' by constructing a model using tangled type theory, with refined details verified in Lean.
Contribution
It provides a formal proof of NF's consistency through a novel model construction and leverages formal verification tools for rigor.
Findings
NF is consistent based on the constructed model
The model uses tangled type theory
Formal verification in Lean confirms the proof
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Logic, programming, and type systems · Advanced Topology and Set Theory