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 models and discuss some of the interesting ideas that Holmes uses in one of his possible proofs, that I have understood.