| Description: Define the successor of a
class. When applied to an ordinal number, the
successor means the same thing as "plus 1" (see oa1suc 4154). Definition
7.22 of [TakeutiZaring] p. 41, who
use "+ 1" to denote this function.
Our definition is a generalization to classes. Although it is not
conventional to use it with proper classes, it has no affect on a proper
class (sucprc 3039), so that the successor of any ordinal class
is still
an ordinal class (ordsuc 3060), simplifying certain proofs. Some authors
denote the successor operation with a prime (apostrophe-like) symbol,
such as Definition 6 of [Suppes] p. 134
and the definition of successor
in [Mendelson] p. 246 (who uses the
symbol "Suc" as a predicate to mean
"is a successor ordinal"). The definition of successor of [Enderton]
p. 68 denotes the operation with a plus-sign
superscript. |
Home
