Abstract

Quine’s “New Foundations” (NF) was first presented in Quine [1937] and later on in Quine [1963]. Ernst Specker [1958, 1962], building upon a previous result of Ehrenfeucht and Mostowski [1956], showed that NF is consistent if and only if there is a model of the Theory of Negative (and positive) Types (TNT) with full extensionality that admits of a “shifting automorphism,” but the existence of a such a model remains an open problem.