Editing Axiom of regularity (section)

== Regularity, the cumulative hierarchy, and types ==
In ZF it can be proven that the class <math display="inline"> \bigcup_{\alpha} V_\alpha </math>, called the [[von Neumann universe]], is equal to the class of all sets. This statement is even equivalent to the axiom of regularity (if we work in ZF with this axiom omitted). From any model which does not satisfy the axiom of regularity, a model which satisfies it can be constructed by taking only sets in <math display="inline"> \bigcup_{\alpha} V_\alpha </math>.

Herbert Enderton{{sfn|Enderton|1977|loc=p. 206}} wrote that "The idea of rank is a descendant of Russell's concept of ''type''". Comparing ZF with [[type theory]], [[Alasdair Urquhart]] wrote that "Zermelo's system has the notational advantage of not containing any explicitly typed variables, although in fact it can be seen as having an implicit type structure built into it, at least if the axiom of regularity is included.<ref>The details of this implicit typing are spelled out in {{harvnb|Zermelo|1930}}, and again in {{harvnb|Boolos|1971}}.</ref>{{sfn|Urquhart|2003|p=305}}

Dana Scott{{sfn|Scott|1974}} went further and claimed that:

{{Blockquote|The truth is that there is only one satisfactory way of avoiding the paradoxes: namely, the use of some form of the ''theory of types''. That was at the basis of both Russell's and Zermelo's intuitions. Indeed the best way to regard Zermelo's theory is as a simplification and extension of Russell's. (We mean Russell's ''simple'' theory of types, of course.) The simplification was to make the types ''cumulative''. Thus mixing of types is easier and annoying repetitions are avoided. Once the later types are allowed to accumulate the earlier ones, we can then easily imagine ''extending'' the types into the transfinite&mdash;just how far we want to go must necessarily be left open. Now Russell made his types ''explicit'' in his notation and Zermelo left them ''implicit''. [emphasis in original]}}

In the same paper, Scott shows that an axiomatic system based on the inherent properties of the cumulative hierarchy turns out to be equivalent to ZF, including regularity.{{sfn|Lévy|2002|p=73}}