  This view of set theory gave rise to the Theory of Types. In the Theory of Types (as simplified successively by Ramsey, Carnap, Gödel and Quine) the bottom type is a collection of atoms. Atoms are non-sets (dormice, teapots, anything you please) with no internal structure visible to the set theory. Thereafter type \(n + 1\) is simply the power set of type \(n\), and there is a type for each natural number. The process cannot be extended to give transfinite types, since the types (being formally disjoint) are not cumulative so there is no sensible way to define a \(\omega\)th type. NF arises from a consideration of the syntax used to describe structures of this kind, and the syntax requires more careful handling. A first-order language for describing structures of this sort has infinitely many suites of variables, one suite for each type, and a membership symbol (‘\(\in\)’ as usual) which can be placed only between variables of consecutive types: ‘\(x_n \in y_{n+1}\)’ is wellformed but ‘\(x_n \in y_n\)’ is not. The equality sign can be placed only between variables of the same type.