Set Theory and Foundations of Mathematics
2. Set theory

2.1. First axioms of set theory

The inclusion predicate

E ⊂ F ⇔ ∀x∈E, x ∈ F

(E ⊂ F ⊂ G) ⇔ (E ⊂ F ∧ F ⊂ G) ⇒ E ⊂ G.

E ⊂ F ⇔ ∀x∈E, F(x)

Formulas vs statements

The role of axioms

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

(∃x∈E, A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x ∈ E ⇒ A(x))

Classification of axioms

• The technical axioms give to the primitive notions and symbols their correct roles :
  • The notions of sets and functions, symbolized in 1.7, are axiomatized here in 2.1 : axioms for notions ; axiom of extensionality ; axioms for functions.
  • Unique element (2.4) ;
• Axioms from the set generation principle (2.2) ;
• Strengthening axioms, introduced in 1.A ;
• More optional technical axioms will come later:
  • Axiom of choice (2.10) might be seen as a further specification for the powerset ;
  • Axiom of foundation (evoked in 2.A and expressed in 5.3).

Axioms for notions

∀parameters, ∀_SetE, (∀x∈E, dt(x, parameters)) ⇒

Axiom of Extensionality

∀_set E,F, E ⊂ F ⊂ E ⇒ E = F.

(∀x∈F, R(x)) ⇔ (∀x∈E, R(x))

Axioms for functions

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

1. ∀(t,E), ∀_Fnc f, f = (E ∋ x ↦ t(x)) ⇔ (Dom f = E ∧ ∀x∈E, f(x) = t(x))
2. ∀(t,E), Dom(E ∋ x ↦ t(x)) = E ∧ ∀x∈E, (E ∋ y ↦ t(y))(x) = t(x)

1'. ∀(t,E), ∀f, f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀x∈E, f(x) = t(x)).

2.2. Set generation principle

Formalizing diverse notions in set theory

• Diverse "set-like" classes will be converted into sets (2.2) (thus giving the existence of sets coinciding with these classes);
• Indirectly specified elements will become directly designated (2.4).

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

x ∈ E ⇔ (∃y∈E, x = y)

Statement of the principle

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

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

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

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.

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

Set(K) ∧ (∀x∈K, x∈E ∧ B(x)) ∧ (∀x∈E, B(x) ⇒ x ∈ K)

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

(f : E → F) ⇔ (Fnc(f) ∧ Dom f = E ∧ Im f ⊂ F)

The empty set ∅ is the only set without element, and is included in any set (∀_SetE, ∅ ⊂ E).
Thus, (E=∅ ⇔ E ⊂ ∅ ⇔ ∀x∈E, 0), and thus (E ≠ ∅ ⇔ ∃x∈E, 1).
The presence of this constant symbol ∅ ensures the existence of a set; for any set E we also get ∅ = {x∈E | 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.

(∃x∈E, A(x)) ⇔ {x∈E | A(x)} ≠ ∅ ⇔ (1 ∈ Im(E∋x ↦ A(x))).

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

Id_E = (E ∋ x ↦ x).

Dom Id_E = E = Im Id_E
∀x∈E, Id_E(x) = x.

2.3. Currying and tuples

Formalizing operations and relations

• A list of n domain functors (sometimes not available but not needed since domains are usually fixed by the context);
• Its evaluator is an (n+1)-ary operator (resp. predicate) written in filled form as f(x₀,…,x_n−1), with arguments one n-ary operation (resp. relation) f, and its n arguments x₀,…,x_n−1;
• Its definer binds n variables to their respective ranges on a term (resp. a formula).

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

• The notion of n-ary relation can be constructed as a class of n-ary operations, by taking the Boolean pair as target set, as we did in 1.4 (for predicates) and will formalize in 2.4.
• Inversely, the notion of n-ary operation can be constructed as a class of (n+1)-ary relations (2.7).

Currying

b = (E ∋ x ↦ (F ∋ y ↦ B(x,y)))
Dom b = E ∧ ∀x∈E, Dom b(x) = F ∧ ∀y∈F, B(x,y) = b(x)(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 = (E ∋ x ↦ {y ∈ F | R(x,y)})
Dom r = E ∧ (∀x∈E, r(x) ⊂ F ∧ ∀y∈F, R(x,y) ⇔ y ∈ r(x))

Tuples

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.

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.

Tuples axiom

∀_E x, ∀_F y, ∀_P z, (x = π₀(z) ∧ y = π₁(z)) ⇔ (x,y) = z

∀_P z, (π₀(z), π₁(z)) = z
∀_E x, ∀_F y, π₀(x,y) = x
∀_E x, ∀_F y, π₁(x,y) = y
∀_E x,x', ∀_F y,y', (x,y) = (x',y') ⇔ (x = x' ∧ y = y')

Tuples in set theory

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

∀i∈V_n, π_i(x) = x(i).

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

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

Single element axiom

∀x, ℩{x} = x
∀_SetE, ∃!:E ⇒ ℩E ∈ E

Conditional connective

(A ? B : C) ⇔ (¬C⇒A⇒B) ⇔ ((A⇒B)∧(¬A⇒C)) ⇔ (¬A ? C : B)
⇔ ((A∧B)∨(¬A∧C)) ⇔((C⇒A)⇒(A∧B)) ⇎ (A ? ¬B : ¬C)

¬A ⇔ (A ? 0 : 1)
(A⇒B) ⇔ (A ? B : 1)
(A∧B) ⇔ (A ? B : 0)
(A∨B) ⇔ (A ? 1: B)
(A ⇔ B) ⇔ (A ? B : ¬B).

Conditional operator

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

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

Relations as operations

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

Defining the tuples definers

(x,y) = (V₂ ∋ a ↦ (a = 1 ? y : x))

(x,y,z) = (V₃ ∋ a ↦ (a = 2 ? z : (a = 1 ? y : x)))

x = π₀(π₀(t))
y = π₁(π₀(t))
z = π₁(t)

2.5. Families and Boolean operators on sets

Families

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 u_i (looking like a meta-variable symbol of variable). The family definer on a term t is written (t(i))_i∈I or sometimes with ellipsis as (t(0),…,t(n−1)) abbreviating the n-tuple definer, instead of I ∋ i ↦ t(i). The argument i is called index, and the family is said indexed by its domain I. We may write u = (u_i)_i∈I as a shorthand for Fnc u ∧ Dom u = I.

• The list of abstract types is a set of urelements, serving as indexing set (i.e. domain) for the family of interpreted types
• Both lists of predicate symbols and operator symbols, are families of tuples of abstract types
• Of the list of axioms, only its image matters, which is a subset of the set of all statements.

Structures and binders

(B₀∧…∧B_n−1) ⇔ (∀i∈V_n, B_i)
(B₀∨…∨B_n−1) ⇔ (∃i∈V_n, B_i)

(C ∧ ∃x∈E, R(x))  ⇔  (∃x∈E, C ∧ R(x))
(C ∨ ∀x∈E, R(x))  ⇔  (∀x∈E, C ∨ R(x))
(C ⇒ ∀x∈E, R(x))  ⇔  (∀x∈E, C ⇒ R(x))
((∃x∈E, R(x)) ⇒ C)  ⇔  (∀x∈E, R(x) ⇒ C)
(∃x∈E, C) ⇔ (C ∧ E≠∅) ⇒ C ⇒ (C ∨ E=∅) ⇔ (∀x∈E, C)

Extensional definitions of sets

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

{T(x)| x∈E} = {T(x)}_x∈E = Im(E ∋ x ↦ T(x))

{T(x)| x∈E ∧ R(x)} = {T(x)| x∈{y∈E|R(y)}}

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 = (F_i)_i∈I ∧ ∀i∈I, Set F_i), is defined from the previous functor of union of a set of sets (2.2) :

Other Boolean operators on sets

∀_C x, R(x) ⇔ Qi, A_i(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.

∀_Set E,F, E\F = {x∈E | x ∉ F}
∀_Set E,F, F⊂E ⇒ ∁_E F = E\F ⊂ E ∴ (∀x∈E, x ∈ ∁_E F ⇔ ¬x∈F)

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

X = {x∈U| R(x)}.

∀x, x ∈ U ∨ (R(x) ⇔ Qi, 0)

∀_Set E,F, ∀x, x∈ E\F ⇔ (x∈E ∧ x∉F).

Intersection

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

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

E∩F∩G = (E∩F)∩G = E∩(F∩G) = ⋂(E,F,G)

Finally the connective ⇎ gives the symmetric difference: E ∆ F = (E∪F) \ (E∩F).

2.6. Graphs

gr R ⇔ (Set R ∧ ∀x∈R, Fnc x ∧ Dom x = V₂).

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

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

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

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

Currying notation

∀x,  R⃗(x) = {y | (z,y)∈R ∧ z=x}.
∀y,  R⃖(y) = {x | (x,z)∈R ∧ z=y} = ^tR⃗ (y).
∀x,y,   y ∈ R⃗ (x) ⇔ (x,y) ∈ R ⇔ x ∈ R⃖ (y)
∀x,  x ∈ Dom R ⇔ R⃗ (x) ≠ ∅
Dom R ⊂ E ⇒ Im R = ⋃_x∈E R⃗(x) ∧ ∀y, R⃖(y) = {x∈E | (x,y) ∈ R}

R⃗_E = (E∋x ↦ R⃗(x))
R⃖_F = (F∋y ↦ R⃖(y))
(R⃗) = R⃗_{Dom R}
(R⃖) = R⃖_{Im R}.

Functional graphs

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

∀x∈ Dom R, !: R⃗(x)
∀x,y∈R, x₀ = y₀ ⇒ x₁ = y₁.

For any set E we shall denote 𝛿_E = Gr Id_E.

Indexed partitions

(∀y≠z∈F, ¬∃x∈R⃖(y), x ∈ R⃖(z)) ⇔ (∀(x,y)∈R, ∀z∈F, xRz ⇒ y = z)

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

∀y,z∈F, f_•(y) ∩ f_•(z) ≠ ∅ ⇒ ∃x∈ f_•(y) ∩ f_•(z), y = f(x) = z
⋃_y∈F f_•(y) = E
Im f = {y∈F | f_•(y) ≠ ∅}.

Sum or disjoint union

Direct and inverse images by a graph

R_|A = {(x,y)∈R | x∈A} = ∐_x∈A R⃗(x)

R_⋆(B) = ^tR^⋆(B) = ⋃_y∈B R⃖(y) = {x | (x,y)∈R∧ y ∈ B} ⊂ Dom R.

Direct image and preimage by a function

For any family (B_i)_{i ∈ I} of subsets of F, f_⋆(⋂_i∈I B_i) = ⋂_i∈I f_⋆(B_i) where intersections are respectively interpreted as subsets of F and E.

2.7. Products and powerset

Cartesian product of two sets

R ⊂ E×F ⇔ (Dom R ⊂ E ∧ Im R ⊂ F)
R_|E = R∩(E× Im R)

(∃(x,y)∈E×F, A(x,y)) ⇔ (∃x∈E, ∃y∈F, A(x,y)) ⇔ (∃y∈F, ∃x∈E, A(x,y))
(∀(x,y)∈E×F, A(x,y)) ⇔ (∀x∈E, ∀y∈F, A(x,y)) ⇔ (∀y∈F, ∀x∈E, A(x,y))
(∃x∈E, A(x)∨B(x)) ⇔ ((∃x∈E, A(x)) ∨ (∃x∈E, B(x)))
(∀x∈E, A(x)∧B(x)) ⇔ ((∀x∈E, A(x)) ∧ (∀x∈E, B(x)))
(∃x∈E, C∨A(x)) ⇔ ((C ∧ E≠∅) ∨ ∃x∈E, A(x))
(∀x∈E, C∧A(x)) ⇔ ((C ∨ E=∅) ∧ ∀x∈E, A(x))

Finite products, operations and relations

E×F×G = ⋃_x∈E⋃_y∈F {(x,y,z) | z∈G} = {(x,y,z) | ((x,y),z))∈(E×F)×G}

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

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 R ⊂ E×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

∀x, ∃!y, xRy

xRy ⇔ y = K(x)

∃y, xRy ∧ A(y)
∀y, xRy ⇒ A(y)

More primitive symbols

• A symbol K (namely, two operators and one binder) naming as a set the given class C, with arguments the parameters of C here abbreviated as a family y ranging over the intended definiteness class of K;
• The statement ∀_dK y, Set K(y) ∧ ∀x, x ∈ K(y) ⇔ C_y(x).

Exponentiation. ∀_Set E,F, Set F^E ∧ ∀f, f ∈ F^E ⇔ f : E → F

Product of a family of sets. The binder ∏ generalizes the finite product operators to any family of sets (∀i∈I, Set E_i):

∀i∈I, π_i : ∏_j∈I E_j → E_i.

F ⊂ E ⇒ ℘(F) ⊂ ℘(E)
F ⊂ E ⇒ F^G ⊂ E^G
(∀i∈I, F_i ⊂ E_i) ⇒ ∏_i∈I F_i ⊂ ∏_i∈I E_i

Their equivalence

Even some cases are expressible from previous tools:

Cantor's Theorem

∀_Fnc f, ℘(Dom f) ⊄ Im f.

The ZF approach

∀_...y, ∃X, ∀x, x ∈ X ⇔ C_y(x).

• ∀x∈K means ∀x, C(x)⇒ ;
• The equality (X=K) means (∀x, x ∈ X ⇔ C(x)) or equivalently (∀x∈X, C(x)) ∧ (∀_C x, x ∈ X);
• Any other formulas using K with y free, written as A(K), mean the formula so abbreviated as ∃X, (X=K)∧A(X).
• To justify binding y on terms using K, involves the axiom schema of replacement.

2.8. Injections, bijections

Composition, restriction

g⚬f = ((Dom f) ∋ x ↦ g(f(x)))
(f : E → F ∧ g : F → G) ⇒ g⚬f : E → G

h⚬g⚬f = (h⚬g)⚬f = h⚬(g⚬f) = (E ∋ x ↦ h(g(f(x))))

f_|A = (A ∋ x ↦ f(x)) = f⚬Id_A.
Gr(f_|A) = (Gr f)_|A
f[A] = Im(f_|A)
∀_Fnc f,g, Gr g ⊂ Gr f ⇔ (Dom g ⊂ Dom f ∧ g = f_{|Dom g})

Injections, bijections, inverse

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

f ^-1 = ℩f_• = (Im f ∋ y ↦ ℩f_•(y))
Gr(f ^-1) = ^tGr f
(f ^-1)^-1 = f.

Diverse properties

1. (Inj f ∧ Inj g) ⇒ Inj(g⚬f)
2. Inj(g⚬f) ⇒ Inj f
3. Im(g⚬f) = g[Im f] ⊂ Im g.

1. ∀x,y∈E, g(f(x)) = g(f(y)) ⇒ f(x) = f(y) ⇒ x = y.
   
2. ∀x,y ∈ E, f(x) = f(y) ⇒ g(f(x)) = (g(f(y)) ⇒ x = y.
   
3. ∀z∈G, z ∈ Im(g⚬f) ⇔ (∃x∈E, g(f(x))=z) ⇔ (∃y∈ Imf, g(y)=z) ⇔ z ∈ g[Imf]. ∎

Im(g⚬f) = G ⇒ Im g = G
Im f = F ⇒ Im(g⚬f) = Im g
(f:E ↠ F) ⇒ (g:F ↠ G ⇔ g⚬f:E ↠ G)

(g⚬f = Id_E ∧ Inj g ∧ Im g ⊂ E) ⇒ (∀y∈F, g(f(g(y))) = g(y) ∴ y = f(g(y)) ∈ Im f)

Proposition. (f : E → F ∧ g : F → E ∧ g⚬f = Id_E) ⇒ (Im f = F ⇔ Inj g ⇔ f⚬g = Id_F ⇔ g = f ^-1).

Proposition. 1) If f,g are injective and Im f = Dom g, then (g⚬f)^-1 = f ^-1⚬g^-1.
2) If f,h : E→F and g : F→E then (g⚬f = Id_E ∧ h⚬g = Id_F) ⇔ ((g : F ↔ E) ∧ f = h = g⁻¹).

Canonical functions

• E ⊂ F ⇒ Id_E : E ↪ F
• (x ↦ {x}) : E ↪ ℘(E)
• Gr : F^E ↪ ℘(E×F).

V₂^E ⥬ ℘(E)
E ≠ ∅ ⇒ {x}^E ⥬ {x}
E×{x} ⥬ E
E×F ⇌ F×E
E×{x} ⇌ {x}×E ⇌ E^{x}
E×{0} ⇌ E.

℘(E×F) ⇌ ℘(F×E)
G^E×F ⇌ G^F×E
∀f∈G^E×F, ^tf = (F×E∋(x,y) ↦ f(y,x)) ∈ G^F×E.

Sums of functions

(℘(E))^I ⥬ ℘(I×E)
∏_i∈I ℘(A_i) ⥬ ℘(∐_i∈I A_i)

∀i∈I, j_i : A_i ↪ S.

∐_i∈I f_i = (S ∋ (i,x) ↦ f_i(x))
g = ∐_i∈I f_i ⇔ (Dom g = S ∧ ∀i∈I, f_i = g⚬j_i = g⃗(i))

B⃗ = (E ∋ x ↦ (F ∋ y ↦ B(x,y)))
B⃖ = ^tB⃗ = (F ∋ y ↦ (E ∋ x ↦ B(x,y))

Product of functions or recurrying

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 = V₂):

2.9. Binary relations on a set

Preimages and products

{(x,y)∈E² | f(x) R f(y)}

{(x,y)∈P² | ∀i∈I, x_i R_i y_i} = ⋂_i∈I π_i⋆(R_i).

Both operations can be combined in one step: for any family of functions f_i : E → F_i, the relation

{(x,y)∈E² | ∀i∈I, f_i(x) R_i f_i(y)} = ⋂_i∈I f_i⋆(R_i)

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

Basic properties

A binary relation R on a set E will be said

Example. Let A ⊂ E^E and R = ⋃_f∈A Gr f. Then

Preorders and orders

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

{(x,y)∈E² | R⃗(x) ⊂ R⃗(y)}.

∀x,y∈E, R⃗(y) ⊂ R⃗(x) ⇔ x R y ⇔ R⃖(x) ⊂ R⃖(y)

∀x∈E, (∀y∈E, R⃗(x) ⊂ R⃗(y) ⇒ y R x) ⇔ x R x ⇔ (∀y∈E, R⃖(x) ⊂ R⃖(y) ⇒ x R y). ∎

∀x,y∈E, R⃖(x) = R⃖(y) ⇔ (R⃖(x) ⊂ R⃖(y) ∧ R⃖(y) ⊂ R⃖(x)) ⇔ (xRy ∧ yRx)

Strict and total orders

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

x < y ⇔ (x ≤ y ∧ x ≠ y).
x ≤ y ⇔ (x < y ∨ x = y).

• an order ≤ related with its strict order < by ∀x,y∈E, x < y ⇎ y ≤ x.
• a transitive relation ≤ such that ∀x,y∈E, x ≤ y ⇔ (y ≤ x ⇒ x=y).

∀x,y∈E, x < y ⇎ (y < x ∨ x = y)
∀x,y∈E, x = y ⇎ (y < x ∨ x < y)

Equivalence relations

∼_f = {(x,y)∈E | f(x) = f(y)} = ∐(f_•⚬f)
Inj f ⇔ ∼_f = 𝛿_E

∀x,y∈E, x R y ⇔ R⃗(y) ⊂ R⃗(x) ⇔ R⃗(x) ⊂ R⃗(y) ⇔ R⃗(x) = R⃗(y)

Quotient functions

Proof : ∀...∀f∈F^E, ∀h∈G^E, 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 ∧ ∀g∈G^F, h = g⚬f ⇔ H ⊂ Gr g. ∎

h/f = (Im f ∋y↦ ℩h[f_•(y)])
Gr (h/f) = Im (f×h)
Inj f ⇒ (f ^-1 = Id_{Dom f} /f ∧ h/f = h⚬f ^-1)
∼_f = ∼_h ⇔ Inj(h/f) ⇒ (h/f)^-1 = f/h

h = g⚬f ⇒ (∼_f ⊂ ∼_h ∧ h/f = g_{|Im f})
⇒ (∼_f  = ∼_h ⇒ f = (g_{|Im f})⁻¹⚬h)

∀x,y ∈ Dom f, x ∼_f y ⇔ ∼⃗_f(x) =  ∼⃗_f(y)

where (∼⃗_f) = f_•⚬f, 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.

Partitions

(∀x,y∈E, x∈R⃗(y) ⇔ R⃗(x) = R⃗(y)) ⇔ (∀x∈E, ∀A∈P, x∈A ⇔ R⃗(x) = A) ⇔ Id_P = (R⃗_E•)

Dom g = E ∧ (g_•) = Id_P ∴ P = Dom (g_•) = Im g
R = ∐g ⊂ E×E ∴ g = R⃗_E ∴ (P = R⃗[E] ∧ Id_P = (R⃗_E•))

∀x,y∈E, xRy ⇔ y∈ ℩{A∈P | x∈A} ⇔ (∃A∈P, x∈A ∧ y∈A) ⇔ (∀A∈P, x∈A ⇒ y∈A).

(R⃗) : E ↠ E/R.

f/R : E/R ↠ Im f
Inj f/R ⇔ R = ∼_f

2.10. Axiom of choice

Properties of curried composition

1. Im f = F ⇒ Inj(G^F ∋ g ↦ g⚬f)
2. (Inj(G^F ∋ g ↦ g⚬f) ∧ ∃^≥2:G) ⇒ Im f = F
3. (Inj f ∧ G ≠ ∅) ⇒ {g⚬f | g∈G^F} = G^E
4. ({g⚬f | g∈G^F} = G^E ∧ ∃^≥2:G) ⇒ Inj f
5. (E ⊂ F ∧ G ≠ ∅) ⇒ {g_|E | g∈G^F} = G^E
6. (Inj f ∧ E ≠ ∅) ⇒ ∃g∈E^F, g⚬f = Id_E

The case G = V₂ gives the following properties of h = (℘(F)∋B↦ f_⋆(B)) :

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

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

1. Inj g ⇒ Inj(F^E ∋ f ↦ g⚬f)
2. (Inj(F^E ∋ f ↦ g⚬f) ∧ E ≠ ∅) ⇒ Inj g
3. ∀_SetG, ({g⚬f | f∈F^E} = G^E ∧ E ≠ ∅) ⇒ Im g = G.

Axiom of choice over a set (AC_X)

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

• (AC1_X) ∀_SetE, ∀R⊂X×E, (∀x∈X, ∃y∈E, xRy) ⇒ (∃f∈ E^X, ∀x∈X, xRf(x)).
• (AC2_X) ∀A : X → Set, (∀x∈X, A_x ≠ ∅) ⇒ ∏A ≠ ∅
  (The product of any family of nonempty sets indexed by X is nonempty)
• (AC3_X) ∀_Fnc g, X ⊂ Im g ⇒ ∃f ∈ (Dom g)^X, g⚬f = Id_X
• (AC4_X) ∀_grR, X ⊂ Dom R ⇒ ∃f ∈ (Im R)^X, Gr f ⊂ R.

• (AC1_X)⇒(AC2_X) by R = ∐ A ∧ E = Im R ;
• (AC2_X)⇒(AC3_X) by A = (g_•(x))_x∈X ;
• (AC3_X)⇒(AC4_X) : X ⊂ π₀[R] ⇒ ∃(h×f) ∈ R^X, h = Id_X ∴ Gr f = Im (h×f) ⊂ R ;
• (AC4_X)⇒(AC1_X) obvious.∎

• (AC2_X)⇒(AC1_X) by A_x = R⃗(x) ;
• (AC4_X)⇒(AC3_X) by R = ^tGr g.

Dependencies between diverse AC_X

• ∀_SetX,Y, (AC_X ∧ ∃f, f : Y ↪ X) ⇒ AC_Y
• ∀_SetX,Y, (AC_X ∧ AC_Y) ⇒ (AC_X∪Y ∧ AC_X×Y)
• (AC_I ∧ ∀i∈I, AC_Ai) ⇒ AC_{∐i∈I Ai}

Finite choice theorem. If X is finite then AC_X.

∀_SetX,Y,Z, (X ≠ ∅ ∧ Y ≠ ∅ ∧ Z ≠ ∅) ⇒ (∃x∈X, ∃y∈Y, ∃z∈Z, (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 ⇒ ∏ Id_E ≠ ∅.
(AC6) For any partition P of a set E, ∃K⊂E, ∀A∈P, ∃!: K∩A.
(AC7) For any sets E,F,G and any g: F ↠ G, {g⚬f | f ∈ F^E} = G^E.

Note: (AC5)⇒(AC2) is also easy : ∅ ∉ Im A ⊂ Set ⇒ ∃f ∈ ∏ Id_{Im A}, f⚬A ∈ ∏ 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

The general idea is that the structures of U₁ (the considered interpretation of symbols of set theory in U₁ to make it a universe) must be the restrictions of those used for U₂. But it depends which structures we mean, and how we define their restrictions. From the property of preservation by restriction from U₂ to U₁ we shall specify for each version, more preservation properties on other symbols implicitly follow, thanks to the axioms of set theory in U₂. Any structure defined using only symbols with preserved meaning, is also preserved. The structures not preserved are anyway determined in U₁ as defined from those of U₂ with parameter U₁ (as a set or a unary predicate). This is why U₁ only needs to be specified as a meta-subset or class in U₂, 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 Set₁ = Set₂ ∩ U₁. 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 Set₁ ⊂ Set₂ ∩ U₁ 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) : ∈₁ = ∈₂ ∩ (U₁× Set₁).

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

(ST') : ∈₁ = ∈₂ ∩ (U₂× Set₁) ⊂ U₁× Set₁

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

(STP) : ℘₁ = ℘_2|Set1

(ST") : (ST) ∧ ∀E∈Set₁, ∀F∈Set₂, F ⊂₂ E ⇒ F ∈ Set₁

Ideally standard universes

(U₁ is standard in U₂) ⇔ (U₁ is standard in U₃).

A sub-universe U₁ of U₂ will be qualified as small in U₂ if it is known as a set there. This can be written U₁ ∈ Set₂ if U₂ is also itself (ST')-standard, otherwise ∃X∈Set₂, U₁ = ∈⃖₂(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

The above concepts provide a realistic meaning for set theory :

• Generic theories, seen axiomatically, are meant to be interpreted in a fixed model containing all values of variables and expressions;
• But set theory aims to "locally" interpret in the standard way any expression with fixed values of its free variables, independently of the choice of a standard universe, containing these values, where this interpretation may be processed.

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)

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 U∈M 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).

Can a set contain itself ?

• Take U\X as class of objects, and turn into urelements all sets E which contained a reflexive set (∃x∈E, x∈x), and all functions whose domain or image was such an E. (These sets cannot be rebuilt from the data of their elements, since each one has an element removed from the universe, namely itself ; any class of urelements can also be eliminated in the same way, turning other objects into urelements).
• Progressively rebuild a universe from scratch: this avoids all reflexive sets. Namely, from a given universe, first accept its urelements, then also accept, progressively along an endless "time", every set only made of previously accepted objects, and every function only involving such objects. Each set so accepted at some time, is formed as a collection of previously accepted objects. At the first time a set is so accepted as a collection of previously available objects, it could not be available yet as a possible element, thus it cannot be reflexive.
  As the reflexivity of a set is independent of context, a union of universes each devoid of reflexive sets, cannot contain one either.

• a universe with an urelement x and a non-reflexive set y such that x ∈ y,
  
• and a universe with a reflexive set x and an urelement y such that y ∉ x ?

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

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

• The variability of value of a statement there, is equivalent to its undecidability (completeness theorem);
• However, this undecidability, when true, cannot anyway be proven by the same axiomatic set theory (incompleteness theorem).

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 (∀x∈U, ¬A(x)), and another universe U' where it is true (∃x∈U', 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».

The indefiniteness of classes

• The equality of classes A = B would be defined by ∀x, A(x) ⇔ B(x);
• The statement (∀x, A(x)) means A = 1 (the universe, class of all objects).

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

∃P, ∀x, C(x) ⇔ x ∈ P
∃E, ∀x, C(x) ⇒ x ∈ E

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.

• The "weak" version is to claim S(C) true in all members of this multiverse. That means C always coincides with some set P, but this may be a different P from one universe to another.
• The "strong" version requires P to stay constant. This can be seen as the meaning behind the formal choice of naming P by a symbol of set theory, as was discussed with the powerset (2.7). But just the constancy of P = {x∈U | C(x)} when U varies, needs not imply the above weak version, as there can exist some universe U (among the smallest of this multiverse) such that P ∉ U. This means P is arising to existence with U, and will anyway exist as a set in all the "future" (larger) universes which see U as a set. So, a class C is not considered a set in this "strong" sense, if it remains able to contain «unknown» or «not yet existing» objects (in some future universe), that would only belong to some larger future value of P, which can thus vary with the growth of U.
• The middle version (implied by the strong one) is to interpret S(C) in the union U of the multiverse. Deciphered there, it says that, while U expands, «there exists a time from which P stays constant» (and thus after which it will exist as a set). So, this just differs from the strong version by ignoring any "past" variations (which could occur during some "beginning" of the expansion), to focus on the ultimate behavior (among the latest, i.e. largest universes, somehow "closest" to the U where S(C) is interpreted).

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

C(x) ⇔ ((By, y = x) ⇎ (By, 0)) ⇒ (∃y∈E, y = x ⇎ 0) ⇔ x ∈ E

• C is a set in the above "strong" sense (C ⊂ U) ;
• Moreover E is a set in the sense of first-order logic (1.D): the formula of B only has definite, fixed means (variables bound to given sets, fixed parameters) to provide its elements. ∎

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)) ∧ {x∈ F | B(x)}≈Ø,

What,(∀x ∈ F, C(x) ⇔ B(x)) ????

2.C. Concepts of truth in mathematics

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.

Arithmetic truths

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.

• FOT-sound (included in the class of realistic truths);
• Large (compared by inclusion with other such existential classes).

More concepts of strength

1. The class of its arithmetical theorems ;
2. The statement of its consistency.

• 1. cannot contain 2. (unless 2. is false), though 2. must be true if 1. is valid. This is because 1. is only made of the theorems of T with a standard proof, while 2. means to forbid the current universe from containing even a non-standard proof (with pseudo-finite length) from T that would lead to contradiction.
  
• So, 2. means the existence, in the current universe, of some model of T but with no requirement of standardness ; while 1. means the current universe agrees with T on arithmetic, and thus can only be philosophically justified by the idea that T is valid in the sense of having a FOT-standard model.

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

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

• Sound = keeps accepting some standard universes (for FOT-soundness);
• Strong = only accepts "large" universes (truly large in the standard case, otherwise anyway looking large by the description of their hierarchy of sub-universes), to contribute to a large class of theorems.

• T + the consistency of T;
• T₀ + the existence of a standard universe of T ;
• T₀ + the existence of infinitely many standard universes of T forming a standard multiverse (actually only ensured to be quasi-standard).

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

• An axiom is open if satisfied by any open universe, i.e. where eternity is a very long time especially towards the end.

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.

Alternative logical frameworks

• Some logicians developed the «intuitionistic logic», which lets formulas keep a possible indefiniteness as we mentioned for open quantifiers, but treated as a modification of the pure Boolean logic (the rejection of the excluded middle, where ¬(¬A) does not imply A), without any special mention of quantifiers as the source of this uncertainty. Or it might be seen as a formal confusion between truth and provability. In this framework, {0}∪ ]0,1] ⊂ [0,1], without equality. I could not personally find any interest in this formalism but only heard that theoretical computer scientists found it useful.
• When studying measure theory (which mathematically defines probabilities in infinite sets), I was inspired to interpret its results as simpler statements on another concept of set, with the following intuitive property. Let x be a variable randomly taken in [0,1], by successively flipping a coin for each of its (infinity of) binary digits. Let E be the domain of x, set of all random numbers in [0,1]. It is nonempty because such random numbers can be produced. Now another similarly random number, with the same range (y ∈ E) but produced independently of x, does not have any chance to be equal to x. Thus, ∀x∈E, ∀y∈E, x ≠ y. This way, x ∈ E is no more always equivalent to ∃y∈E, x = y.