 Quine’s set theory New Foundations (abbreviated NF, proposed in 1937 in his paper “New Foundations for Mathematical Logic”), is also based on a procedure for identifying the objects in successive types in order to obtain an untyped theory. However, in the case of NF and related theories, the idea is to identify the entirety of type \(n + 1\) with type \(n\); the type hierarchy is to be collapsed completely. An obvious difficulty with this is that Cantor’s theorem suggests that type \(n + 1\) (being the “power set” of type \(n)\) should be intrinsically larger than type \(n\) (and in some senses this is demonstrably true).