Axiom of Regularity - Regularity, The Cumulative Hierarchy, and Types

Regularity, The Cumulative Hierarchy, and Types

In ZF it can be proven that the class (see cumulative hierarchy) 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 axiom of regularity, a model which satisfies it can be constructed by taking only sets in .

Herbert Enderton (1977, 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. The details of this implicit typing are spelled out in, and again in a well-known article of George Boolos ." Urquhart (2003, p. 305)

Dana Scott (1974) went further an claimed that: "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—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. (Lévy 2002, p. 73)