2.2. 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 suffice to provide its full perception as a set, that is the perspective over all its elements as coexisting. The above formula can be seen as confirming this view of a set as a coexistence of its elements, by describing the property of belonging to a set as a form of existence with respect to this set. Thus, Russell's paradox can be read as saying that mathematical objects cannot all coexist as a completed totality. The explanation of 1.7 that no set theoretical universe can be the ultimate one is just another aspect of this, as will be further commented in philosophical pages.

Set generation principle. For any class C defined by a bounded formula, if ∀C is found equivalent to the quantifier Q defined by another bounded formula (whose free variables are the parameters of C and a variable unary predicate symbol A), by formally proving by second-order universal introduction (under a given condition on parameters) that

A, (∀x,C(x) ⇒ A(x)) ⇔ (Qx, A(x))

then C is a set that can be named by an 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) ∧ (∀xK, C(x)) ∧ (Qx, xK).

(The involved second-order universal introduction can accept 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 ; I am not sure if this is 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) ∀A, ∀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. For 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 remaining non-trivial (but very easy) condition to check.

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.

dK xE, dB(x) Set(E)∧∀xE, Set(x)
Fnc(f) 1
1
1
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}

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}.
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.
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:

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

Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. Formalization of set theory
2.2. Set generation principle
⇨ 2.3. Tuples, families
2.4. Boolean operators on sets
2.5. Products, graphs and composition
2.6. Uniqueness quantifiers, functional graphs
2.7. The powerset
2.8. Injectivity and inversion
2.9. Binary relations ; order
2.10. Canonical bijections
2.11. Equivalence relations, partitions
2.12. Axiom of choice
2.13. Galois connection
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 1.11. Principe de génération des ensembles