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)
∧ (∀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) 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=y
⇒ A(x)) ∴ ((3) ⇒ Q*x,A(x))
∎
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  {y ∈ EB(y)}  ⋃E  Im f  ∅  {y}  {y,z} 
dK  ∀x∈E, dB(x)  Set(E) ∧ ∀x∈E, Set(x) 
Fnc(f)  1 
1 
1 
C(x)  x∈E ∧ B(x)  ∃y∈E, x∈ y  ∃y∈D, f(y)=x  0 
x=y  x=y ∨ x=z 
Qx, A(x)  ∀x∈E, B(x) ⇒ A(x)  ∀y∈E, ∀x∈y, A(x)  ∀x∈D, 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∈D, A(f(x))  0 
A(y)  A(y) ∨ A(z) 
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. The empty set ∅ is the only set without element, and is
included in any set E (∅ ⊂ E).
Thus, (E=∅ ⇔ E ⊂ ∅ ⇔ ∀x∈E, 0), and
thus (E ≠ ∅ ⇔ ∃x∈E,1).
This constant symbol ∅ ensures the existence of a set; for any set
E we also get ∅ = {x∈E  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: (∃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.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, metaobjects 
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 classesClasses 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)

3. Model theory
