1.11. Set generation principle

Bounded quantifiers give sets their fundamental role as ranges of bound variables, unknown by the predicate ∈ which only lets them play a role of classes. Technically, the bounded quantifier (∃ ∈ , ) suffices to define the predicate ∈ as
xE ⇔ (∃yE, x=y)
but is not definable from it in return in the set theoretical formalism, as the inverse definition involves an open quantifier. Philosophically, the perception of a set as a class (ability to classify each object as belonging to it or not) does not provide its full perception as a set (the perspective over all its elements as coexisting).

Set generation principle. For any class C (defined by a given bounded formula with parameters), if the formula (∀x,C(x) ⇒ A(x)) expressing C on an undefined unary predicate A (an extra symbol of predicate used ignoring the possibility to replace it by a formula, as mentioned in 1.5) is proven equivalent to a bounded formula (here abbreviated as (Qx, A(x)) like a quantifier), then C is a set that can be named by a new operator symbol K to be added to the language of set theory, with arguments the (common) parameters of C and Q, and axiom :
(For all accepted values of parameters), Set(K) ∧ (∀xK, C(x)) ∧ (Qx, xK).

This equivalence 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) For all (undefined symbols of) unary predicates A and B, (∀x, A(x) ⇒ B(x)) ⇒ ((Qx, A(x)) ⇒ (Qx, B(x))).

Indeed 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)) ∎

(3) will often be immediate, by lack of any troubling occurrence of A in Q (inside a negation, an equivalence, or left of a ⇒), leaving us to verify (1) and (2).

Here are examples of such operator symbols (the first column is the generic abbreviation while others are the effective examples, and denoting D=Dom f) :

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

The definition of the set K={xE | B(x)}, that was only expressed as a class, can also be written as the particular case of the above mentioned axiom, i.e.
Set(K) ∧ (∀xK, xEB(x)) ∧ (∀xE, B(x) ⇒ xK)
or more shortly as
Set(K) ∧ KE ∧ (∀xE, xKB(x))
with which the proof of Russell's paradox would be written
F={xE | Set(x) ∧ xx} ⇒ ((∀xE, xF ⇔ (Set(x) ∧ xx)) ∧ (FF ⇎ (Set(F) ∧ FF))) ⇒ FE

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

The set Imf of values of f(x) when x ranges over Dom f, is called the image of f.
We define the predicate f:EF as
(f:EF) ⇔ (Fnc(f) ∧ Set(F) ∧ Domf = E ∧ ImfF)
that reads «f is a function from E to F ». A set F such that ImfF (i.e. ∀xDom f, f(x) ∈ F), is called a target set of f.
The more precise (Fnc(f) ∧ Dom f=EImf = 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 E (⌀ ⊂ E).
Thus, (E=⌀ ⇔ E ⊂ ⌀ ⇔ ∀xE, 0), and thus (E ≠ ⌀; ⇔ ∃xE,1).
This constant symbol ⌀ ensures the existence of a set; for any set E we also get ⌀ = {xE | 0}.
As (Dom f=⌀ ⇔ Imf=⌀) and (Dom f=Dom g=⌀ ⇒ f=g), the only function with domain ⌀ is called the empty function.

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, y we have {x, y}={y, x}. If xy, the set {x, y} with 2 elements x and y is called a pair.

Our set theory will later be completed with more symbols and axioms, either necessary (as here) or optional (opening a diversity of possible set theories).

Set theory and Foundations of mathematics
1. First foundations of mathematics
Philosophical aspects
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
Intuitive representation and abstraction
Platonism vs Formalism
1.3. Form of theories: notions, objects, meta-objects
Realistic vs. axiomatic theories
1.4. Formalizing types and structures
1.5. Expressions and definable structures
Time in Model theory
The time of interpretation
The metaphor of the usual time
The finite time between expressions
1.6. Connectives
1.7. Classes in set theory
The infinite time between theories
Zeno's Paradox
1.8. Binders in set theory Time in Set theory
Expansion of the set theoretical universe
Can a set contain itself ?
1.9. Quantifiers
The relative sense of open quantifiers
Interpretation of classes
Classes in an expanding universe
Concrete examples
1.10. Formalization of set theory
1.11. Set generation principle
Justifying the set generation principle
Concepts of truth in mathematics
Alternative logical frameworks
2. Set theory (continued)
Other languages:
FR : 1.11. Principe de génération des ensembles