Peter Aczel: On the Consistency Problem for Quine's New Foundations, NF

In 1937 Quine introduced an interesting, rather unusual, set theory called New Foundations - NF for short.  Since then the consistency of NF has been an open problem. And the problem remains open today.  But there has been considerable progress in our understanding of the problem. In particular NF was shown, by Specker in 1962, to be equiconsistent with a certain theory, \(TST^+\) of simple types. Moreover Randall Holmes, who has been a long-term investigator of the problem, claims to have  solved the problem by showing that \(TST^+\) is indeed consistent.  But the working manuscripts available on his web page that describe his possible proofs are not easy to understand - at least not by me.

In my talk I will introduce \(TST^+\) and its possible models and discuss some of the interesting ideas, that I have understood, that Holmes uses in one of his possible proofs.