| Description: Define the cumulative
hierarchy of sets function, using Takeuti and
Zaring's notation (𝑅1).
Starting with the empty set, this
function builds up layers of sets where the next layer is the power set
of the previous layer (and the union of previous layers when the
argument is a limit ordinal). Using the Axiom of Regularity, we can
show that any set whatsoever belongs to one of the layers of this
hierarchy (see tz9.13 8654). Our definition expresses Definition 9.9 of
[TakeutiZaring] p. 76 in a closed
form, from which we derive the
recursive definition as theorems r10 8631, r1suc 8633, and r1lim 8635.
Theorem r1val1 8649 shows a recursive definition that works for
all values,
and theorems r1val2 8700 and r1val3 8701 show the value expressed in terms of
rank. Other notations for this function are R with the argument
as a
subscript (Equation 3.1 of [BellMachover] p. 477), V with a
subscript (Definition of [Enderton] p.
202), M with a subscript
(Definition 15.19 of [Monk1] p. 113), the
capital Greek letter psi
(Definition of [Mendelson] p. 281),
and bold-face R (Definition 2.1 of
[Kunen] p. 95). (Contributed by NM,
2-Sep-2003.) |
