1.7. Classes in set theory
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 by the following means.
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». Indeed as will be explained in 4.7
(Non-standard
models of Arithmetic), any first-order theory aiming to describe finite systems
without size limit (such as expressions and proofs) inside its model (as classes
included in a type), will still admit in some models some pseudo-finite ones,
which are infinite systems it mistakes as «finite» though sees them larger than any size
it can describe (as the latter is an infinity of properties which it cannot express as a
whole to detect the contradiction ; these systems will also be called non-standard
as «truly finite» will be the particular meaning of «standard» when qualifying kinds of
systems which should normally be finite).
To fill this gap will require a second-order universal quantifier
(1.9), whose meaning is best expressed (in appearance though not really
completely) after insertion
in set theory (whose concept of finiteness will be defined in 4.5). 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, will be exposed in
Parts 3 and 4, completing the grand tour of the foundations of mathematics
after the formalization
of set theory in a logical 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.
In some proper formalization, 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 forms a convenient unified framework for describing theories interpreted
in models, encompassing both previous ones (set-theoretical and model-theoretical):
all works of the theory T_{0} (expressions, proofs and other
developments), have copies as objects formally described by the model theoretical
development of set theory as works of the theory T. In the same
universe, any system M described as a model of T is indirectly
also a (set-theoretical) model of T_{0}.
This powerful framework is bound to the following limits :
- Starting from an arbitrary theory T_{0} with infinitely many
components, a corresponding T cannot be directly defined, as a definition
must be expressible by finite means and thus cannot depend on an infinity of
meta-objects. Any infinite list of components of T_{0} must be
defined by some rules, for getting T as defined by the same rules.
- The risk for a universe to be non-standard in the sense of containing
pseudo-finite systems (which formalizations of set theory in first-order logic
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 that usually 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 by not fitting some
non-standard components (axioms) of T.
- By the incompleteness theorem, T may be inconsistent while
T_{0} is consistent, either due to non-standard axioms of
T, or to a non-standard contradiction between standard axioms, which
may exist even if these theories are identical (having a finite initial content).
As such a contradiction means that T has no model in this universe
(non-standard «proofs» are only valid in the universe containing them),
models of T_{0} may either have the above
failure (in the infinite case), or only exist outside this universe.
So understood, the conditions of use of this unified framework
of theories, are usually accepted as legitimate assumptions,
by focusing on well-described theories (though no well-described set
theory can be the "ultimate" one as mentioned below), interpreted in standard
universes whose existence is admitted on philosophical grounds;
this will be further discussed in philosophical pages.
Standard universes and meta-sets
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 interpreted by two universes, that will
be distinguished by giving the meta- prefix to the interpretation in the role of
framework.
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 (the synonymous object
and meta-object are
now equal), and each function is interpreted by its synonymous meta-function
(see more details
with how it relates with finiteness).
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 will turn out to be
irreducible (by the incompleteness theorem): for any given (invariant) formalization
of set theory, the existence of a model of it (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, and thus
also the stronger statement of the existence of a standard universe,
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 as domains of its structures, 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 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