| Description: Define the universal
class. Definition 5.20 of [TakeutiZaring] p. 21.
Also Definition 2.9 of [Quine] p. 19. The
class V can be described
as the "class of all sets"; vprc 5076
proves that V is not itself a set
in ZFC. We will frequently use the expression 𝐴 ∈ V as a short way
to say "𝐴 is a set", and isset 3427 proves that this expression has the
same meaning as ∃𝑥𝑥 = 𝐴. The class V is called the "von
Neumann universe", however, the letter "V" is not a tribute
to the name of
von Neumann. The letter "V" was used earlier by Peano in 1889
for the
universe of sets, where the letter V is derived from the word
"Verum".
Peano's notation V was adopted by Whitehead and Russell in Principia
Mathematica for the class of all sets in 1910. For a general discussion
of the theory of classes, see mmset.html#class. (Contributed by NM,
26-May-1993.) |
