| 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 5193
proves that V is not itself a set
in ZF. We will frequently use the expression 𝐴 ∈ V as a short way
to
say "𝐴 is a set", and isset 3411 proves that this expression has the
same meaning as ∃𝑥𝑥 = 𝐴.
In well-founded set theories without urelements, like ZF, the class V
is equal to the von Neumann universe. However, the letter "V"
does not
stand for "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 Latin
word "Verum", referring to the true truth constant 𝑇.
Peano's
notation V was adopted by Whitehead and Russell in
Principia
Mathematica for the class of all sets in 1910.
The class constant V is the first class constant
introduced in this
database. As a constant, as opposed to a variable, it cannot be
substituted with anything, and in particular it is not part of any
disjoint variable condition.
For a general discussion of the theory of classes, see
mmset.html#class 3411. See dfv2 3401 for an alternate definition.
(Contributed by NM, 26-May-1993.) |
