1.D. Set theory as a unified framework
Structure definers in diverse theories
Let us call structure definer any binder B which faithfully records the unary
structure (relation, resp. function), defined by any input expression (formula, resp. term)
A on some range E (type, class or set here fixed), i.e. its result S =
(Bx, A(x)) can restore this structure by an evaluator V
(symbol or expression) : ∀E x,
V(S, x) = A(x).
Admitting the use of negation and the possibility to interpret
Booleans by objects (in a range with at least 2 objects, which is often
the case), Russell's paradox shows that adding both following requirements on
a structure definer in a theory would lead to contradiction :
Let us list the remaining options. Set theory rejects 1. but keeps 2. But since 1.
is rejected, keeping 2. may be or not be an issue depending on further details.
- All such S belong to E
- V can occur in the expression A and use x anyhow in
its arguments. So V(x, x) is allowed, which is expected as 1.
ensures the definiteness of any V(S, S).
Any generic theory (whose ranges of binders are types) can be legitimately
developed (as explained in 4.9) by the construction of a new
type K given as the set of all structures defined by a fixed expression
A for all combinations of values of its parameters.
Indeed a binder with range K abbreviates a successive use of binders
on all the parameters of A. Here A and the interpreting model
come first, then the range K of structures with its evaluator V are
created outside them : A has no sub-term with type K, thus does
not use V.
The notion of "structure" in 1MT (one-model
theory in first-order logic) has this similarity with the notion of set in set theory : the class of
all structures of any fixed symbol
type (beyond constants) is usually not a set, calling "sets" such ranges K (of those
with a fixed defining expression and variable parameters) and their subsets.
can be formalized by gathering all such K of the same symbol type (constructed by
all possible expressions A) into a single type U, with the same evaluator
V (those A might use V but not the range U). This merging of
infinitely many ranges into one, merely re-writes what can be done
without it, as long as variables of type U are only bound on one of
these "sets" K (or equivalently, a range covered by finitely many of them).
In set theory, the ranges of binders are the sets. Thus, beyond its simplifying
advantage of removing types, set theory will get more power by its strengthening axioms
which amount to accept more classes as sets.
Other theories, which we shall ignore in the rest of this work, follow more
- Keeping 1. and rejecting 2. will be shown consistent by
Skolem's Paradox (4.6)
but would be quite unnatural.
Even weirder is NF
("New Foundations", so called as it was new when first published in 1937),
combining 1. with a lighter version of 2. restricting the syntax of A
to forbid occurrences of (x∈x) or any way to define it.
- The most extreme is lambda
calculus, that keeps both points but
tolerates the resulting contradiction by ignoring Boolean logic with its
concept of "contradiction". This "theory" does not describe any object but
only its own terms, seen as computable functions. As a computation system,
its contradictions are computations which keep running never giving any
The unified framework of theories
Like arithmetic (and other FOT), to formalize TT or any 1TT as a complete theory,
requires a second-order
axiom to exclude non-standard models with pseudo-finite
«expressions» and «proofs». Now, the best environment for such second-order
theories (giving an appearance of unique determination, though not a real one),
and also for MT or 1MT, is the
in a strong enough version of set theory (which can define finiteness: see 4.5).
As this insertion turns components into free variables which together designate
the model, their variability removes the main difference between TT and 1TT, and
between MT and 1MT (another difference is that MT can describe inconsistent theories).
This development of model theory from a strong enough version of set theory will
come in parts 3 and 4, completing the grand tour of the foundations of mathematics
after the formalization
of set theory (mainly by parts 1 and 2).
Given a theory T so described, let T0 be the external
theory, also inserted in set theory, which looks like a copy of T as any
of T0 is the copy of an object serving as a component of T.
In a suitable formalism, T0 can be defined from T as made of
the k such that Universe⊨ ⌜k⌝∈T, i.e. the value of the quoting term
⌜k⌝ interpreted in the universe belongs to T. This forms a convenient framework for describing theories and their models,
unifying both previously mentioned set-theoretical and model-theoretical frameworks :
all works of the theory T0 (expressions, proofs and other
developments), have copies as objects (by interpreting their quotes) 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 T0.
But there is no general
inverse definition, of T from a T0 with infinitely many
components, as an object cannot be defined from a given infinity of
meta-objects. Any infinite list of components of T0 needs to fit
some definition, to get the idealized image T of T0 by
interpreting that definition in the universe. (The defining formula must be bounded for
T0 to match the above definition from this T).
But as a first-order theory, set theory cannot exclude non-standard universes, whose
interpretation of FOTs is non-standard (with pseudo-finite objects). There, the
following discrepancies between T0 and T may occur :
So understood, the validity conditions of this unified framework are usually accepted as
legitimate assumptions, by focusing on well-described theories, interpreted in standard
universes whose existence is admitted on philosophical grounds.
- Any T with an infinity of components also has non-standard
ones; but T0 only copies its standard components.
Then a model of T0 may fail to be a model of T by not fitting
some non-standard axioms of T.
- T may be inconsistent while T0 is consistent, due to a
non-standard contradiction (may it use non-standard axioms or only standard ones).
Such a T has no model in this universe, letting models of T0
either only exist outside it, or also in it with the above described failure to be a model
Set theory as its own unified frameworkApplying
this unified framework to the choice of a set theory in the role of T0
(describing M and idealized as an object T), expands the tools of interpretation of set theory into itself
(1.7). As T0 co-exists at the same level with the set theory serving as
framework, they can be taken as exact copies of each other (with no standardness issue),
which amounts to taking the same set theory with two interpretations : M called
"universe", and the framework interpretation called "meta-universe".
But the second
incompleteness theorem makes them differ as follows. The statement of existence
(in the meta-universe) of a universe of any given set theory (and thus also the stronger
statement of existence of a standard universe), cannot be a theorem of the same set
theory used as framework. To add this statement as an axiom or have it as a theorem,
the framework version must be stronger.
Achilles runs after a turtle; whenever he crosses the distance to
it, the turtle takes a new length ahead.
Seen from a height, a vehicle gone on a horizontal road approaches
Particles are sent in accelerators closer and closer to the speed of
Can they reach their ends ?
Each example can be seen in two ways:
In each example, a physical measure of the «cost» to approach and
eventually reach the targeted end, decides which view is «true», according
to whether this cost would be finite or infinite (which may differ from the first
guess of a naive observer). But the realm of mathematics, free from all
physical costs and where objects only play roles, can accept both
- the «closed» view, sees a reachable end;
- the «open» view ignores this end, but only sees the movement
towards it, never reaching it.
As each generic theory can use binders over types, it sees types as wholes (sets)
and «reaches the end» of its model seen as «closed». But any framework encompassing
it (one-model theory or set theory) escapes this whole. Now set theory has multiple
models, from a universe to a meta-universe (containing more sets : meta-sets, and
new functions between them) and so on (a meta-meta-universe...). To reflect the endless
possibilities of escaping any given universe, requires an «open» theory integrating each
universe as a part (past) of a later universe, forming an endless sequence of growing realities,
with no view of any definite totality. The role of this open theory is played by set theory itself,
with the way its expressions only
bind variables on sets.
Le cadre ensembliste unifié