Peter LeFanu Lumsdaine: Quine’s set theory NF and relatives
Time: Wed 2022-09-14 10.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Peter LeFanu Lumsdaine (Stockholm University)
This talk will be an introduction to Quine’s remarkable system NF, a set theory with a universal set. It has a very simple axiomatisation – extensionality, plus stratified comprehension – with powerful and subtle consequences. The world of NF is in many ways natural and idiomatic as a foundational setting, but very foreign from a ZF-acclimatised point of view.
A long-standing question is (or was) the consistency of NF. For the slightly variant NFU (NF with atoms) it is easy to exhibit models; but consistency of NF itself has long been elusive, until a recent proof by Randall Holmes – originally very technical and not widely accepted, but recently significantly simplified.
In this talk, I will briefly introduce NF, along with several variants and related systems, including NFU, TST, and Holmes’ TTT, and discuss their comparisons and model constructions. The seminar is partly intended as background for a possible future seminar on Holmes’ proof of consistency of NF.