1.7. Classes in set theory
The unified framework of theories
Attempts to formalize one-model theory in first-order logic cannot completely specify
the meta-notions of «expressions» and «proofs», because as will be explained in 4.7
(Non-standard
models of Arithmetic), descriptions of finite systems by first-order axioms
cannot detect and exclude all non-standard ones, calling «non-standard system»
an infinite system mistakenly (but consistently) described by a theory as
«finite but indescribably large» (non-standard «proofs» are not actually
valid). To fill this gap requires a second-order
axiom, whose meaning is best expressed after insertion in set theory.
As this insertion turns its components into free variables whose values define its
model [T, M], their variability removes its main difference with model theory
(the other difference is that model theory can also describe theories without models).
This view of model theory as developed from set theory, which Parts 3 and 4
will almost achieve, will complete the grand tour of the foundations of mathematics
after the formalization
of set theory in the model theoretical framework.
Given a theory T so described, let T_{0} be the external
theory, also inserted in set theory, which looks like a copy of T as any
component k
of T_{0} has a copy as an object serving as a component of T.
Formally, T_{0} can be defined from T as
made of the k such that («k» ∈ T) is true, where the notation
«k» abbreviates a term of set theory designating k
as an object, and the truth of this formula means that the value of this term
in the universe belongs to T.
This picture forms a convenient unified framework for interpreting theories in models,
encompassing both previous ones (set-theoretical and model-theoretical):
all works on the theory T_{0} (expressions, proofs and other developments),
have copies as objects formally described by the model theoretical development of set
theory as the same «works on the theory T». Meanwhile in the same universe,
any system M described as a «model of T» is indirectly
also a set-theoretical model of T_{0}.
However, the power of this framework comes with a cost in legitimacy:
- Starting from an arbitrary infinite T_{0}, a corresponding
T cannot be directly defined, as a definition must be finitely expressible.
We need some finite rules specifying the infinities of components of
T_{0}, for getting T as defined by the same rules.
- The risk for the universe to be non-standard in the sense of containing
non-standard systems (which first-order formalizations of set theory cannot
prevent), leads to the following possible discrepances between
T_{0} and T :
- T_{0} only copies the standard components of
T, ignoring non-standard ones which also
exist for infinite theories in a non-standard universe. Then a model of
T_{0} in this universe may fail to be a model of T
as it does not fit the non-standard components of T.
- The consistency of T_{0} does not imply that of T, as a
non-standard contradiction of T may exist even if T_{0} is
identical to T (incompleteness theorem). As such a contradiction means that T has
no model in the universe, models of T_{0} may either have the above
failure (in the infinite case), or only exist outside this universe.
Classes, sets and meta-sets
For any theory, 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 particular
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 notion of set,
that need to be distinguished as follows.
From
now on, in the above unified framework, the theory T_{0}
describing M and idealized as an object T, will be set theory
itself. Taking it as an identical copy of the set theory serving as framework,
amounts to taking the same set theory with two interpretations, that will
be distinguished by giving the meta- prefix to the use of the framework
interpretation.
Aside generic
interpretations, set theory has a standard kind of interpretation into itself
where each set is interpreted by the class (meta-set) of its elements, and
each function is interpreted by the synonymous meta-function (more details in
1.D).
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);
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).
A kind of theoretical difference between both uses of set theory is irreducible (by the
incompleteness theorem): for any given defined (invariant) axioms list for
T, the existence of a model (universe), or equivalently its consistency,
formalized as a set theoretical statement with the meta
interpretation, cannot be logically deduced (a theorem) from the same axioms.
This statement, or a fortiori that of the existence of a standard interpretation,
thus forms an additional axiom of the set theory so used as framework.
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, which can only be conveniently formalized as classes. So, the notions
of set and function will also be 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 (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
(arguments and parameters). This condition forms 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 like set 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.
In particular, let us see A ∧ B and A ⇒ B as definite if A
is false (with respective values 0 and 1) even if B is not definite. That is,
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 itself 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, which by the above rule can be easily
expressed 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