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 in second-order logic, best expressible only after insertion into set theory (though this solution remains incomplete, as will be explained in Part 3).
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,
the grand tour of the foundations of mathematics).
Now let T0 be the external copy of T, 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 truly finite
components of T. Formally, T0 is made of the k such that
«k» ∈ T, where the notation as a quote
«k» abbreviates a ground term of set theory describing k
as an object. 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
a 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)».
for set theory, 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 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
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»
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.
= «is a function»
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 (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, which will be given below.
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 A ∧ B 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 dA ∧ A and dA ⇒ A (extending A where it was not definite, by 0 and 1 respectively). This way, both formulas A ∧ (B ∧ C)
(A ∧ B) ∧ C have the same definiteness condition (dA ∧ (A ⇒ (dB ∧ (B ⇒ dC)))).
For any class A and any unary predicate B definite in all A, the class defined by the (everywhere definite) predicate A∧B, is called the subclass of A defined by B.
FR : 1.7. Classes
en théorie des ensembles