 The two “restrictions” that Gödel intends are the restriction that types are not cumulative and that the levels of types are limited to the natural numbers 0, 1,… n,…. Gödel suggests that one adopt a cumulative system of types in which a given type includes functions of all lower types (or orders), and the types extend beyond \(\omega\), \(\omega\) + 1, …\(\omega^{\omega}\), …, through all the ordinals. Such a “natural generalization” of the theory of types, he asserts, amounts to the same as Zermelo-Fraenkel set theory (ZF). Gödel’s claim is spelled out by George Boolos (1971) as the “iterative conception” of sets, which can be expressed formally. If one thinks of sets as built up in stages, with each stage adding all sets of members of the last stage, and the process extending endlessly, then the axioms of ZF set theory are indeed provable from the axioms of the theory of the “iterative conception” of sets. In turn the “iterative conception” relies on a strong intuition, contrary to what Quine says. It is the same intuition that underlies the hierarchy of types.