Set generation principle

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 :

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

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

x ∈ E ⇔ (∃y∈E, 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) ∧ (∀x∈K, C(x)) ∧ (Qx, x ∈ K).

(*) 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)) ⇎ (Qx,¬A(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)) ⇒ ((∀_Cx, A(x)) ⇒ Qx,A(x))
((1) ∧ ∃_Cx, A(x)) ⇒ ∃y, (Q*x, x=y) ∧ (∀x, x=y ⇒ A(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	{y∈E \| B(y)}	⋃E	Im f	∅	{y}	{y,z}
C(x)	x∈E ∧ B(x)	∃y∈E, x∈ y	∃y∈Dom f, f(y)=x	0	x=y	x=y ∨ x=z
dK	∀x∈E, dB(x)	Set(E)∧∀y∈E, Set(y)	Fnc(f)	1	1	1
Qx, A(x)	∀x∈E, B(x)⇒A(x)	∀y∈E, ∀x∈y, A(x)	∀x∈Dom f, A(f(x))	1	A(y)	A(y) ∧ A(z)
Q*x,A(x)	∃x∈E, B(x) ∧ A(x)	∃y∈E, ∃x∈y, A(x)	∃x∈Dom f, A(f(x))	0	A(y)	A(y) ∨ A(z)

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)

or more shortly Set(K) ∧ K ⊂ E ∧ (∀x∈E, x ∈ K ⇔ B(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={x∈E | Set(x) ∧ x∉x} ∴ Set(F) ∴ (F∈F ⇎ (Set(F) ∧ F∉F))) ∴ F ∉ E

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 : E → F) 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 : E → F) ⇔ (Fnc(f) ∧ Dom f = E ∧ Im f ⊂ F)

A set F such that Im f ⊂ F (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 : E ↠ F (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 ⊂ ∅ ⇔ ∀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.

We can redefine ∃ from the above in two ways:

(∃x∈E, A(x)) ⇔ {x∈E | A(x)} ≠ ∅ ⇔ (1 ∈ Im(E∋x ↦ A(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 x ≠ y, 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

Id_E = (E ∋ x ↦ x).

Thus,

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

Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. First axioms of set theory ⇦ 2.2. Set generation principle ⇨ 2.3. Tuples 2.4. Uniqueness quantifiers 2.5. Families, Boolean operators on sets 2.6. Graphs 2.7. Products and powerset	2.8. Injections, bijections 2.9. Properties of binary relations 2.10. Axiom of choice
	Time in set theory Interpretation of classes Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations

Other languages:
FR : 2.2. Principe de génération des ensembles