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 :
  1. All such S belong to E
  2. 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 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.
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 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 daring options:

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 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 T0 be the external theory, also inserted in set theory, which looks like a copy of T as any component k 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.
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).

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 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.

Set theory as its own unified framework

Applying 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.

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: 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 (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.

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions,..., meta-objects
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
1.6. Logical connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Axioms and proofs
1.10. Quantifiers
1.11. Second-order quantifiers
Philosophical aspects
1.A. Time in model theory
1.B. Truth undefinability
1.C. Introduction to incompleteness
1.D. Set theory as unified framework
2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations

Other languages:
FR : Le cadre ensembliste unifié