1.7. Classes in set theory
In any system, a class is a unary
predicate A seen as the set of objects where A is true, that is «the
class of all x such that A(x)».
In a set theoretical universe,
each set E is synonymous with the class of the x such that x∈E
(defined by the formula x∈E with argument x and parameter E).
However, this involves two different interpretations of the notion of set,
that need to be distinguished as follows.
Standard universes and meta-sets
Interpreting (inserting)
set theory into itself, involves articulating two interpretations (models) of set theory, which
will be distinguished by giving the meta- prefix to the one used as framework. Aside generic
interpretations, set theory has a standard kind of interpretations into itself, where each
set is interpreted by the class (meta-set) of its elements (the synonymous set and
meta-set, i.e. with the same elements, are now equal), and each function is interpreted
by its synonymous meta-function.
This way, any set will be a class, while any class is a meta-set of objects. But some
meta-sets of objects are not classes (no formula with parameters can define them ;
giving examples would be paradoxical as it would mean defining something
undefinable, yet 1.B
introduces such possibilities);
and some classes are not sets, such as the class of all sets (see Russell's
paradox in 1.8), and the universe (class of all objects, defined by 1).
Definiteness classes
Set theory accepts all objects as «elements» that can belong to sets and be
operated by functions (to avoid endless further divisions between sets of
elements, sets of sets, sets of functions, mixed sets...). This might be formalized
keeping 3 types (elements, sets and functions), where each set would have a
copy as element, identified by a functor from sets to elements, and the same for
functions. But beyond these types, our set theory will anyway need more
notions as domains of its structures, which can only be conveniently formalized
as classes. So, let us keep "element" as the only type containing all objects, and
formalize the notions of set and function as classes named by predicate symbols:
Set = «is a set»
Fnc = «is a function»
In first-order logic, any expression is ensured to take a definite value, for
every data of a model and values of all free variables there (by virtue of its
syntactic correction, that is implicit in the concept of «expression»).
But in set theory, this may still depend on the values of free variables.
So, an expression A (and any structure defined from it) will be called
definite, if it actually takes a value for the given values of its free variables
(seen as arguments and parameters of any structure it defines). This condition
is itself an everywhere definite
predicate, expressed by a formula dA with the same free variables.
Choosing one of these as argument, the class it defines is the meta-domain,
called class of definiteness, of the unary structure defined by A.
Expressions should be only used where they are definite, which will be done
rather naturally. The definiteness condition of (x ∈ E) is Set(E).
That of the function evaluator f(x) is Fnc(f) ∧
x ∈ Dom f.
But the definiteness of the last formula needs a justification, given below.
Extended definiteness
A theory with partially definite structures, like set theory, can be formalized (translated) as
a theory with one type and everywhere definite structures, keeping intact all expressions
and their values wherever they are definite : models are translated one way by giving
arbitrary values to indefinite structures (e.g. a constant value), and in the way back by
ignoring those values. Thus, an expression with an indefinite subexpression may be
declared definite if its final value does not depend on these extra values.
In particular for any formulas A and B, we shall regard the formulas
A ∧ B and A ⇒ B as definite if A
is false, with respective values 0 and 1, even if B is not definite. So,
let us give them the same definiteness condition
dA ∧ (A ⇒ dB)
(breaking, for A ∧ B, the symmetry between A
and B, that needs not be restored). This formula is made definite by the
same rule provided that dA and dB were definite. This way, both formulas
A ∧ (B ∧ C)
(A ∧ B) ∧ C
have the same definiteness condition (dA ∧
(A ⇒ (dB ∧ (B ⇒ dC)))).
Classes will be defined by everywhere definite predicates, easily expressible by
the above rule as follows.
Any predicate A can be extended beyond its
domain of definiteness, in the form dA ∧ A (giving 0), or
dA ⇒ A (giving 1).
For any class A and any unary predicate B definite in all A, the class defined
by A∧B is called the subclass of A
defined by B.
Other languages:
FR : 1.7. Classes
en théorie des ensembles