Set generation principle. For any class C defined by a given bounded formula with parameters, if ∀_{C} is proven equivalent to another bounded formula (using a variable unary predicate symbol A) here abbreviated as the quantifier Q defined by it, in the sense that ∀A, (∀x,C(x) ⇒ A(x)) ⇔ (Qx, A(x)) is deduced by secondorder universal introduction from a given condition on parameters, then C is a set that can be named by an operator symbol K added to the language of set theory, with arguments the parameters of C and Q (which are the same), 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).
(This condition of "proven equivalent" can accept as valid a proof using an already accepted axiom schema applied to an expression using A, thus beyond the strict concept of provability in the firstorder version of set theory ; but I am not sure if this is can be ever used or not)
(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))).
A list of cases of application of this principle is given by the following table, where the first column recalls the above generic abbreviations while each other column gives an effective example of expressions on which it works. The K line gives the notations for the set theoretical symbols so introduced.
C(x)  x∈E ∧ B(x)  ∃y∈E, x∈ y  ∃y∈Dom f, 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∈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) 
K  {y∈E  B(y)}  ⋃E  Im f  ∅  {y}  {y,z} 
dK  ∀x∈E, dB(x)  Set(E)∧∀x∈E, Set(x) 
Fnc(f)  1 
1 
1 
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. 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 = ∅ ⇔ Im f = ∅) 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).
Metaobjects behaving as objects with another role beyond sets and functions, will be represented as another kind of objects (operations, relations, tuples), and the conversion tools from roles (metaobjects) to objects will be completed by new conversion tools from objects into their roles. But this can be done inside the same set theory (just by developing it), as already present objects (sets or functions) can be found to naturally play the roles of these new objects. So, the new notions can be defined as classes of existing objects (that will offer their expressible features to the new objects), while the tools of interpretation and definition of objets (converting objects into their roles of metaobjects and inversely) are defined as abbreviations of some fixed expressions. Then, the only needed functors of conversion between objects playing the role of the same metaobject by different methods (expressions), will relate the different objects of old kinds that usefully represent in different ways the same object of the new kind.
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
