Set theory as a unified framework
Structure definers in diverse theories
Let us call structure definer any binder B which, used on
diverse expressions A, faithfully records the unary structure defined
by A on some range E (type or class defined by an argument
here implicit), 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, namely V(x, x) is allowed, which makes
sense 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.
Generic theories (whose ranges of binders were types) can be legitimately
developed (for reasons specified 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 on a variable S with range K
abbreviates a successive use of binders on all the parameters of A
which replaces S. Here A and the system
interpreting it come first, then the range K of the resulting S
and their interpretations by V are created outside
them : A has no subterm with type K, thus does
not use V (which has an argument of type K).
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 structures defined by a fixed expression with variable
parameters) and their subsets.
This similarity can be formalized by gathering
all such K (in the fully developed theory with all such constructed K
of the same symbol type by all possible expressions A)
to a single type U, interpreted by the same symbol V (which could be already
used by A).
This merely packs into V different structures without conflict
since they come from different types K of the first argument.
This merely rewrites what can be done without it, as long as in
the new theory, the binders of type U stay restricted to one of these
"sets" K (while any range covered a finite list of them is actually
included in a single other one).
In set theory, the ranges of binders are the sets. Thus, beyond the simplifying
advantage of removing types, set theory will get more power when accepting more
classes as sets (or using open quantifiers as in specification axioms).
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 possible 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
results.
The unified framework of theories
Since a complete formalization of 1TT (as strong as arithmetic), and thus 1MT, requires a secondorder axiom (to exclude
pseudofinite
«expressions» and «proofs»), its best natural framework (providing an appearance
of unique determination, though not a real one) is the insertion
in set theory (in which finiteness will be defined in 4.5). As this insertion
turns its components into free variables whose values define its model T (resp.
[T, M]), its variability removes its main difference with TT (resp. MT, which can
also describe theories without models).
So, after the formalization
of set theory in a logical framework, mainly presented in parts 1 and 2 of this work,
the development of model theory from a strong enough version of set theory in parts
3 and 4 will complete the grand tour of the foundations of mathematics.
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
«k» abbreviates the quoting term describing k
as an object, and the truth of this formula means that the value of this term
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 as depending on an infinity of
metaobjects. Any infinite list of components of T_{0} needs to be
defined by some rules, for defining T by the same rules.
This forms a convenient unified framework for describing theories and their models,
encompassing both previous ones (settheoretical and modeltheoretical):
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 (settheoretical) model of T_{0}.
But as a firstorder theory, set theory cannot exclude universes with a nonstandard
FST part (i.e. containing pseudofinite systems), in which 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.
 When T_{0} is consistent, T may be inconsistent due
to a nonstandard contradiction (may it use nonstandard axioms, or only standard ones,
while they are all standard if in finite number).
In this case, T has no model in this universe, so that
models of T_{0} may either only exist outside this universe,
or exist in it with the above described failure to be a model of T.
So understood, the validity limits and conditions of this unified framework
of theories, 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 the above unified framework to a set theory, expands the tools of interpretation of set theory into
itself (1.7). Namely, consider choosing T_{0}
(describing M and idealized as an object T) to be a set theory.
Taking a copy of the set theory serving as framework, amounts to taking the same
set theory with two interpretations (M called "universe" and the framework interpretation
called "metauniverse").
But by the incompleteness theorem
(1.C), both uses (versions) of set theory must differ as follows.
The statement of existence (in the metauniverse) of a universe of any given set theory,
cannot be a theorem of the same set theory used as framework.
The framework must be stronger, with this statement (or the stronger statement of
the existence of a standard universe) as an additional axiom (or theorem from other
additional axioms).
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 world 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 (or classes), it sees these types as wholes
(sets) and «reaches the end» of its model, and thus sees it as «closed». But
any framework for 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 from there beyond again (a metametauniverse)
and so on. As this can be repeated endlessly, we need 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. This role of an open theory will be played by set theory itself,
with the way its expressions only bind
variables on sets (1.8).