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 :
  1. All such S belong to E
  2. 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 sub-term with type K, thus does not use V (which has an argument of type K).

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 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 re-writes 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:

The unified framework of theories

Since a complete formalization of 1TT (as strong as arithmetic), and thus 1MT, requires a second-order axiom (to exclude pseudo-finite «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 T0 be the external theory, also inserted in set theory, which looks like a copy of T as any component k of T0 has a copy as an object serving as a component of T. Formally, T0 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 T0 with infinitely many components, as an object cannot be defined as depending on an infinity of meta-objects. Any infinite list of components of T0 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 (set-theoretical and model-theoretical): all works of the theory T0 (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 (set-theoretical) model of T0.
But as a first-order theory, set theory cannot exclude universes with a non-standard FST part (i.e. containing pseudo-finite systems), in which the following discrepancies between T0 and T may occur : So understood, the validity limits and conditions of this unified framework of theories, 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 the above unified framework to a set theory, expands the tools of interpretation of set theory into itself (1.7). Namely, consider choosing T0 (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 "meta-universe").

But by the incompleteness theorem (1.C), both uses (versions) of set theory must differ as follows. The statement of existence (in the meta-universe) 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:

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 (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 from there beyond again (a meta-meta-universe) 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).

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