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) :
V(S, x) = A(x) for all x in E.
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.
As will be explained in 4.9, extending a generic theory (whose ranges of binders
were the types) by 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, forms a legitimate development of the theory (a construction).
Indeed a binder on a variable structure symbol S with such a 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 firstorder logic (as a onemodel theory) has this similarity
with the notion of set in set theory : for each given symbol type beyond constants,
the class of all structures of that type is usually not a set, calling "sets" such
ranges K (of structures defined by a fixed expression with variable
parameters), or subclasses of these.
The fully developed
theory with the infinity of such new types constructed for all possible expressions A,
can become similar to set theory by gathering to a single type U all constructed types
K of variable structures of the same symbol type (structures over the same sets),
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 remains innocent (rewriting 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 (or covered by finitely many of them, which are actually
included in another 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.
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
Attempts to formalize onemodel theory in firstorder logic cannot completely specify
the metanotions of «expressions» and «proofs». Indeed as will be explained in 4.7
(Nonstandard
models of Arithmetic), any firstorder 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 pseudofinite 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 nonstandard
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 secondorder universal quantifier
(1.10), 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 (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}.
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
metaobjects. 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 nonstandard in the sense of containing
pseudofinite systems (which formalizations of set theory in firstorder logic
cannot prevent, but only a condition of standardness of interpretation
can), leads to the following possible discrepances between
T_{0} and T :
 T_{0} only copies the standard components of
T, ignoring nonstandard ones that usually exist for infinite theories
in a nonstandard universe. Then a model of T_{0}
in this universe may fail to be a model of T by not fitting some
nonstandard components (axioms) of T.
 By the incompleteness theorem, T may be inconsistent while
T_{0} is consistent, either due to nonstandard axioms of
T, or to a nonstandard 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
(nonstandard «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 welldescribed theories (though no welldescribed 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.
Set theory as a unified framework of itself
The above
unified framework is applicable to the case of set theory itself, thus
expanding the tools of interpretation
of set theory into itself already mentioned in 1.7. Namely,
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.
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.
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 its «true»
interpretation, 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 conventional roles, can accept both
interpretations.
Each generic theory is «closed», as it can see its model (the ranges
of its variables) as a whole (that is a set in its set theoretical
formulation): by its use of binders over types (or classes), it
«reaches the end» of its model, and thus sees it as «closed». But
any possible framework for it (onemodel theory and/or set theory)
escapes this whole.
As explained in 1.7, set theory has multiple possible models : from
the study of a given universe of sets, we can switch to that of a
larger one with more sets (that we called metasets), and new
functions between the new sets.
As this can be repeated endlessly, we need an «open» theory
integrating each universe described by a theory, 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).