1.7. Classes in set theory

The unified framework of theories

Attempts to formalize one-model theory in first-order logic, would fail to exclude infinitely large «expressions» and «proofs»: this needs an axiom of second-order logic, best expressible only after insertion (interpretation) in set theory. As the components of its model [T, M] are named there by free variables, their variability makes this the set-theoretical expression of model theory (which, together with the axiomatization of set theory, will complete the grand tour of the foundations of mathematics).

Now let T0 be the external theory looking like a copy of T (even if it might only be a copy of part of it), i.e. the theory (integrated in the formalism of set theory but not part of its universe of objects) whose components k (types, symbols, axioms) have copies as objects which are the standard (= truly finite) components of T. Formally, T0 is made of the k such that the formula («k» ∈ T) is true, where the notation as a quote «k» abbreviates a ground term of set theory describing k as an object, and the truth of this formula means that the value of this term «k» in the universe, belongs to T. By this correspondence, any (model-theoretical) model M of T is indirectly also a (set-theoretical) model of T0.

This gives a powerful framework for the interpretation of T0 in M, encompassing both previous (set-theoretical and model-theoretical) frameworks of interpretations of theories in models. Namely, all works (expressions, proofs and other developments) done in T0, have copies as objects in the system T (system of objects described by set theory as having the formal property of «being a theory»); meanwhile, the (set theoretical) model M of T0 is formally seen as a «model of T», in the model-theoretical sense formalized inside the same set-theoretical framework, as it belongs to the same universe as T.
However, the power of this interpretation comes with a cost in legitimacy: for an externally given theory T0 with infinitely many components, we cannot directly define a corresponding T, as a set cannot be formally defined as exactly made of the values of an infinite list of terms (which are only meta-objects). We can work starting from a T0 only if its infinities of components are produced by some rules, for getting T as defined by the same rules. Then, no matter if T0 is finite or not, the existence of a model M of T, reflecting the consistency of T as defined inside the universe, does not automatically result from the consistency of T0 (as seen outside the universe). These consequences of the completeness and incompleteness theorems will be explained later.

Classes, sets and meta-sets

For any theory, a class is just a unary predicate A reinterpreted as the set of objects where A is true, that is «the class of the x such that A(x)».
In particular for set theory, each set E is synonymous with the class of the x such that xE (defined by the formula xE with argument x and parameter E). However, this involves two different interpretations of the concept of set, that need to be distinguished as follows.

From now on, in the above unified framework, the theory to be used as T0, interpreted in the model M and studied as an object T, will be set theory itself (expressible as a generic theory as explained in 1.9 and 1.10). Thus, our above use of set theoretical concepts as the framework describing the surrounding universe, is now a copy of T0 but with a different interpretation, that will be distinguished by carrying the meta- prefix. Set theoretical concepts in M can be nicely reflected by their meta interpretation, but both should not be confused.

Instead of the generic representation of all objects of generic theories as pure meta-elements, the role of each object «set» of set theory will usually be played by the class (meta-set) of its elements; similarly, the role of functions will be played by the corresponding functors.
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 (they cannot be defined by any formula with parameters); and some classes are not sets, such as the universe (class of all objects, defined by 1), and the class of all sets, according to Russell's paradox (1.8).

Definiteness classes

In set theory, all objects need to be accepted as «elements» that can belong to sets and be operated by functions (to avoid illimited divisions between sets of elements, sets of sets, sets of functions, mixed sets...). This might be formalized by keeping 3 types where each set would have a copy among elements (identified by a functor from sets to elements), and the same for functions. But it would not suffice to our set theory, that will need more notions beyond those of set and function. For this, our set theory will use classes instead of types as its notions. In particular, the notions of set and function will be classes named by predicate symbols:

Set = «is a set»
Fnc = «is a function»

In generic theories, the syntactic correction of an expression (that is implicit in the concept of «expression») ensures that it will take a definite value, for every data of a model with an interpretation of its free variables there. But in set theory, this may still depend on the values of its 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 (arguments and parameters) in the model. This definiteness condition is itself an everywhere definite predicate, expressed by a formula we shall abbreviate here as dA, with the same free variables.
Classes are defined by definite unary predicates. The meta-domain of any unary structure A, is the class defined by dA, with the same argument and parameters, called its class of definiteness.
Expressions should be only used where they are definite, which will be done rather naturally. The definiteness condition of (xE) 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, which will be given below.

Extended definiteness

A theory with partially definite structures 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.

For all predicates A and B, let us give to AB and A ⇒ B the same definiteness condition (dA ∧ (A ⇒ dB)) (breaking, for A ∧ B, the symmetry between A and B, that needs not be restored). They will thus be seen definite (with respective values 0 and 1) if A is false and B is not definite.

This makes definite the definiteness conditions themselves, as well as dAA and dAA (extending A where it was not definite, by 0 and 1 respectively). This way, both formulas
A ∧ (BC)
(AB) ∧ C
have the same definiteness condition (dA ∧ (A ⇒ (dB ∧ (BdC)))).

For any class A and any unary predicate B definite in all A, the class defined by the (everywhere definite) predicate AB, is called the subclass of A defined by B.

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions, objects, meta-objects
1.4. Formalizing types and structures
1.5. Expressions and definable structures
1.6. Connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Quantifiers
1.10. Formalization of set theory
1.11. Set generation principle
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
Philosophical aspects Time in model theory
Time between theories
2. Set theory (continued) 3. Algebra 4. Model theory
Other languages:
FR : 1.7. Classes en théorie des ensembles