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 :
 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).
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.
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 subterm with type K, thus does
not use V.
The notion of "structure" in 1MT (onemodel
theory in firstorder 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.
This similarity
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 rewrites 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
daring options:
 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
result.
The unified framework of theories
Like arithmetic (and other FOT), to formalize TT or any 1TT as a complete theory,
requires a secondorder
axiom to exclude nonstandard models with pseudofinite
«expressions» and «proofs». Now, the best environment for such secondorder
theories (giving an appearance of unique determination, though not a real one),
and also for MT or 1MT, is the
insertion
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 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} is the copy of an object serving as a component of T.
In a suitable formalism, T_{0} 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.
But there is no general
inverse definition, of T from a T_{0} with infinitely many
components, as an object cannot be defined from a given infinity of
metaobjects. Any infinite list of components of T_{0} needs to fit
some definition, to get the idealized image T of T_{0} by
interpreting that definition in the universe. (The defining formula must be bounded for
T_{0} to match the above definition from this T).
This forms a convenient framework for describing theories and their models,
unifying both previously mentioned settheoretical and modeltheoretical frameworks :
all works of the theory T_{0} (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 (settheoretical) model of T_{0}.
But as a firstorder theory, set theory cannot exclude nonstandard universes, whose
interpretation of FOTs is nonstandard (with pseudofinite objects). There, the
following discrepancies between T_{0} and T may occur :
 Any T with an infinity of components also has nonstandard
ones; but T_{0} only copies its standard components.
Then a model of T_{0} may fail to be a model of T by not fitting
some nonstandard axioms of T.
 T may be inconsistent while T_{0} is consistent, due to a
nonstandard contradiction (may it use nonstandard axioms or only standard ones).
Such a T has no model in this universe, letting models of T_{0}
either only exist outside it, or also in it with the above described failure to be a model
of T.
So understood, the validity conditions of this unified framework are usually accepted as
legitimate assumptions, by focusing on welldescribed theories, interpreted in standard
universes whose existence is admitted on philosophical grounds.
Set theory as its own unified framework
Applying
this unified framework to the choice of a set theory in the role of T_{0}
(describing M and idealized as an object T), expands the tools of interpretation of set theory into itself
(1.7). As T_{0} coexists 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 "metauniverse".
But the second
incompleteness theorem makes them differ as follows. The statement of existence
(in the metauniverse) 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.
Zeno's Paradox
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
the horizon.
Particles are sent in accelerators closer and closer to the speed of
light.
Can they reach their ends ?
Each example can be seen in two ways:
 the «closed» view, sees a reachable end;
 the «open» view ignores this end, but only sees the movement
towards it, never reaching it.
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
views.
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 (onemodel theory or set theory) escapes this whole. Now set theory has multiple
models, from a universe to a metauniverse (containing more sets : metasets, and
new functions between them) and so on (a metametauniverse...). 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.
Other languages:
FR :
Le cadre ensembliste unifié