Set Theory and Foundations of Mathematics
2. Set theory

Sylvain Poirier

2.1. First axioms of set theory

The inclusion predicate

The binary predicate ⊂ of inclusion between sets is defined by : for all sets E and F,

EF ⇔ ∀xE, xF

and read as "E is included in F", or "E is a subset of F", or "F includes E". Properties of inclusion between classes apply.
EE is logically valid. Implications chains also appear as inclusion chains:

(EFG) ⇔ (EFFG) ⇒ EG.

We may use the same notation EF as abbreviation for the inclusion of a set E in a class F (and similarly for other formulas defined from this):

EF ⇔ ∀xE, F(x)

Formulas vs statements

Most set theories (except mainly FST and some strong versions) will only accept bounded formulas as sub-formulas of terms (by the set-builder, and later by the conditional operator) and as possible definitions of predicates (what predicate symbols abbreviate). Open quantifiers will be only allowed in statements (declarared true as axioms or theorems).
In set theory, a statement is a ground formula which can combine the symbols of first-order logic with the regular ones of set theory as follows: it must be made of a chain of open quantifiers, usually all ∀ and often written in words ("for all"), followed by a bounded formula. Proofs will naturally use the deduction rules for open quantifiers (introduction and elimination) by common language articulations.
The above definition of ⊂, basically claiming the predicate symbol ⊂ to abbreviate the bounded formula (∀xE, xF), can also be seen as an example of statement with open quantifiers (∀SetE,F, ) taken as an axiom.

The role of axioms

As explained in 1.9, the role of the axioms of a generic theory, is to express its intended range of models as a selection (class) from a wider notion of "all systems" with structures named by the same language. The logical framework, which holds (describes) this wider notion, can interpret the axioms in each such system, then exclude those where it finds some axiom to be false. Excluded systems remain possible models of different theories described by the same framework. Any statement true in all systems (a logically valid statement) is useless (redundant) as an axiom.

But expressing set theory in its special logical framework not used for other theories, leaves a priori undefined the distinction between its logically valid statements, and its other basic accepted truths which need to be declared as axioms due to their falsity in some "non-universe". Now this distinction can be given sense by converting set theory into a generic theory: let us call axioms of a set theory a list of its basic "true" statements whose translated versions in first-order logic are not logically valid, but form a proper list of axioms for that generic theory to be equivalent to the intended version of set theory. From there, provability in a set theory can be defined as the one given by first-order logic with these axioms.

Converting the binders

When converting set theoretical expressions into first-order logic, the only modified symbols are the binders, as their format of use differs between both frameworks. Let us describe the rules of this conversion.
The function definer (1.8) becomes an infinity of operator symbols: for each term t with one argument and any list of parameters, the whole term (Ext(x)) is seen as the big name of a distinct operator symbol, whose arguments are E and the parameters of t. (Those where every subexpression of t without any occurrence of x is the only occurrence of a parameter, would suffice to define others).
The same goes for the set-builder, which will come as a particular case in 2.2.
The conversion of quantifiers comes by expressing their domains as classes :

(∃xE, A(x)) → (∃x, xEA(x))
(∀xE, A(x)) → (∀x, xEA(x))

Classification of axioms

Axioms of set theories (sometimes with other primitive components) can be classified as follows according to their roles, ordered from the more "primitive" (necessary) components, to the more optional and debatable ones (opening a diversity of acceptable set theories).

Axioms for notions

The formalization of primitive notions by class symbols following 1.7, needs to be completed by the following axioms.

x, ¬(Set(x) ∧ Fnc(x)) : sets are not functions (though it does not matter)
Fnc f, Set(Dom f) : the domain of every function is a set
(Fc) ∀(t,E), Fnc(Ext(x)) : any definite (Ext(x)) is a function

Here and in the below axioms for functions, ∀(t,E) is meant as declaring an axiom schema by second-order universal elimination over the variable functor t with E included in the definiteness class of the term defining t for the given values of parameters (this is the definiteness condition for (Ext(x))). Thus for each term defining t we have an axiom where ∀(t,E) is replaced by

∀parameters, ∀SetE, (∀xE, dt(x, parameters)) ⇒

Axiom of Extensionality

This axiom lets sets be determined by their role (either as ranges for quantifiers, or as the classes they define by ∈), saying that any two sets playing the same role are equal :

set E,F, EFEE = F.

Indeed, EFE means that E and F have the same elements (∀x, xExF), and for any predicate R,

(∀xF, R(x)) ⇔ (∀xE, R(x))

and similarly for ∃. Informally, the elements of a set are given in bulk.

Axioms for functions

Functions are also made determined by their role, by the following axiom

(=Fnc) : ∀Fnc f,g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g.

The function definers are related with the function evaluator by an axiom which can be written in either way:
  1. ∀(t,E), ∀Fnc f, f = (Ext(x)) ⇔ (Dom f = E ∧ ∀xE, f(x) = t(x))
  2. ∀(t,E), Dom(Ext(x)) = E ∧ ∀xE, (Eyt(y))(x) = t(x)
Indeed (Fc) ⇒ (1.⇔(2.∧(=Fnc))).

The proof can be taken as an exercise (click to show)

Assume (Fc) for 2. to be definite.
Abbreviate (Dom f = E ∧ ∀xE, f(x) = t(x)) as [f : E, t], to shorten the above as
  1. ∀(t,E), ∀Fnc f, f = (Ext(x)) ⇔ [f : E, t]
  2. ∀(t,E), [Ext(x) : E, t]
1. ⇔ (2. ∧ 1b.) where

1b. ∀(t,E), ∀Fnc f, [f : E, t] ⇒ f = (Ext(x))

Proof of 1b. ⇒ (=Fnc)
Fnc g, applying 1b. to (g, E) where E = Dom g as ∀x∈Dom g, dg(x) :
Fnc f, [f : E, g] ⇒ f = (Exg(x))
[g : E, g] ∴ g = (Exg(x))
Fnc f, [f : E, g] ⇒ f = g
Proof of (2.∧(=Fnc)) ⇒ 1b.
∀(t,E), ∀Fnc f, ([f : E, t] ∧ [Ext(x) : E, t]) ⇒ f = (Ext(x)). ∎
Note: (Fc) ∧ 1. can also be written

1'. ∀(t,E), ∀f, f = (Ext(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀xE, f(x) = t(x)).

2.2. Set generation principle

Formalizing diverse notions in set theory

Set theory will be extended by additional components to represent diverse kinds of meta-objects (roles played by symbolic systems) directly as objects (which can play them). This can only apply to meta-objects which are "concrete" i.e. object-like enough, in a sense to be clarified : as seen in 1.8 and 1.D, not all classes can be sets, while only the functors whose domains are sets are represented by functions.
Some of those extensions will consist in primitive "definer" symbols (with the relevant axioms) serving to convert into an existing kind of objects some meta-objects (roles) of the same kind :

Other kinds of meta-objects beyond the normal roles of elements, sets and functions, will form new notions : those of operation, relation and tuple will be formalized in 2.3. The new symbols they need are both definers (converting meta-objects into the new objects) and evaluators (interpreting these objects back to their roles as meta-objects).
But, like for unary relations (1.8), these new notions with their role-giving symbols, need not be primitive, as they can be naturally constructed as (represented by) classes of existing objects (sets or functions), which can offer their tools (expressible features) to the new objects. So, these extensions of set theory can be obtained by giving definitions of their definer and evaluator symbols. As the notions of operation and relation can be represented in several useful ways by classes of old objects, which do not represent each new object by the same old object (2.3), functors will be used for translations between the classes playing the roles of these notions in the different ways (2.6, 2.8).

Sets as domains of bounded quantifiers

Bounded quantifiers give sets their fundamental role as ranges of bound variables, unknown by the predicate ∈ which only gives them their role of classes. Technically, the bounded quantifier (∃ ∈ , ) suffices to define the predicate ∈ as

xE ⇔ (∃yE, x = y)

but is not generally definable from it in return by any bounded formula, as its definition involves an open quantifier.
Philosophically speaking, the perception of a set as a class (ability to classify each object as belonging to it or not) does not suffice to provide its full perception as a set, that is the perspective over all its elements as coexisting. This intuitive view of a set as a coexistence of its elements can be seen as supported by the above definition of membership as a form of existence with respect to this set. This way, Russell's paradox means that mathematical objects cannot all coexist as a ultimate totality.

Statement of the principle

For any data of a class C and a quantifier Q defined by given bounded formulas with the same parameters, if the equivalence between Q and ∀C, namely

A, (∀x, C(x) ⇒ A(x)) ⇔ (Qx, A(x))

is proven by second-order universal introduction (*) under a given condition on parameters, then C is a set that can be named by a new operator symbol K added to the language of set theory, with these parameters as arguments, and the following axiom which expresses K = C by double inclusion: for all values of parameters satisfying the condition,

Set(K) ∧ (∀xK, C(x)) ∧ (Qx, xK).

(*) we shall focus on cases whose proofs do not use any axiom obtained from a second order axiom by using A in the definition of its variable structure, though I am not sure if any such use is possible.
This principle will be justified in 2.B.
The equivalence condition between Q and ∀C is equivalently expressible as the following list of 3 statements, where the quantifier Q* defined by (Q*x, A(x)) ⇎ (QxA(x)) will be equivalent to ∃C:

(1) ∀x, C(x) ⇔ Q*y, x=y (in fact we just need ∀x, C(x) ⇒ Q*y, x=y)
(2) Qx, C(x)
(3) ∀A,B, (∀x, A(x) ⇒ B(x)) ⇒ ((Qx, A(x)) ⇒ (Qx, B(x))).

Proof of equivalence (click to show) These 3 properties are already known consequences of «Q = ∀C ». Conversely,
((2) ∧ (3)) ⇒ ((∀C x, A(x)) ⇒ Qx,A(x))
((1) ∧ ∃C x, A(x)) ⇒ ∃y, (Q*x, x=y) ∧ (∀x, x=yA(x)) ∴ ((3) ⇒ Q*x,A(x)) ∎

Main examples

Our first and main use cases of this principle are listed in the following table. To justify all of these, (1) comes by finding C to be the formula so defined from Q, while (3) is ensured by the absence of any "negative" occurrence of A in Q (inside a negation, an equivalence, or left of a ⇒). This leaves (2) as the easy remaining condition to check.
The first column recalls the above generic abbreviations ; each other column gives an effective example. The K line gives the notations for the set theoretical symbols so introduced.

K {yE | B(y)} E Im f {y} {y,z}
C(x) xEB(x) yE, xy y∈Dom f, f(y)=x 0
x=y x=yx=z
dK xE, dB(x) Set(E)∧∀yE, Set(y)
Fnc(f) 1
Qx, A(x) xE, B(x)⇒A(x) yE, ∀xy, A(x) x∈Dom f, A(f(x)) 1 A(y) A(y) ∧ A(z)
Q*x,A(x) xE, B(x) ∧ A(x) yE, ∃xy, A(x) x∈Dom f, A(f(x)) 0
A(y) A(y) ∨ A(z)

The value of the set-builder K={xE | B(x)} first defined in 1.8 as a class, thus with an open quantifier (∀x, xK(xEB(x))) is now re-defined by axioms without open quantifier beyond parameters:

Set(K) ∧ (∀xK, xEB(x)) ∧ (∀xE, B(x) ⇒ xK)

or more shortly Set(K) ∧ KE ∧ (∀xE, xKB(x)). Like the axioms for functions, this is an axiom schema by second-order universal elimination on ∀B, so with all unary predicates B defined by bounded formulas with parameters.
This way, the proof of Russell's paradox would be written
F, (F={xE | Set(x) ∧ xx} ∴ Set(F) ∴ (FF ⇎ (Set(F) ∧ FF))) ∴ FE

The functor ⋃ is the union symbol, and its axioms form the axiom of union.

The set Im f of values of f(x) when x ranges over Dom f, is called the image of f.
We define the predicate (f : EF) that reads «f is a function from E to F », while E and F are sets (definiteness condition which may also be integrated in this definition), as

(f : EF) ⇔ (Fnc(f) ∧ Dom f = E ∧ Im fF)

A set F such that Im fF (i.e. ∀x ∈ Dom f, f(x) ∈ F), is called a target set of f.
The more precise (Fnc(f) ∧ Dom f = E ∧ Im f = F) will be denoted f : EF (f is a surjection, or surjective function from E to F, or function from E onto F).

The empty set ∅ is the only set without element, and is included in any set (∀SetE, ∅ ⊂ E).
Thus, (E=∅ ⇔ E ⊂ ∅ ⇔ ∀xE, 0), and thus (E ≠ ∅ ⇔ ∃xE, 1).
The presence of this constant symbol ∅ ensures the existence of a set; for any set E we also get ∅ = {xE | 0}. We have ⋃∅ =∅.
As (Dom f = ∅ ⇔ Im f = ∅) and (Dom f = Dom g = ∅ ⇒ f = g), the only function with domain ∅ is called the empty function.
That a variable may have empty range, is no obstacle for fixing it. In particular, developing an inconsistent theory means studying a fixed system whose range of possibilities is empty. We may actually need to do so in order to discover a contradiction there, which means to prove that no such system exists.

We can redefine ∃ from the above in two ways:

(∃xE, A(x)) ⇔ {xE | A(x)} ≠ ∅ ⇔ (1 ∈ Im(ExA(x))).

For all x, {x,x} = {x}. Such a set with only one element is called a singleton.

For all x and y we have {x, y} = {y, x}. If xy, the set {x, y} with 2 elements x and y is called a pair.

For any set E, the identity function on E is defined by

IdE = (Exx).


Dom IdE = E = Im IdE
xE, IdE(x) = x.

2.3. Currying and tuples

Formalizing operations and relations

To formalize in set theory every notion of operation (resp. relation) with any fixed arity n>1, acting as n-ary structures between n sets, would involve the following symbols (generalizing the case n = 1 of functions which we took as primitive): Let us give to the operation definers, the following notation which will be later (2.7) justified as reflecting their definitions: in the binary case (n = 2), operations defined by a binary operator A with domains E and F will be written

E×F ∋ (x,y) ↦ A(x,y)

After seeing what operations and relations are (which role they play) let us discuss how they are reducible to something else.
One aspect is that relations are reducible to operations, and vice-versa: These constructions can be useful despite their circularity (they are not decreasing the arity). But for foundational purposes, we need a construction which reduces to lower arity cases, down to sets and functions. There are actually 2 such constructions.


The simplest constructions of the notions of n-ary operation from our primitive tools for functions, are their curried representations, defined as classes of functions by expressing the operation definer as n successive uses of the function definer (one for each bound variable); and thus the evaluator as n uses of the function evaluator. For n=2, this means a binary operation in curried form b with domains E and F, is defined from a binary operator B, and evaluated back as B, by the formulas

b = (Ex ↦ (FyB(x,y)))
Dom b = E ∧ ∀xE, Dom b(x) = F ∧ ∀yF, B(x,y) = b(x)(y)

whose equivalence, similar to the axiom 1. for functions, is deducible from it.
The first domain functor comes as Dom b = E, but the second one, given as common value of all Dom b(x), is only definite for E ≠ ∅. The intermediate function b(x) = (FyB(x,y)) represents the functor defined by B with parameter x (free) and argument y (bound).
This somehow makes each binary operation work as a function evaluator, by giving x the role of a function with argument y ; the curried function evaluator just gives back each function it takes : f ↦ ((Dom f) ∋ yf(y)).

Similarly, the notion of n-ary relation can be defined in curried form as a class, giving the role of definer to a succession of n−1 uses of the function definer and 1 use of the set-builder. The curried form r of a binary relation with domains E and F, is so defined from a binary predicate R, and evaluated back as R, by the equivalent formulas

r = (Ex ↦ {yF | R(x,y)})
Dom r = E ∧ (∀xE, r(x) ⊂ F ∧ ∀yF, R(x,y) ⇔ yr(x))

This leaves no way to define second domain functor (F cannot be restored from r).
These constructions have the defect of breaking the symmetry of role between arguments. The next construction method, by tuples, will preserve this symmetry, and will be usually preferred for this reason.


For any theory and any natural number n, a notion of n-tuple is a notion constructed for its variables to serve as abbreviations for a pack of n variables from previous notions. A 2-tuple is called an ordered pair, a 3-tuple is a triple, a 4-tuple is a quadruple and so on. So each tuple x (so constructed object) represents a meta-function of "interpretation" from this list (meta-set) of n variables, into the model.

The definer and evaluator symbols for tuples take a special form because, while tuples are meta-functions, the role they play in the theory differs from those of functors or functions.

An n-tuple definer is not a binder but an n-ary operator, packing its n variables into one by taking them as its arguments in a parenthesis and separated by commas: ( ,…, ).

Now, each structure (resp. operation, relation) can be re-formalized as a unary structure (resp. a function, a unary relation) with domain a type (resp. a class which is actually a set) of tuples, to be used with the relevant tuples definer. This can be implicitly done by re-interpreting the notation: S(x,y) can be read seeing S either as a binary structure (resp. operation, relation), or as a unary one taking as argument the ordered pair given by the term (x,y) formed by the ordered pair definer with arguments x and y.

The role of n-tuple evaluator is played by a list of n functors called projections which extract each variable from the given pack. This list plays the role of the function evaluator curried in the reverse way, by fixing its meta-argument whose range (the domain of tuples as meta-functions) is not seen by the theory as a set of objects but as a list of n symbols to be taken separately.

The formal details of this construction depend whether we take a generic theory or a set theory.

Tuples axiom

In generic theories, it must be a distinct constructed type for not only each n but also each choice of the type of each of these n variables (if starting from a theory with multiple types - this choice of a list of variables with their types amounts to the choice of a predicate symbol type), but this directly forms a legitimate construction (4.11).
For n=2 (other cases are similar), and a type P of ordered pairs (x,y) where x,y have types E and F, the projections π0 and π1 are related to the ordered pair definer, by the axiom

E x, ∀F y, ∀P z, (x = π0(z) ∧ y = π1(z)) ⇔ (x,y) = z

which implies

P z, (π0(z), π1(z)) = z
E x, ∀F y, π0(x,y) = x
E x, ∀F y, π1(x,y) = y
E x,x', ∀F y,y', (x,y) = (x',y') ⇔ (x = x'y = y')

Tuples in set theory

Set theory having no types only needs one notion of n-tuple for each n. But it faces one difficulty : in order to rigorously justify that all tools of set theory remain applicable to tuples in the same way as to the rest of elements, tuples need to be integrated among elements. Namely, set theory needs to develop its notions of tuples by defining them as classes of already existing elements, instead of simply accepting them by the above constructions, which would leave them as separate types.

For this, since tuples are meta-functions, they are naturally represented by functions. This involves copying their meta-domain, which is a list of symbols, into a set (of elements). Namely, let us represent the domain of considered n-tuples by the set Vn of n numbers from 0 to n−1 all named by constant symbols we shall simply conceive as digits. To justify this as a development of set theory, these digits can be defined by any ground terms with distinct values, such as ∅, {∅}, {∅, {∅}} and endlessly many more sets and functions expressed from there. The notion of n-tuple is then defined as the class of all functions with domain Vn.

Then, the projections are defined by the function evaluator applied to the respective digits, which can be read as disguised in their notations : for all n-tuples x,

iVn, πi(x) = x(i).

This index notation, making a pun of the equivalence between reading the index i as an argument or a meta-argument that means to take the i-th symbol from a list (here πi is the i-th projection), is also commonly used for tuples : xi can be either read as the i-th variable in the tuple x = (x0,…,xn−1), or as a third notation for the same evaluator after x(i) and πi(x).

More tools need to be introduced before defining in set theory the tuple definers (2.4) and the operation definers working with tuples (2.7).

2.4. Uniqueness quantifiers and conditional operator

Uniqueness quantifiers

For all sets FE, all unary predicate A definite on E, and all xE,

xF ⇔ {x} ⊂ F ⇔ (∃yE, x=yyF) ⇔ (∀yE, x=yyF)
xF ⇒ ((∀yF, A(y)) ⇒ A(x) ⇒ ∃yF, A(y))
F ⊂ {x} ⇔ (∀yF, x=y) ⇒ ((∃yF, A(y)) ⇒ A(x) ⇒ (∀yF, A(y)))
F={x} ⇔ (xF ∧ ∀yF, x=y) ⇔ (∀yE, yFx=y)

Here are 3 new quantifiers: ∃≥2 (plurality), ! (uniqueness), and ∃! (existence and uniqueness), whose results when applied to A in E only depend on F={xE | A(x)} (like ∃ and unlike ∀) :

(∃xE, A(x)) ⇔ (F ≠ ∅) ⇔ (∃xF, 1) ⇔ (∃xE, {x} ⊂ F)
(∃≥2xE, A(x)) ⇔ (∃≥2: F) ⇔ (∃x,yF, xy) ⇔ (∃xyE, A(x) ∧ A(y))
(!xE, A(x)) ⇔ (!:F) ⇔ ¬(∃≥2: F) ⇔ (∀x,yF, x=y) ⇔ ∀xF, F ⊂ {x}
(∃!xE, A(x)) ⇔ (∃!:F) ⇔ (∃xF, F⊂{x}) ⇔ (∃xE, F={x})
F ⊂ {x} ⇒ (∀yF, F⊂{y}) ⇔ (!:F)
(∃!:F) ⇔ (F≠∅ ∧ !: F)
F≠∅ ⇒ ((∀yF, B(y)) ⇒ (∃yF, B(y)))
( !: F) ⇒ ((∃yF, B(y)) ⇒ (∀yF, B(y)))
F={x} ⇒ ((∃yF, B(y)) ⇔ B(x) ⇔ ∀yF, B(y))

Single element axiom

Let us introduce a new primitive symbol ℩ to serve as inverse of the singleton functor { } : only definite on the class of singletons d℩E ⇔ (Set(E) ∧ ∃!:E), it gives their unique element, as defined by the single element axiom which can be equivalently written

x, ℩{x} = x
SetE, ∃!:E ⇒ ℩EE

Then for every unary predicate A and every singleton E, A(℩E) ⇔ (∃xE, A(x)) ⇔ (∀xE, A(x)).

Conditional connective

Following conventions from computer science, let us denote the ternary connective «If A then B otherwise C» as

(A ? B : C) ⇔ (¬CAB) ⇔ ((AB)∧(¬AC)) ⇔ (¬A ? C : B)
⇔ ((AB)∨(¬AC)) ⇔((CA)⇒(AB)) ⇎ (A ? ¬B : ¬C)

Any n+1-ary connective K amounts to two n-ary ones: K(A) ⇔ (A ? K(1): K(0)). Thus,

¬A ⇔ (A ? 0 : 1)
(AB) ⇔ (A ? B : 1)
(AB) ⇔ (A ? B : 0)
(AB) ⇔ (A ? 1: B)
(AB) ⇔ (A ? B : ¬B).

Conditional operator

Like the conditional connective, it chooses between two objects x,y depending on the boolean B:

(B ? x : y) = ℩{z∈{x,y}| B ? z=x : z=y} = ℩{z∈{x,y}| z=xB}

so that for any unary predicate A,

A(B ? x : y) ⇔ (B ? A(x) : A(y)).

All para-operators other than connectives but with at least a Boolean argument, are naturally expressed as composed of the conditional operator with operators, or the conditional connective with predicates, which is why they did not need an explicit presence in the language of a theory.

Relations as operations

For a given n, once given the notion of n-ary operation with its definer and its evaluator denoted as in 2.3, the notion of n-ary relation can be defined as a role of the class of n-ary operations with values in V2 = {0,1} (serving as Boolean type), as follows. Booleans B are converted to and from objects bV2, by b = (B ? 1 : 0) and Bb = 1.
So with n=2 (other cases are similar), such a binary operation r with domains E and F gets this role of binary relation, being defined from any binary predicate R, and evaluated back as R, by the formulas

r = (E×F ∋ (x,y) ↦ (R(x,y) ? 1 : 0))
xE, ∀yF, R(x,y) ⇔ r(x, y) = 1

Defining the tuples definers

The ordered pair definer can be defined as a curried view on the conditional operator:

(x,y) = (V2a ↦ (a = 1 ? y : x))

Confusing Booleans with objects, (B ? x : y) = πB(y,x).
Other tuples can be similarly defined in diverse ways, such as

(x,y,z) = (V3a ↦ (a = 2 ? z : (a = 1 ? y : x)))

Given the notion of ordered pairs, the roles of notions of tuples of any higher arity n > 2 can also be played by other classes, with other definitions of their definers and projections, satisfying the same axioms. For example, triples t = (x,y,z) can be defined as t = ((x,y),z)) and evaluated by

x = π00(t))
y = π10(t))
z = π1(t)

2.5. Families and Boolean operators on sets


The notion of family is formally synonymous with that of function, but meant to play roles intuitively similar to those of tuples : while the domains of tuples are finite and made of symbols or numbers, those of families can be more general but still seen as intuitively "simple" sets, fixed in each context of use, and outside the "main studied system" containing the target set. A «family of...» is a family whose image is a «set of... » (included in the said notion).

Families use the formalism of functions disguised in the style of the symbols for tuples (themselves inapplicable due to their finiteness for infinite domains). The evaluator for a family u at i, instead of u(i), is written πi(u) or ui (looking like a meta-variable symbol of variable). The family definer on a term t is written (t(i))iI or sometimes with ellipsis as (t(0),…,t(n−1)) abbreviating the n-tuple definer, instead of Iit(i). The argument i is called index, and the family is said indexed by its domain I. We may write u = (ui)iI as a shorthand for Fnc u ∧ Dom u = I.

When formalizing model theory in set theory, the "lists" of components forming the contents of theories are basically families. More precisely:

Structures and binders

Seeing tuples as particular functions, explains that structures (unary structures on classes of tuples) are particular binders over terms (unary structures on classes of functions defined by these terms: 1.8).
Similarly, logical connectives are particular quantifiers. In particular, ∀ and ∃ respectively generalize the chains of conjunctions and of disjunctions:

(B0∧…∧Bn−1) ⇔ (∀iVn, Bi)
(B0∨…∨Bn−1) ⇔ (∃iVn, Bi)

The distributivity of connectives (1.6) also works for quantifiers as follows. For any unary predicate R definite on E and any Boolean C,

(C ∧ ∃xE, R(x))  ⇔  (∃xE, CR(x))
(C ∨ ∀xE, R(x))  ⇔  (∀xE, CR(x))
(C ⇒ ∀xE, R(x))  ⇔  (∀xE, CR(x))
((∃xE, R(x)) ⇒ C)  ⇔  (∀xE, R(x) ⇒ C)
(∃xE, C) ⇔ (CE≠∅) ⇒ C ⇒ (CE=∅) ⇔ (∀xE, C)

Extensional definitions of sets

The operators of empty set ∅, singleton {a} and pairing {a,b} (2.2) are the first cases (those of arities 0,1,2) of operator symbols of exensional definition of sets (listing their elements) which amount to applying the Im functor to tuples :

{a,b,…} = Im(a,b,…).

The definition of Vn from 2.3 can be written {0,…,n−1}. Images of tuples are finite sets.
Similar notations are used for the binder also given by Im:

{T(x)| xE} = {T(x)}xE = Im(ExT(x))

As this notation looks similar to the set builder, both may be combined into a third notation :

{T(x)| xER(x)} = {T(x)| x∈{yE|R(y)}}

A function f is said constant when !: Im f. The constancy of a tuple is the chain of equalities:

x=y=z ⇔ !:{x,y,z} ⇔ ((x=y)∧(y=z)) ⇒ x=z

Union of a family of sets

The binder of union of any family of sets (F = (Fi)iI ∧ ∀iI, Set Fi), is defined from the previous functor of union of a set of sets (2.2) :

F =
Fi = ⋃{Fi}iI = ⋃ Im F
x, x
Fi ⇔ (∃X∈ Im F, xX) ⇔ ∃iI, xFi

XY = ⋃{X, Y}
x, xXY ⇔ (xXxY)
XYZ = ⋃{X, Y, Z} = (XY) ∪ Z
fnc f, Im f = ⋃x∈Dom f {f(x)}
Fi, A(x)) ⇔ ∀iI, ∀xFi, A(x)
Fi, A(x)) ⇔ ∃iI, ∃xFi, A(x)
Set E,
FiE ⇔ ∀iI, FiE
In return, the union of a set of sets is expressible from that of a family : ⋃ E = ⋃ IdE because Im IdE = E.

Other Boolean operators on sets

A binary predicate with domains a set I and a class C, can be seen in either curried way, as a meta-family (Ai)iI of unary predicates definite in C, or as a family of Boolean variables (Ai(x))iI depending on a common parameter x with range C. This way, any quantifier Q with range I (thus, for finite I, any connective) defines a meta-binder (resp. a meta-operation) on this meta-family (resp. this meta-tuple) of unary predicates (sub-classes of C), with result a unary predicate R, defined as

C x, R(x) ⇔ Qi, Ai(x).

When C is a set E, this defines a genuine binder (resp. operation) acting in the class of subsets of E. However, the result depends a priori not only on the given family of sets but also on the chosen set E. This parameter may be kept implicit as fixed in some contexts, but in others it needs to be explicitly added as argument.

The functor so defined by the negation connective (¬) is the complementE (with set parameter E) : ∁E F is called the complement of F in E. It is synonymous with the following binary operator \ of difference between any two sets, except that ∁E F is considered only definite if FE :

Set E,F, E\F = {xE | xF}
Set E,F, FE ⇒ ∁E F = E\FE ∴ (∀xE, x ∈ ∁E F ⇔ ¬xF)

Let us analyze the issue of the dependence on E in the general case. Any family of sets F = (Fi)iI is a family of subsets of its union U = ⋃iI Fi and of any larger set EU.

In any of these, the existential quantifier (Q = ∃) defines the union binder:

(∀iI, FiE) ⇒
Fi = {xE| ∃iI, xFi}
The binder defined by any Q gives a set X = {xE| R(x)} where R(x) abbreviates (Qi, xFi). For this to define a binder (resp. operation) on the class of all sets, this X must be independent of the chosen EU, and then it can be written

X = {xU| R(x)}.

Noting that

x, xU ∨ (R(x) ⇔ Qi, 0)

the needed independence condition appears to be ¬Qi, 0 which also implies that X coincides with the class R.
The difference operator can be so defined by the connective (A∧¬B) which satisfies this condition ¬(0∧¬0):

Set E,F, ∀x, x∈ E\F ⇔ (xExF).


The quantifier ∀ defines the intersection of any family of subsets Fi of a fixed set E:

Fi = {xE | ∀iI, xFi} = ∁E
E Fi

The condition of independence from E is that I ≠ ∅. As above defined, the intersection of the empty family gives E. The intersection of any non-empty family of sets (I ≠ ∅) can be written

Fi = {xFj | ∀iI, xFi}
x, x
Fi ⇔ ∀iI, xFi
Set G, G
Fi ⇔ ∀iI, GFi
Set E,F, EF = {xE | xF} = FE
x, xEF ⇔ (xExF)

Union and intersection have the same associativity and distributivity properties as ∧ and ∨ :

EFG = (EF)∩G = E∩(FG) = ⋂(E,F,G)

Fi =

Fi =
E∩(FG) =  (EF)∪(EG) E∪(FG) =  (EF)∩(EG)

Finally the connective ⇎ gives the symmetric difference: EF = (EF) \ (EF).

2.6. Graphs

A graph is a set of ordered pairs. Let us denote the class of graphs as gr:

gr R ⇔ (Set R ∧ ∀xR, Fnc x ∧ Dom x = V2).

For any binder Q and any graph G, the formula QzG, A(z0,z1) that binds the variable z = (z0, z1) on a binary structure A definite on G, can be seen as binding 2 variables z0, z1 on A(z0, z1), and thus be denoted with a pair of variables: Q(x,y)∈G, A(x,y).

The transpose of an ordered pair is

t(x,y) = (y,x)

The transpose of a graph R is the image of transposition over it:

tR = {(y,x)|(x,y) ∈ R}

We define the domain and the image of a graph as the respective images of π0 and π1 over it:

Dom R = {x|(x,y) ∈ R}
Im R = {y|(x,y) ∈ R} = Dom tR

Currying notation

Graphs R can be expressed in curried forms as functors R and R:

xR(x) = {y | (z,y)∈Rz=x}.
yR(y) = {x | (x,z)∈Rz=y} = tR (y).
x,y,   yR (x) ⇔ (x,y) ∈ R ⇔ xR (y)
xx ∈ Dom RR (x) ≠ ∅
Dom RE ⇒ Im R = ⋃xE R(x) ∧ ∀y, R(y) = {xE | (x,y) ∈ R}

They can also appear as functions

RE = (ExR(x))
RF = (FyR(y))
(R) = RDom R
(R) = RIm R.

Functional graphs

The graph of a function f is defined by

Gr f = {(x,f(x)) | x ∈ Dom f}
x,y, (x,y) ∈ Gr f ⇔ (x ∈ Dom fy = f(x))
Dom f = Dom Gr f
Im f = Im Gr f

For any function f and any graph R,

Gr fR ⇔ ∀x∈Dom f, f(x) ∈ R(x)
R ⊂ Gr f
⇔ (Dom R ⊂ Dom f ∧ ∀(x,y)∈R, y = f(x))
R = Gr f
⇔ (Dom R ⊂ Dom f ∧ ∀x∈Dom f, R(x) = {f(x)} )

A graph R is functional if it is the graph of a function. This condition is equivalently written in either way

x∈ Dom R, !: R(x)
x,yR, x0 = y0x1 = y1.

It is then the graph of the unique function ℩R = ((Dom R) ∋ x ↦ ℩(R(x))).

For any set E we shall denote 𝛿E = Gr IdE.

Indexed partitions

Two sets E and F are called disjoint when EF = ∅, or equivalently ∀xE, xF.
A family of sets (Ai)iI is called pairwise disjoint when ∀ijI, AiAj = ∅
For any graph R with Im RF, the family (R(y))yF is pairwise disjoint if and only if R is functional:

(∀yzF, ¬∃xR(y), xR(z)) ⇔ (∀(x,y)∈R, ∀zF, xRzy = z)

For any function f and any y we define the fiber of y under f as

f(y) = {x∈Dom f | f(x) = y} = (Gr f)(y)

When f : EF this defines a family fF = (f(y))yF of pairwise disjoint subsets of E:

y,zF, f(y) ∩ f(z) ≠ ∅ ⇒ ∃xf(y) ∩ f(z), y = f(x) = z
yF f(y) = E
Im f = {yF | f(y) ≠ ∅}.

An indexed partition of a set E is a family of nonempty, pairwise disjoint subsets of E, whose union is E.
In other words it is any family of the form f = f•Im f for any function f with domain E.

Sum or disjoint union

The binder ∐ of sum of any family of sets (Ei)iI, gives a graph ∐iI Ei defined as

Ei =
{(i,x) | xEi}
i,x, (i,x) ∈
Ei ⇔ (iIxEi)
Ei, A(i,x)) ⇔ (∀iI, ∀xEi, A(i,x))
(∀iI, EiEi) ⇔ ∐iI Ei ⊂ ∐iI Ei
E0⊔…⊔En−1 = ∐iVn Ei
This binder serves as inverse of currying : R = ∐iI Ei ⇔ (Dom RI ∧ ∀iI, R(i) = Ei).
It is also called disjoint union as the family of copies {(i,x) | xEi} of each Ei is pairwise disjoint, with the function from R to I given by π0.

Direct and inverse images by a graph

The restriction of a graph R to a set A is defined as

R|A = {(x,y)∈R | xA} = ∐xA R(x)

The direct image of a set A by a graph R is
R(A) = Im R|A = ⋃xA R(x) = {y |(x,y)∈RxA} ⊂ Im R.
Dom RA ⇔ R|A = RR(A) = Im R
Ai) =
Ai) ⊂

ABR(A) ⊂ R(B)
Similarly, the inverse image or preimage of a set B by a graph R is

R(B) = tR(B) = ⋃yB R(y) = {x | (x,y)∈RyB} ⊂ Dom R.

Direct image and preimage by a function

The direct image of a subset A ⊂ Dom f by a function f, denoted f[A] or f(A), is
f[A] = (Gr f)(A) = {f(x) | xA} ⊂ Im f
For any f : E → F and BF, the preimage of B by f, written f(B), is defined by

f(B) = (Gr f)(B) = {xE | f(x) ∈ B} =
f(y) = f({y})

f(∁F B) = ∁Ef(B)

For any family (Bi)iI of subsets of F, f(⋂iI Bi) = ⋂iI f(Bi) where intersections are respectively interpreted as subsets of F and E.

2.7. Products and powerset

Cartesian product of two sets

For any two sets E and F, the (cartesian) product E×F is the set of (x,y) where xE and yF.
E×F = ∐xE F

Ei =
(EE′ ∧ FF′) ⇒ E×FE′×F
E×∅ = ∅ = ∅×E
For any graph R,

RE×F ⇔ (Dom RE ∧ Im RF)
R|E = R∩(E× Im R)

Quantifiers over a product have equivalent curried views:

(∃(x,y)∈E×F, A(x,y)) ⇔ (∃xE, ∃yF, A(x,y)) ⇔ (∃yF, ∃xE, A(x,y))
(∀(x,y)∈E×F, A(x,y)) ⇔ (∀xE, ∀yF, A(x,y)) ⇔ (∀yF, ∀xE, A(x,y))
(∃xE, A(x)∨B(x)) ⇔ ((∃xE, A(x)) ∨ (∃xE, B(x)))
(∀xE, A(x)∧B(x)) ⇔ ((∀xE, A(x)) ∧ (∀xE, B(x)))
(∃xE, CA(x)) ⇔ ((CE≠∅) ∨ ∃xE, A(x))
(∀xE, CA(x)) ⇔ ((CE=∅) ∧ ∀xE, A(x))

Quantifiers (Qx,yE, ) can be equivalently written (Q(x,y)∈E×E, ) while the notation QxyE can be read as one quantifier with domain {(x,y)∈E×E | xy} = (E×E) \ 𝛿E.

Finite products, operations and relations

Beyond the binary operator of cartesian product, there is an n-ary product operator between any number n>1 of sets : E0×…×En−1 is the set of all n-tuples (x0,…,xn−1) such that ∀iVn, xiEi.
For example, the ternary product is

E×F×G = ⋃xEyF {(x,y,z) | zG} = {(x,y,z) | ((x,y),z))∈(E×FG}

where the latter notation abbreviates the use of the evaluators for this representation of triples. It can also be seen as directly justified by the set generation principle:

(∀(x,y,z)∈E×F×G, A(x,y,z)) ⇔ (∀xE, ∀yF, ∀zG, A(x,y,z))

This finally justifies the most natural formalization of n-ary operations, as functions with domain a product of n sets, with evaluator given in 2.3. It justifies our first notation of 2.3 for operation definers, as a use of the abbreviated notation of 2.6 for binders on graphs, extensible to any arity.

The notion of n-ary relation R will usually be formalized as that of a set of n-tuples, subset of the product of its domains. This way, a binary relation between sets E and F will be a graph RE×F. The equality relation on a set E is so formalized as 𝛿E, called the diagonal of E×E.
For a formalization which specifies the domains E and F of arguments, we can take the triple (E,F,R).

Translating operators into predicates

The use of any functor symbol K in a generic theory is equivalent to that of a binary predicate symbol R with the functionality axiom

x, ∃!y, xRy

It is meant as the "graph of K", i.e. defined from K by

xRyy = K(x)

Terms of first-order logic using K cannot be re-expressed using R, but formulas can: each formula with each occurrence of K in it, can be written A(K(x)) where x abbreviates a term and A abbreviates a formula as a unary predicate; then equivalently replaced by either of

y, xRyA(y)
y, xRyA(y)

The same goes for other arities : the role of any n-ary operator can be played by an (n+1)-ary predicate with the functionality axiom. This generalization can be explained as replacing the argument by a tuple.
This construction does not fit for the operators of our set theory, due to its use of open quantifiers. Yet it works when domains are sets: n-ary operations can be represented as functional (n+1)-ary graphs.

More primitive symbols

Let us strengthen set theory by 3 extensions that declare more kinds of classes to be sets : powersets, exponentiations and products. These extensions are equivalent, in the sense that accepting anyone of them as primitive suffices to get both others as developments from it. They are similar to those provided by the set generation principle, but no more fit its condition ; this lack of justification has deep connections with incompleteness aspects of mathematics.
To fit our way of formalizing set theory (unlike the ZF way introduced below), each such extension is made of Powerset.Set E, Set ℘(E) ∧ ∀F, F∈℘(E) ⇔ (Set FFE)
We shall abbreviate ∈℘ as ⊂ also in binders: for example (∀FE,…) ⇔ (∀F∈℘(E),…).

Exponentiation.Set E,F, Set FE ∧ ∀f, fFE ⇔ f : EF

Product of a family of sets. The binder ∏ generalizes the finite product operators to any family of sets (∀iI, Set Ei):

x, x
 Ei ⇔ (Fnc(x) ∧ Dom x = I ∧ ∀iI, xiEi).
Like with tuples, the function evaluator curried in the reverse way defines a family of projections πi (keeping implicit their dependence on the given product which is usually fixed in context):

iI, πi : ∏jI EjEi.

These symbols preserve inclusion as follows

FE ⇒ ℘(F) ⊂ ℘(E)
(∀iI, FiEi) ⇒ ∏iI Fi ⊂ ∏iI Ei

Their equivalence

From any of these 3 symbols, both others can be defined as follows.

Ei = {x(
Ei)I | ∀iI, xiEi} = {℩R | R
Ei ∧ ∀iI, ∃!: R(i)}

FE = ∏xE F = {℩R | RE×F ∧ ∀xE, ∃!: R(x)}
℘(E) = {f(1) | fV2E}

Even some cases are expressible from previous tools:

F{a}= {{a}∋xy | yF}
F = ∏∅ = {∅}
℘({a}) = {∅,{a}}
Ei = {(iI ? xi : yi)iIJ | (x,y) ∈
Ei ×
(∃iI, Ei = ∅) ⇒
Ei = ∅
(∀iI, ∃!:Ei) ⇒
Ei = {(℩Ei)iI}

Cantor's Theorem

This famous theorem is simply expressible as

Fnc f, ℘(Dom f) ⊄ Im f.

Proof for the case when all f(x) are sets (to which the general case is reducible):
(E = Dom fF = {xE| xf(x)}) ⇒ (∀xE, xFxf(x)) ⇒ (∀xE, Ff(x)) ⇒ F ∉ Im f.∎

Russell's paradox may be seen as the particular case of Cantor's theorem for f = IdE.

The ZF approach

In the traditional ZF formalism for set theory, each such extension is formalized as first made of a mere statement without any special symbol, keeping ∈ as the only primitive structure:

...y, ∃X, ∀x, xXCy(x).

Namely, the powerset axiom (existence of the powerset) is written ∀E, ∃X, ∀F, FXFE, from which the statements of existence of exponentiations and products come as theorems.
Then, the uses of each symbol K with argument y as above, naming these sets, can be justified as developed from there as abbreviations by the following rules. But our framework does not even allow the first of these cases, because it involves an open quantifier, which cannot be replaced by a bounded formula because these extensions do not fit the condition of the set generation principle.
This impossibility to interpret the equality formula (X=K) means that even a given set identical to a class C, would not be recognizable as such. Hence the need to accept the symbols K as primitive, for giving effective sense to the statement that C coincides with a set.

2.8. Injections, bijections

Composition, restriction

The composite of any 2 functions f,g such that Im f ⊂ Dom g is defined by

gf = ((Dom f) ∋ xg(f(x)))
(f : E → Fg : F → G) ⇒ gf : E → G

(This notation will be abusively kept if g is a functor, in which case this is a schema of definitions).
Similarly with more than 2 functions: adding a third one h : G →H to the above conditions, we define

hgf = (hg)⚬f = h⚬(gf) = (Exh(g(f(x))))

The restriction of a function f to a set A ⊂ Dom f is

f|A = (Axf(x)) = f⚬IdA.
Gr(f|A) = (Gr f)|A
f[A] = Im(f|A)
Fnc f,g, Gr g ⊂ Gr f ⇔ (Dom g ⊂ Dom fg = f|Dom g)

When g is a restriction of f, we also say that f is an extension of g.

Injections, bijections, inverse

A function f is called injective (or : an injection ), if tGr f is a functional graph:

Inj f (∀xx′∈Dom f, f(x) ≠ f(x′))
(∀x,x′∈Dom f, f(x) = f(x′) ⇒ x=x′)
(f : EF) ⇔ (f : EF ∧ Inj f)
Im fF (Inj f ⇔ ∀yF, !:f(y))

The inverse of any injection f, is the function f -1 with graph tGr f:

f -1 = ℩f = (Im fy ↦ ℩f(y))
Gr(f -1) = tGr f
(f -1)-1 = f.

A function f : E → F is said bijective (or a bijection) from E onto F, if it is both injective and surjective :
f : EF (f : EF ∧ ∀yF, ∃!: f(y))
(f : EF ∧ Im f = F)
(f : EF ∧ Inj f)
f -1: FE.
In particular IdE : EE.

Diverse properties

Proposition. Let f : E → F and g : F → G. Then
  1. (Inj f ∧ Inj g) ⇒ Inj(gf)
  2. Inj(gf) ⇒ Inj f
  3. Im(gf) = g[Im f] ⊂ Im g.
  1. x,yE, g(f(x)) = g(f(y)) ⇒ f(x) = f(y) ⇒ x = y.
  2. x,yE, f(x) = f(y) ⇒ g(f(x)) = (g(f(y)) ⇒ x = y.
  3. zG, z ∈ Im(gf) ⇔ (∃xE, g(f(x))=z) ⇔ (∃y∈ Imf, g(y)=z) ⇔ zg[Imf]. ∎
From 3. we can obviously deduce

Im(gf) = G ⇒ Im g = G
Im f = F ⇒ Im(gf) = Im g
(f:EF) ⇒ (g:FGgf:EG)

Let f : E → F, and a function g with Dom g = F. Then, easily,
gf = IdE ⇔ (∀xE, ∀yF, f(x) = yg(y) = x)
⇔ Gr ftGr g ⇔ (∀yF, f(y)⊂{g(y)})
⇔ (∀xE, f(x)∈g(x)) ⇔ (Inj fg|Im f = f -1)
⇒ (Im f = Fg = f -1 ⇔ (Inj g ∧ Im gE))
Proof of the non-obvious step :

(gf = IdE ∧ Inj g ∧ Im gE) ⇒ (∀yF, g(f(g(y))) = g(y) ∴ y = f(g(y)) ∈ Im f)

Proposition. (f : EFg : FEgf = IdE) ⇒ (Im f = F ⇔ Inj gfg = IdFg = f -1).

Proof : (Inj ggfg = g⚬IdF) ⇒ fg = IdF. ∎

Proposition. 1) If f,g are injective and Im f = Dom g, then (gf)-1 = f -1g-1.
2) If f,h : EF and g : FE then (gf = IdEhg = IdF) ⇔ ((g : FE) ∧ f = h = g−1).

1) ∀x∈Dom f, ∀y∈ Im g, (gf)(x) = yf(x) = g-1(y) ⇔ x = (f -1g-1)(y).
Other method: (gf)-1 = (gf)-1gg-1 = (gf)-1gff -1g-1 = f -1g-1.
2) We deduce f = h from f = hgf = h, or from Gr ftGr g ⊂ Gr h. The rest is obvious.∎

Canonical functions

For any objects x,y we shall say that x determines y if there is an invariant functor T (known but kept implicit) such that T(x) = y. Then the role of y as free variable can be played by the term T(x), thus by the use of x.
Similarly, a function f : EF will be said canonical if it is defined as ExT(x) where T is some invariant functor.
Examples of important canonical injections : A bijection f will be said bicanonical if both f and f−1 are canonical.
When a bijection f : E ↔  F is canonical (resp. bicanonical), we shall write f : EF (resp. f : EF); or, with its defining functor φ as φ : EF which means that (Ex ↦ φ(x)) is injective with image F. We shall write EF (resp. EF) to mean the existence of a canonical (resp. bicanonical) bijection, that is kept implicit. These will often look like equality properties on numbers, as the existence of a bijection between finite sets implies the equality of their numbers of elements.
Canonical bijections can fail to be bicanonical especially when their defining functor is not injective:

V2E ⥬ ℘(E)
E ≠ ∅ ⇒ {x}E ⥬ {x}
E×{x} ⥬ E
E×{x} ⇌ {xEE{x}
E×{0} ⇌ E.

This meta-relation between sets is preserved by constructions: if EE′ and FF′ then ℘(E) ⥬ ℘(E'), E×FE′×F′ and FEFE (using the direct image of the graph), and the same for ⇌.
This is how transposition (E×FF×E) extends to both graphs and operations:

℘(E×F) ⇌ ℘(F×E)
fGE×F, tf = (F×E∋(x,y) ↦ f(y,x)) ∈ GF×E.

Sums of functions

The binder ∐ of sum of sets defines canonical bijections (whose inverses, defined by RRI, depend on I):

(℘(E))I ⥬ ℘(I×E)
iI ℘(Ai) ⥬ ℘(∐iI Ai)

Any sum of sets S = ∐iI Ai has its family of natural injections ji given by the curried ordered pair definer :

iI, ji : AiS.

The sum over I of functions fi where ∀iI, Ai = Dom fi is defined by

iI fi = (S ∋ (i,x) ↦ fi(x))
g = ∐iI fi ⇔ (Dom g = S ∧ ∀iI, fi = gji = g(i))

It is the inverse of the currying of binary operations, which we shall denote like for graphs: for any sets E, F and any operation (function) B with domain E×F ≠ ∅ (from which E and F can be restored as E = Dom Dom B and F = Im Dom B, while if E×F = ∅ the notation can be abusively kept while taking E and F from context),

B = (Ex ↦ (FyB(x,y)))
B = tB = (Fy ↦ (ExB(x,y))

Hence the canonical bijections (bicanonical if I = Dom S, thus if E ≠ ∅ in the case I×E)

(∀F : S → Set)
f ∈ (FE)I
Gr fi ⊂ ℘(I×(E×F)) ⇌ ℘((I×EF) ⊃ Gr

Product of functions or recurrying

Both curried forms R and R of graphs RE×F are exchanged by a bijection ℘(F)E  ↔  ℘(E)F defined with parameter F.
The similar bijection between both curried forms of operations with a given domain I×E, is defined by the binder ⊓ of product of functions all with domain E, and indexed by I :

(∀iI, Dom fi = E) ⇒
fi = (Ex ↦ (fi(x))iI)
g, g =
fi  ⇔ (g : E →
Im fi ∧ ∀iI, fi = πig)
(F : I → Set) ⇒ ⊓ :
FiE ⥬ (
Set F ⇒ ⊓ : (FE)I ⥬ (FI)E

These bijections are canonical for nonempty families (I ≠ ∅) as only these determine E, and are usually bicanonical as their inverse uses I which is definable when E ≠ ∅; anyway we shall abusively keep the notation ⥬ for the general case while E remains fixed by the context.
A particular case is the binary product (I = V2):

Fncf,g, Dom f = Dom g = Efg = (Ex ↦ (f(x),g(x)))
 IE×FE ⇌ (I×F)E
Fncf, Gr f = Im(IdDom ff)

2.9. Binary relations on a set

A binary relation on a set E is a relation with both domains equal to E, thus formalized by a graph RE×E. Let us abbreviate E×E as E2 and (x,y) ∈ R as x R y

Preimages and products

For any function f : EF and any binary relation R on F, the preimage of R by f is the binary relation f(R) on E defined as

{(x,y)∈E2 | f(x) R f(y)}

For any family of a binary relations (Ri)iI on respective sets Fi, their product is the binary relation on P = ∏iI Fi defined as

{(x,y)∈P2 | ∀iI, xi Ri yi} = ⋂iI πi(Ri).

(It is actually in canonical bijection with the product of sets ∏iI Ri)
In particular with a constant family : any binary relation on a set F defines one on any FI.

Both operations can be combined in one step: for any family of functions fi : EFi, the relation

{(x,y)∈E2 | ∀iI, fi(x) Ri fi(y)} = ⋂iI fi(Ri)

is the preimage of the product relation of the Ri on P, by the function ⊓iI fi : EP.

These concepts will be later generalized to other first-order structures.

Basic properties

A binary relation R on a set E will be said

reflexive  ⇔  xExRx ⇔  𝛿ER ⇒ Dom R = Im R = E
irreflexive  ⇔   ∀xE, ¬(xRx)
symmetric  ⇔  (∀x,yE, xRyyRx) ⇔ RtRR = tR ⇔ (R) = (R)
antisymmetric  ⇔   ∀x,yE, (xRyyRx) ⇒ x = y
transitive  ⇔   ∀x,y,zE, (xRyyRz) ⇒ xRz

These properties are preserved by transposition, preimages and products, except that the preimage of an antisymmetric relation by a non-injective function may not be antisymmetric, and the empty product (I=∅) is not irreflexive.
In particular for FE, the restriction of a relation RE×E to F, namely R∩(F×F), is its preimage by IdF : FE, thus preserves all properties.

Example. Let AEE and R = fA Gr f. Then

(IdEA) ⇒ R is reflexive
(∀f,gA, gfA) ⇒ R is transitive
(∀fA, f : EEf -1A) ⇒ R is symmetric

For any transitive binary relation R we denote x R y R z ⇔ (x R yy R z) ⇒ x R z.

Preorders and orders

A preorder is a reflexive and transitive binary relation. An order is an antisymmetric preorder.
A preordered set is (an ordered pair of) a set with a chosen preorder on it.
An ordered set is a set with a chosen order, usually written as ≤ or ≤E. The formula xy can be read «x is less than y», or «y is greater than x».
Two elements x, y of an ordered set are said comparable when (xyyx).

On the class of sets, the meta-relation ⥬ (existence of a canonical bijection) is a meta-preorder.
The Boolean pair V2 is naturally ordered by ⇒ which coincides there with the usual order between numbers.
The resulting product order on V2E ⥬ ℘(E) (and thus any set of sets) is that of inclusion (⊂).

Any relation RE×F defines a preorder on E as the preimage by R of the inclusion order:

{(x,y)∈E2 | R(x) ⊂ R(y)}.

Conversely, any preorder R on a set E is so definable from itself in both ways (exchanged by transposition):

x,yER(y) ⊂ R(x) ⇔ x R y ⇔ R(x) ⊂ R(y)

Proof. Transitivity is equivalent to (∀x,yE, x R yR(y) ⊂ R(x)) and to (∀x,yE, x R yR(x) ⊂ R(y)).
Reflexivity is equivalent to the converses:

xE, (∀yE, R(x) ⊂ R(y) ⇒ y R x) ⇔ x R x ⇔ (∀yER(x) ⊂ R(y) ⇒ x R y). ∎

Thus R is the preimage of ⊂ by (R). Moreover,

x,yE, R(x) = R(y) ⇔ (R(x) ⊂ R(y) ∧ R(y) ⊂ R(x)) ⇔ (xRyyRx)

so that (R) is injective if and only if R is an order.
The idea of considering only one order written ≤ on each set E, may be formalized by replacing the ordered set (E,R) by (Im(R), ⊂), though this does not exactly fit the following convention : any subset of an ordered set will be implicitly also ordered by restriction.

Strict and total orders

A strict order is a binary relation both transitive and irreflexive; and thus also antisymmetric.

Strict orders < bijectively correspond to orders ≤ by

x < y ⇔ (xyxy).
xy ⇔ (x < yx = y).

A total order on a set E is an order where all elements are comparable (∀x,yE, xyyx), i.e. (≤ ∪ t≤) = E×E.
Equivalent definitions: A strict total order on a set E is a strict order associated with a total order, i.e. any transitive relation < such that, equivalently

x,yE, x < y ⇎ (y < xx = y)
x,yE, x = y ⇎ (y < xx < y)

Equivalence relations

An equivalence relation is a symmetric preorder.
On any set E, the equality relation 𝛿E is an equivalence relation (as already expressed by the axioms of equality), and the only relation altogether symmetric, antisymmetric and reflexive.
On any product of sets, the product of equality relations is also equality.
The preimage of equality by any f : EF is an equivalence relation on E we shall write ∼f :

f = {(x,y)∈E | f(x) = f(y)} = ∐(ff)
Inj f ⇔ ∼f = 𝛿E

Conversely, any equivalence relation R is so definable from itself : R = ∼R. Indeed

x,yEx R y ⇔ R(y) ⊂ R(x) ⇔ R(x) ⊂ R(y) ⇔ R(x) = R(y)

Quotient functions

Proposition.SetE,F,G, ∀f, (f : EF) ⇒ (GFggf) : GF ↔ {hGE | ∼f ⊂ ∼h}.

Proof : ∀...∀fFE, ∀hGE, H = Im(f×h) ⇒

f ⊂ ∼h(x,x'E, f(x) = f(x′) ⇒ h(x) = h(x′))(∀(y,z), (y′,z′) ∈ H, y=y′ ⇒ z=z)
Dom H = Im f ∧ ∀gGF, h = gfH ⊂ Gr g. ∎

For any functions f,h such that Dom f = Dom h ∧ ∼f ⊂ ∼h, this unique g : Im f ↠ Im h such that h = gf will be called the quotient of h by f:

h/f = (Im fy↦ ℩h[f(y)])
Gr (h/f) = Im (f×h)
Inj f ⇒ (f -1 = IdDom f /fh/f = hf -1)
f = ∼h ⇔ Inj(h/f) ⇒ (h/f)-1 = f/h

In the more general case Im f ⊂ Dom g (without surjectivity of f),

h = gf ⇒ (∼f ⊂ ∼hh/f = g|Im f)
(f  = ∼hf = (g|Im f)−1h)

The formula that ∼f is an equivalence relation,

x,y ∈ Dom f, xf y ⇔ ∼f(x) =  ∼f(y)

where (∼f) = ff, reflects the injectivity of (f) which can be directly seen as

y∈Im f, ∀z, f(y) = f(z) ⇒ f(y) ∩ f(z) = f(y) ≠ ∅ ⇒ y = z.


A partition of a set E is a set of nonempty, pairwise disjoint sets, whose union is E.
In other words, it is a set P of subsets of E such that IdP is an indexed partition of E.
The image of any indexed partition is a partition of the same set: for any function f with image E, Im(f) = f[E] = Im(ff) is a partition of E.
RE×E, if P = R[E] then

(∀x,yE, xR(y) ⇔ R(x) = R(y)) ⇔ (∀xE, ∀AP, xAR(x) = A) ⇔ IdP = (RE)

Thus if R is an equivalence relation then P is a partition.
Inversely, any partition P of E defines a function g and then a graph R by

Dom g = E ∧ (g) = IdPP = Dom (g) = Im g
R = ∐gE×Eg = RE ∴ (P = R[E] ∧ IdP = (RE))

thus R is an equivalence relation on E and

x,yE, xRy ⇔ y∈ ℩{AP | xA} ⇔ (∃AP, xAyA) ⇔ (∀AP, xAyA).

For any equivalence relation R on E, the partition R[E] = Im (R) is called the quotient of E by R, and written E/R, so that

(R) : EE/R.

For any xE, the set R(x) = ℩{AE/R | xA} is called the class of x by R.
For any function f such that Dom f = ER ⊂ ∼f, let us abbreviate f/(R) as f/R:

f/R : E/R ↠ Im f
Inj f/RR = ∼f

So when R = ∼f the role of E/R may be played by Im f.
In particular, any preorder R on a set E gives an equivalence relation RtR, and the role of E/(RtR) may be played by Im (R).

2.10. Axiom of choice

Properties of curried composition

Proposition.Set E,F,G, ∀fFE,
  1. Im f = F ⇒ Inj(GFggf)
  2. (Inj(GFggf) ∧ ∃≥2:G) ⇒ Im f = F
  3. (Inj fG ≠ ∅) ⇒ {gf | gGF} = GE
  4. ({gf | gGF} = GE ∧ ∃≥2:G) ⇒ Inj f
  5. (EFG ≠ ∅) ⇒ {g|E | gGF} = GE
  6. (Inj fE ≠ ∅) ⇒ ∃gEF, gf = IdE
Proofs :
1. done in 2.9 ; simpler proof: ∀g,hGF, (∀xE, g(f(x)) = h(f(x))) ⇔ (∀yF, g(y) = h(y)) ⇔ g=h
2. ( ) ⇒ ∃zz′∈G, (Fyz)⚬f = (Fy ↦ (y ∈ Im f ? z : z′))⚬f ∴ (∀yF, y ∈ Im fz = z′) ∴ Im f = F
3. Inj f ⇒ ∀zG, ∀hGE, h = (Fy ↦ (y ∈ Im f ? h(f -1(y)) : z))⚬f
4. ∀zz′∈G, ∀xE, ∀gGF, gf = (Ey↦ (y = x ? z : z′)) ⇒ ∀yE, f(y) = f(x) ⇒ g(f(y)) = g(f(x)) = zy = x.
5. and 6. are particular cases of 3.∎

The case G = V2 gives the following properties of h = (℘(F)∋Bf(B)) :

Im f = F ⇔ Inj h
Inj f ⇔ Im h = ℘(E)

Moreover {f[A]|AE} = ℘(Im f) because ∀B ⊂ Im f, f[f(B)] = B.

Proposition. For any sets E, F and any function g with domain F,

  1. Inj g ⇒ Inj(FEfgf)
  2. (Inj(FEfgf) ∧ E ≠ ∅) ⇒ Inj g
  3. SetG, ({gf | fFE} = GEE ≠ ∅) ⇒ Im g = G.
1. ∀f,f'FE, (Inj g ∧ ∀xE, g(f(x)) = g(f'(x))) ⇒ (∀xE, f(x) = f'(x)).
2. ∀y,zF, g(y) = g(z) ⇒ g⚬(Exy) = g⚬(Exz) ⇒ (∀xE, y = z) ⇒ (E ≠ ∅ ⇒ y = z).
3. (left as an exercise to the reader).∎

Axiom of choice over a set (ACX)

The axiom of choice (AC) is a statement expressible in any set theory with powerset, which «feels true» and is convenient to accept as an axiom; but we will actually not need it in the rest of this work.

It has several equivalent formulations (in clear, it is the common name of these equivalent statements). The main ones fit the common format (∀SetX, ACX) where ACX means any of the following equivalent formulas with the free variable X in the class of sets:

(AC3X) and (AC4X) are more often used in cases of equality (respectively X = Im g and X = Dom R) which are equivalent to the general cases, as the proofs of equivalence work the same : Other easy deductions are

Dependencies between diverse ACX

A big achievement of mathematical logic was to prove the independence of AC from the rest of set theory: even the very strong ZF system, if consistent, can neither prove nor refute it, as each universe where AC is true includes another one where it is false, and vice versa. This will be further commented in 5.5 (without the details of the proofs which are much too difficult).
The diverse ways in which AC may fail in different universes, can be partly sorted out by specifying for which X does ACX hold. The different ACX depend on each other as follows: The proofs of these implications are easy and left as an exercise to the reader.

Finite choice theorem. If X is finite then ACX.

This will be easily deducible from the case of singletons AC{x} (which is trivial) and the preservation by binary union (ACX ∧ ACY) ⇒ ACXY once finiteness will be formalized (4.6).
Now let us just suggest a schema of proofs, namely one for each number of elements of X. For example the case of X with 3 elements comes down to (AC2V3) whose proof can be written

SetX,Y,Z, (X ≠ ∅ ∧ Y ≠ ∅ ∧ Z ≠ ∅) ⇒ (∃xX, ∃yY, ∃zZ, (x,y,z) ∈ X×Y×Z) ⇒ X×Y×Z ≠ ∅.∎

More statements simply equivalent to AC

Theorem. The following statements are equivalent to the axiom of choice:
(AC5) Any set E of nonempty sets has a choice function: ∅ ∉ E ⊂ Set ⇒ ∏ IdE ≠ ∅.
(AC6) For any partition P of a set E, ∃KE, ∀AP, ∃!: KA.
(AC7) For any sets E,F,G and any g: FG, {gf | fFE} = GE.

(AC2)⇒(AC5) is obvious ;
(AC5)⇒(AC6) : (x∈ ∏ IdPK = Im x) ⇒ (KE ∧ ∀AP, xAKA ∧ ∀BP, xBAAB ≠ ∅ ⇒ A = B)
(AC6)⇒(AC3) : ∀Fnc g, X ⊂ Im g ⇒ ∃K⊂Dom g, (∀A∈ Im(g), ∃! : KA) ∴ ∃f ∈ (Dom g)X, (∀xX, {f(x)} = Kg(x)) ∴ gf = IdX.
(AC1E)⇒(AC7) : ∀hGE, (∀xE, ∃yF, g(y) = h(x)) ⇒ (∃fFE, ∀xE, g(f(x)) = h(x))
(AC3G)⇒(AC7) : ∃jFG, gj = IdG ∴ ∀hGE, jhFEgjh = h.
(AC7)⇒(AC3) : ∀SetX, ∀Fncg, X = Im g ⇒ IdXXX = {gf | f ∈ (Dom g)X}. ∎

Note: (AC5)⇒(AC2) is also easy : ∅ ∉ Im A ⊂ Set ⇒ ∃f ∈ ∏ IdIm A, fA ∈ ∏ A.

There are many more statements equivalent to AC, which will not be of any use in this work, and for which the proofs of equivalence are much harder. Interested readers can find about them elsewhere.

2.A. Time in set theory

Standard universes

Given two universes U1, U2, with U1U2, we shall define 3 distinct versions for the concept of U1 being standard in U2, also called a sub-universe of U2. We first informally introduced such a concept in 1.7 as the preservation of the roles of sets and functions; then in 1.B with the other meaning (STF) of standardness of ℕ, i.e. the interpretation of finiteness (applicable to any universe as mentioned in 1.D).

The general idea is that the structures of U1 (the considered interpretation of symbols of set theory in U1 to make it a universe) must be the restrictions of those used for U2. But it depends which structures we mean, and how we define their restrictions. From the property of preservation by restriction from U2 to U1 we shall specify for each version, more preservation properties on other symbols implicitly follow, thanks to the axioms of set theory in U2. Any structure defined using only symbols with preserved meaning, is also preserved. The structures not preserved are anyway determined in U1 as defined from those of U2 with parameter U1 (as a set or a unary predicate). This is why U1 only needs to be specified as a meta-subset or class in U2, keeping its structures implicit.

Let us focus on specifying what each version of standardness requires on sets (to which the diversity of versions is reducible, as the conditions on functions follow in the way essentially given by the fate of their graphs as sets, after naturally defining standardness for ordered pairs). The first structure for them is their class Set. The condition for this is that Set1 = Set2U1. Yet, arguing that Set is not really a structure but only a source of definiteness classes for effective structures, this condition may be weakened as Set1 ⊂ Set2U1 without essentially affecting the main 3 degrees of standardness described below.

The weak version (coming when seeing the role of sets as given by ∈) is

(ST) : ∈1 = ∈2 ∩ (U1× Set1).

Actually, this condition will suffice to imply (STF) once adopted the axiom of foundation for U2 and further reasonable conditions which will be detailed later. Otherwise we need to add it as another requirement in the concept of standardness, in the form ℕ1 = ℕ2 (if the axiom of infinity is adopted in both) or anyway in terms of the class Fin of finite sets as Fin1 ⊂ Fin2 which is equivalent to Fin1 = Fin2 ∩ Set1 (for reasons a bit subtle).

The intermediate version (mentioned in 1.7: every set coincides with the meta-set of the same elements) is

(ST') : ∈1 = ∈2 ∩ (U2× Set1) ⊂ U1× Set1

i.e. every set in U1 is interpreted by U2 as included in U1. This implies the preservation of bounded quantifiers (if the sub-formula keeps its values, namely does not involve ℘) and of any operator giving a set determined by the data of its elements, namely the operators given by the set generation principle. Special constructions exist (such as those of internal set theory) of sub-universes not fitting this condition and still preserving bounded quantifiers on formulas with parameters in U1; but the equivalence holds with the faithfulness of bounded quantifiers on formulas with parameters in U2 (as we shall see when justifying the set generation principle in 2.B).

The strongest version of standardness also requires the preservation of the powerset symbol ℘ (2.7):

(STP) : ℘1 = ℘2|Set1

This additional condition can also be written without explicit use of ℘ as

(ST") : (ST) ∧ ∀E∈Set1, ∀F∈Set2, F2 EF ∈ Set1

These conditions are related by (ST") ⇔ ((ST') ∧ (STP)) ⇒ (STF).
Indeed, (STF) comes by the fact finiteness is definable from ℘ (independently of any additional assumption which was needed with the mere (ST)) ; this can also be seen considering that arithmetic is specified as a second-order theory, which can be faithfully interpreted by set theory with ℘.
The independence of the axiom of choice (further commented in 5.5) and other statements involving ℘, can be roughly explained by the possibility to construct universes which do not preserve the essential meaning of ℘. Following convenience, one such construction happens to fit (ST'); others may fit (ST) ∧ (STP) but not (ST') while (ST')-standard copies of their results also exist.

Ideally standard universes

For any 3 universes U1U2U3 where U2 is standard in U3,

(U1 is standard in U2) ⇔ (U1 is standard in U3).

Thus the idea to consider the standardness of U1 as an absolute property, independent of the external universe in which it is described... provided that this external universe is itself standard. This does not define standardness as an absolute concept (which cannot be defined anyway), but suggests that such a concept may make ideal sense.

A sub-universe U1 of U2 will be qualified as small in U2 if it is known as a set there. This can be written U1 ∈ Set2 if U2 is also itself (ST')-standard, otherwise ∃X∈Set2, U1 = ∈2(X).

To complete the concept of ideally standard universe, let us postulate that every two standard universes are small sub-universes of a third one.

This ideal is quite reasonable for (ST) and (ST'); but for (ST") it is somewhat more daring. As a first reason, it can be philosophically argued that any universe (standard or not) can be taken as a small sub-universe of another in the sense (ST'), but not always in the sense (ST") because seeing it as a set may provide means to define more subsets of given sets. In particular, any (ST")-standard universe being a small (ST") sub-universe of another, implies its fulfillment of the specification schema.

The realistic view of set theory

From now on we shall assume a fixed version of "standardness" meant as either (ST') with a set theory without powerset, or (ST") with a set theory with powerset. In either case, all bounded expressions keep the same values from a standard universe to another, thus called their standard values.

The above concepts provide a realistic meaning for set theory :

In the next section (2.B) the meaningfulness of the (ST") ideal will appear philosophically equivalent to the realism of admitting ℘ in set theory.

Let us formalize some aspects of the plurality of standard universes which set theory aims to describe in its realistic view.

Standard multiverses (expansion of the set theoretical universe)

Let us call quasi-standard multiverse (resp. standard multiverse) any collection (range) of universes (resp. standard universes), where any 2 of them are small sub-universes of a third one. Let us require it to also contain all sub-universes of its members, a quality easy to fulfill, taking a multiverse where it did not hold and adding all these sub-universes to it. We shall say that the set theoretical universe expands when it ranges over a standard multiverse.

For any quasi-standard multiverse M, its union U = ⋃M forms another universe containing all members of M as small sub-universes. Then, for any expression with any values of its free variables in U there exists some UM containing these values and thus able to interpret the expression; this interpretation being independent of the chosen U, defines that of U. Therefore,

(M is a standard multiverse) ⇔ (the universe U is standard).

But U cannot belong to M, because M has no greatest element. So, no single standard multiverse can ever contain all possible standard universes.
For a (ST")-quasi-standard multiverse, keeping in U the same powerset of a given set as in member universes, may lead to the failure of the specification schema in U. Here comes another side of the postulate attached to the ideal (ST")-standardness : that with (ST")-standard multiverses, this failure never happens.

Can a set contain itself ?

Let us call a set reflexive if it contains itself.
The proof of Russell's paradox [1.8], shows that the class of non-reflexive sets (Set(x) ∧ xx) cannot be a set (as it is not included in any set). So, many sets are non-reflexive ; but can reflexive sets exist ? this is undecidable; here is why.

From any universe U with a nonempty class X of reflexive sets, another universe containing none can be made by 2 different methods On the other hand, universes with reflexive sets can be produced as follows:

Riddle. What is the difference between
Answer (click to show) : The role of the set containing x but not y, played by y in the former universe, is played by x in the latter.

The axiom of foundation, introduced in 5.3 (well-foundedness), will imply the absence of reflexive sets as a particular case ; its undecidability can be proven in ways essentially similar to the above arguments. But for most purposes, this axiom is as useless as the sets it excludes.

2.B. Interpretation of classes

The relative sense of open quantifiers

As the set theoretical universe expands, the values of decidable statements (under the given axioms) must of course stay constant. However, any undecidable statement, as well as any other formula containing open quantifiers and given with fixed values of its free variables (let us call these "open formulas"), may change value from one universe to another.
But if any value of an open formula can only be "the current one" relative to the choice of this universe, the question whether it is constant or variable, that is how things go «elsewhere», is relative to a choice of multiverse. But the realistic view of set theory means to neither assume a fixed universe nor a fixed multiverse. Thus, the natural way for it is to abstain from giving any value to open formulas (beyond decidable statements with known proof or refutation). Indeed, tries to do better would be rather hopeless due to how messy the situation is. Let us review its diverse aspects.

In a multiverse of «all universes» (standard or not) fitting a given consistent axiomatic set theory, the situation was explained in Part 1 :

The realistic view refering to standard universes, leads to another messy situation, first by lack of formal definition for the ideal concept of standardness.
Trying to materialize the concept of "real indefiniteness" of statements as their variability in a standard multiverse M, the behavior of this M is determined by its union U, as M is the range of all small sub-universes of U; this allows to express relevant questions as statements in U.

For example, the variability in M of an existential statement (∃x, A(x) where A is a bounded formula) means there exists in M a universe U where it is false (∀xU, ¬A(x)), and another universe U' where it is true (∃xU', A(x)). But then it is also true in any standard universe containing both U and U', among which some other members of M, and U itself. Such a statement may be called «ultimately true».

But since some statements may vary between acceptable standard universes U, some of these may still vary between the U of acceptable standard multiverses. Indeed, U is just another universe which can be axiomatically described, but only incompletely, for both formal reasons (the incompleteness theorem) and realistic ones (there is no ultimate standard multiverse). Just more statements can be made decidable for U than for U by describing U with a stronger theory T than the theory T given to describe U. Such a stronger T can already be obtained by formalizing this description of U as the union of a quasi-standard multiverse whose members satisfy T (while the standardness of U escapes formalization).
Behind the undecidability of a statement (existential or other), multiple situations may occur. It might (I guess) be always true in one quasi-standard multiverse, and always false in another, while, depending on the statement, either of them (but not both) may be standard. It may vary or not vary between standard universes, but this variability, itself expressible as a statement in the union of a standard multiverse, may be itself undecidable, and eventually vary between standard multiverses.

The undecidability of some statements such as AC, usually reflects the variability, which may also happen among (ST')-standard universes, of the values of the open quantifiers used in these statements when re-written without ℘. In particular, a quantifier ∀x∈℘(E) appears as an open quantifier on the class of subsets of E, while other uses of ℘ either also involve this once translated, or cannot even be translated when the powerset axiom does not hold.

The indefiniteness of classes

Unlike objects which can be compared in formulas by the = symbol, the meta-relation of equality between classes is as indefinite as the open ∀ since both concepts are definable from each other : This indefiniteness can be understood by remembering that, depite being usable as ranges, classes are only meta-objects, basically given as predicates, i.e. synctactically (as a formula with parameters). Like with open quantifiers, this leaves us with both concepts of provable equality (or proven equality), and provable inequality, according to the status (provable or refutable) of this statement of "equality" of classes (∀x, A(x) ⇔ B(x)).

Each universe U interprets each class C as a meta-set of objects P = {xU | C(x)}, and sees it as a set when PU. This condition is expressible by set theory in U as a statement S(C), written equivalently as

P, ∀x, C(x) ⇔ xP
E, ∀x, C(x) ⇒ xE

The equivalence is because P can be defined from such an E by P = {xE | C(x)}.
Having two open quantifiers, it is "more indefinite" than the equality between classes.

Classes and sets in expanding universes

Aside this formulation S(C) in a fixed universe, let us analyze this distinction of sets among classes (and thus what makes other classes indefinite), from the perspective of a quasi-standard multiverse. There, this concept has 3 possible versions, ordered only approximately by implications which "often work" but have exceptions.

But the ultimate realistic meaning of set theory is to refer to the range of "all standard universes", which differs from the concept of standard multiverse in that this range is not a set but a class. So, the concept of union cannot apply to this range, and yet its impossible result would form the ideal interpretation of set theory. This ideal can be well approximated by interpretations of set theory by either fixed universes or quasi-standard multiverses (whose existence is ensured by the completeness theorem). Both perspectives, in terms of a fixed vs. a variable universe, alternatively transcend each other endlessly along its expansion.

This explains how any intended set theory can be formalized by mere first-order axioms: if any intended property of the universe was only expressible by a second-order statement, or if anyhow its expression involved external objects (regarding this universe as a set), then it could be re-expressed by moving the framework, as the stronger first-order axiom of existence of a sub-universe of this kind, and why not also endlessly many of them, forming a standard multiverse (stating that every object is contained in such a sub-universe).

Justifying the set generation principle

Let B be a quantifier defined by a bounded formula whose parameters take values in a sub-universe U of any other universe we might work in. Let E be the range of all values taken by the argument y of A when interpreting (By, A(y)). It is independent of A and included in U insofar as A is absent from any expression of y in the defining formula. Typical exceptions would be when B involves a formula of the form A(t({xF|A(x)})) for some term t, in which case defining E as the set of possible values of y would require to assume ℘ and the (ST")-standardness of U. Without these assumptions, such exceptional formulas need to be excluded from the definitions of B for the justifications to work. Anyway they are excluded by understanding, as explained in 2.A-2.B, the set-builder as the notation for the operator symbols from an infinite list, one for each formula using the language of set theory to which A does not belong. (The set-builder is needed to put a formula inside a term, unless the conditional operator is accepted as primitive, which is acceptable, but then, function definers using A by the conditional operator are excluded for the same reason)

Let C(x) defined as (By, y = x). By the hypothesis of the set generation principle for the B which was written Q*, we have a proof of (B ⇔ ∃C). This implies ¬(By, 0), and, coming by second-order universal introduction, remains valid in any universe where it is interpreted.

For any x, the value C(x) of B on the predicate (y ↦ (y = x)), can only differ (be true) from its (false) value on (y ↦ 0), if both predicates differ inside E, i.e. if x belongs to E :

C(x) ⇔ ((By, y = x) ⇎ (By, 0)) ⇒ (∃yE, y = x ⇎ 0) ⇔ xE

This inclusion of C in E shows it is essentially a set: For any class satisfying the condition of the set generation principle (being indirectly as usable as a set in the role of domain of quantifiers), is it also indirectly as usable as a set in the role of domains of functions (before using this principle) ? Namely, is there for each such class a fixed formalization (bounded formulas with limited complexity) playing the roles of the definer and the evaluator for functions having this class as domains ? The answer would be yes, but we shall not develop the justifications here.

Concrete examples

A set: Is there any dodo left on Mauritius ? As this island is well known and regularly visited since their supposed disappearance, no surviving dodos could still have gone unnoticed, wherever they may hide. Having not found any, we can conclude there are none. This question, expressed by a bounded quantifier, has an effective sense and an observable answer.

A set resembling a class: Bertrand Russell raised this argument about theology: «If I were to suggest that between the Earth and Mars there is a china teapot revolving about the sun..., nobody would be able to disprove my assertion [as] the teapot is too small to be revealed even by our most powerful telescopes. But if I were to go on to say that, since my assertion cannot be disproved, it is intolerable presumption on the part of human reason to doubt it, I should rightly be thought to be talking nonsense.» The question is clear, but on a too large space, making the answer practically inaccessible. (An 8m telescope has a resolution power of 0.1 arcsec, that is 200m on the moon surface)

A class: the extended statement, «there is a teapot orbiting some star in the universe» loses all meaning: not only the size of the universe is unknown, but Relativity theory sees the remote events from which we did not receive light yet, as not having really happened for us yet either.

A meta-object: how could God «exist», if He is a meta-object, while «existence» can only qualify objects? Did apologists properly conceive their own thesis on God's «existence» ? But what are the objects of their faith and their worship ? Each monotheism rightly accuses each other of only worshiping objects (sin of idolatry): books, stories, beliefs, teachings, ideas, attitudes, feelings, places, events, miracles, healings, errors, sufferings, diseases, accidents, natural disasters (declared God's Will), hardly more subtle than old statues, not seriously checking (by fear of God) any hints of their supposed divinity.

A universal event: the redemptive sacrifice of the Son of God. Whether it would have been theologically equivalent for it to have taken place not on Earth but in another galaxy or in God's plans for the Earth in year 3,456, remains unclear.

Another set reduced to a class... The class F of girls remains incompletely represented by sets: the set of those present at that place and day, those using this dating site and whose parameters meet such and such criteria, etc. Consider the predicates B of beauty in my taste, and C of suitability of a relationship with me. When I try to explain that «I can hardly find any pretty girl in my taste (and they are often unavailable anyway)», i.e.

(∀F x, C(x) ⇒ B(x)) ∧ {xF | B(x)}≈Ø,

the common reaction is: «Do you think that beauty is the only thing that matters ?», i.e.

What,(∀xF, C(x) ⇔ B(x)) ????

then «If you find a pretty girl but stupid or with bad character, what will you do ?». Formally : (∃xF, B(x) ⇏ C(x) !!!). And to conclude with a claim of pure goodness: «I am sure you will find !», that is (∃ plenty of xF, C(x)). Not forgetting the necessary condition to achieve this: «You must change your way of thinking».
... by the absence of God...
: F would have immediately turned into a set by the existence of anybody on Earth able to receive a message from God, as He would obviously have used this chance to make him email me the address my future wife (or the other way round).
... and of any substitute: a free, open and efficient online dating system, as would be included in my project, could give the same result. But this requires finding programmers willing to implement it. But the class of programmers is not a set either, especially as the purpose of the project would conflict with the religious moral priority of saving God's job from competitors so as to preserve His salary of praise.

2.C. Concepts of truth in mathematics

Let us recall and expand on the different concepts of «truth» we saw for mathematical statements, from the simplest to the most subtle.

The most basic was the relative truth (further analyzed in 1.B), that is the Boolean value of any statement expressed in any given theory, depending on the system (model of the theory) where it is interpreted; this system is supposedly fixed like an implicit free variable. More generally, any formula takes a Boolean value for fixed values of its free variables in that system.

Then comes provability in any given first-order axiomatic theory ; this coincides with the quality of being relatively true in all its models.

Finally, come the truths in two realistic theories : arithmetic and set theory. Let us review them in more details.

Arithmetic truths

As explained in 1.C, the concept of provability in any explicit first-order theory, and more generally any effective "provability" concept (predicate) over the class of statements of any conceivable theory, must be a FOT-existential predicate, equivalent (through some encoding) with some existential predicate of arithmetic. But we need to refer to the realistic truth of arithmetic to interpret these. This is an ideal but clear concept (independent of any ontological hypothesis about infinities), meaning the class of properties of "the standard model ℕ of arithmetic" (to say in short, as all standard models of arithmetic are identical copies of each other).
Indeed all standard objects of a FOT being finite can be accepted as real (no matter how big), while their distinction with non-standard objects (pseudo-finite ones) is also real despite being not formalizable.
The meaningfulness of statements can be understood first for bounded formulas, then those with 1 open quantifier, such as provability or consistency statements, whose objects are mere finite systems (proofs). And so on for each additional open quantifier over a previously accepted formula, even if their meaningfulness becomes more and more subtle.

Yet the incompleteness theorem showed that this realistic truth predicate of arithmetic is not itself an existential predicate. More precisely, even the negation of the provability predicate of any explicit theory able to express arithmetic, cannot be itself an existential predicate.

Still we need partial solutions: existential classes of statements of arithmetic with both qualities The natural way to progress in the endless and non-algorithmic quest for larger and larger such classes without breaking FOT-soundness, consists in searching for stronger and stronger axiomatic set theories. Let us comment this further.

More concepts of strength

Any axiomatic set theory (or other foundational theory) T is reflected by 2 classes of arithmetical statements :
  1. The class of its arithmetical theorems ;
  2. The statement of its consistency.
Both should not be confused : They lead to two other conceptions (definitions) of a "strength" preorder between foundational theories, most often equivalent to our first one of 1.A (possible cases of non-equivalence will not be considered here) :
  1. The inclusion order between their classes of arithmetical theorems ;
  2. The deducibility (provable implication) between consistency statements: T' is stronger than T if the consistency of T is deducible from the consistency of T'; then T' is "strictly stronger" than T if the consistency of T is a theorem of T'.
(1. would be related to the implication order between statements of FOT-soundness, except that the expression of such statements requires a framework strong enough to express arithmetical truth, such as MT).

If T' can prove the existence of a standard model of T then T' is strictly stronger than T in both ways.

Set theory from realism to axiomatization

For an axiomatic set theory to give a class of arithmetical theorems both FOT-sound and large, it needs to be "not wrong and yet very good" : Among sound, well-described set theories (or other foundational theories) there can be no strongest one : from any of them T we can get stronger ones, at least arithmetically, in the following ways roughly ordered by increasing power (where T0 is some possibly weaker theory but which fits the below "open" quality): And these are only the first of an open-ended range of possible methods with growing efficiency in their strengthening effect with respect to the added complexity of description. It actually turns out that the Replacement schema, used in ZF set theory, amounts to the use of a much more powerful strengthening method than these.

Arguments to justify any strong axiomatic set theory like this as a valid foundation of mathematics, must remain somewhat philosophical, and thus assessed in intuitive, not completely formalizable ways, since their point is to do better than any formal proof or other predefined algorithm: no fixed formal method can always witness for any strong theory when it is consistent, even less when it is FOT-sound (by truth undefinability), or sound (the idea that some given axiom which excludes one size of standard universe still accepts some larger ones).

The usefulness of strong axiomatic set theories for proving large classes of arithmetical truths (insofar as philosophical disputes on the ontological status of the ideals motivating these theories do not undermine the role of these ideals as reasons for the confidence in the FOT-soundness), can then be read as an indispensability argument for the reality of the universes so described, beyond the infinity of ℕ.
Indeed, it makes these theories "valuable", while their consistency together with the mere existence of ℕ, ensure the existence of models. Only non-standard models are so ensured to exist, but these work similarly to the standard ones which were ideally meant anyway. Hence our last concept of truth, which is the truth of set theoretical statements.

Axioms compatibility condition

Given several axiomatic set theories with both qualities (sound and strong), consider the theory obtained as their union (the union of their classes of axioms if they have the same symbols, for example if all only use ∈, like ZF). It will be stronger than each, but is it still sound ? Let us qualify a collection of set theories (or their axioms) as compatible if their union (conjunction) remains sound.
So, beyond the soundness and strength of axiomatic set theories, we need an additional quality requirement for their axioms, so that, without limiting the strength of sound set theories which can be so written, all such theories will be compatible. Actually this problem has a natural solution. This needed additional quality is another ideal concept, not completely formalizable, so let us first express it intuitively : This is meant as more specific than the mere "eternity is a very long time" which rephrases the quality "large" for universes, and as deepening our previous concept of being open. Let us explain it in several steps.

First, no axiom should put any limit on the size of the universe, for compatibility with set theories stronger than this size (for example, a sound theory T accepting only one standard universe would be incompatible with the statement of existence of a standard universe of T).

Then, the remaining risk for several statements to be incompatible, is if the values of at least 2 of them endlessly vary (alternating truth and falsity) as the universe expands, in such a way that no standard universe "larger than some size" can fit all (their conjunction would limit the size of the universe). This is resolved by only accepting "open" axioms, which will all agree on "open" standard universes. Let us explain how.

Consider such a variable statement : written in prenex form it must be using both kinds of open quantifiers. Let us analyze the case of statements with only 2 open quantifiers: ∃x, ∀y, A(x,y), among which the statements S(C) that some class is a set. (From this, the case ∀x, ∃y is deduced by negation, while cases with more open quantifiers would be trickier and will not be discussed here). For any standard multiverse where it indeed endlessly varies, such a statement turns out to be false in its union. So, taking such a statement as an axiom would be inappropriate for this multiverse. Yet, what really matters is the behavior of the class of all standard universes (there is no systematic way to determine this, but it is our intended ideal). Now the point of a statement being "open", is that it reflects the truth in the union of a multiverse which behaves like the intended class of all standard universes.

Such "open" universes, with the same properties as the union of a standard multiverse behaving like the class of "all standard universes", can be intuitively described as "much larger than any smaller one" : there must be no limit to how bigger the universe is from any sub-universe (described by a weaker theory). This also avoids the inefficiency that could be involved in the opposite case, of an axiomatic system likely to be significantly more complex but only slightly stronger than another one.

The quest for axiomatic set theories approaching all 3 ideally conceived qualities (strong and open but still sound) aiming to select universes with the corresponding 3 qualities (large and open but still existing among standard ones), is endless. Fortunately, rather simple set theories such as ZF, already satisfy these qualities to a high degree, describing much larger realities than usually needed. This is how a Platonic view of set theory (seeing the universe of all mathematical objects as a fixed, exhaustive reality) can work as a good approximation, though it cannot be an exact, absolute fact.

Alternative logical frameworks

The description we made of the foundations of mathematics (first-order logic and set theory), is essentially just an equivalent clarified expression of (or other way to introduce) the same version of mathematics as widely accepted. Other logical frameworks already mentioned, to be developed later, are still in the "same family" of "classical mathematics". But other, more radically different frameworks (concepts of logic and/or sets), called non-classical logic, might be considered. Examples: We will ignore such alternatives in the rest of this work.