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 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 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 ∀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 second-order 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) ∧ (∀xK, C(x)) ∧ (Qx, xK).

(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 first-order version of set theory ; but I am not sure if this is can be ever used or not)
This equivalence between Q and ∀C is equivalently expressible (see proof of this latter equivalence) 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))).

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

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) xEB(x) yE, xy y∈Dom f, f(y)=x 0
x=y x=yx=z
Qx, A(x) xE, B(x)⇒A(x) yE, ∀xy, A(x) x∈Dom f, A(f(x)) 1 A(y) A(y) ∧ A(z)
Q*x,A(x) xE, B(x) ∧ A(x) yE, ∃xy, A(x) x∈Dom f, A(f(x)) 0
A(y) A(y) ∨ A(z)
K {yE | B(y)} E Im f {y} {y,z}
dK xE, dB(x) Set(E)∧∀xE, Set(x)
Fnc(f) 1

For the first of these symbols which is the set builder, the unary predicate symbol B is meant as the abbreviation of any formula which can define it with parameters, so that the axiom for it given by the set generation principle (similar to the axiom for functions) can be read as a use of second-order universal elimination over a ∀B ahead of it. We first defined in 1.8 the set-builder K={xE | B(x)} as a class, thus with an open quantifier (∀x, xK ⇔ (xEB(x))) but the above shows how to write this definition by axioms without open quantifier beyond parameters:
Set(K) ∧ (∀xK, xEB(x)) ∧ (∀xE, B(x) ⇒ xK)
or more shortly
Set(K) ∧ KE ∧ (∀xE, xKB(x))
with which the proof of Russell's paradox would be written
F, (F={xE | Set(x) ∧ xx} ∴ Set(F) ∴ (FF ⇎ (Set(F) ∧ FF))) ∴ FE

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 : EF) as
(f : EF) ⇔ (Fnc(f) ∧ Set(F) ∧ Dom f = E ∧ Im fF)
that reads «f is a function from E to F ». A set F such that ImfF (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: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 = ∅ ⇔ 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: (∃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).

A general principle for the formalization of set theory

For any kind of meta-objects indirectly expressible and usable like objects in expressions, set theory will be enriched with tools to directly present them as objects. Namely, classes behaving as sets will be convertible into sets (1.11), and indirectly specified elements will become directly specified (2.4). But when the indirect expression of meta-objects (here, functors) may run over an infinity of possible expressions (here, any term), another reason is needed to see all these meta-objects as definite objects of a single kind (functions): the reason here is that the domains of these functors are sets, given as an argument to the definer. Otherwise, there cannot be a class of all functors, nor of all classes: naively trying to insert this in the same universe might lead to contradictions by reasonings like the proof of Russell's paradox.

Meta-objects 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 (meta-objects) 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 meta-objects 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 meta-object 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, 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