The powerset axiom

2.7. Products and powerset

Cartesian product of two sets

For any two sets E and F, the (cartesian) product E×F is the set of (x,y) where x∈E and y∈F.

E×F = ∐_x∈E F

∐
i∈IE_i = ⋃
i∈I {i}×E_i ⊂ I×⋃
i∈I

E_i
(E⊂E′ ∧ F⊂F′) ⇒ E×F ⊂ E′×F′
E×∅ = ∅ = ∅×E

For any graph R,

R ⊂ E×F ⇔ (Dom R ⊂ E ∧ Im R ⊂ F)
R_|E = R∩(E× Im R)

Quantifiers over a product have equivalent curried views:

(∃(x,y)∈E×F, A(x,y)) ⇔ (∃x∈E, ∃y∈F, A(x,y)) ⇔ (∃y∈F, ∃x∈E, A(x,y))
(∀(x,y)∈E×F, A(x,y)) ⇔ (∀x∈E, ∀y∈F, A(x,y)) ⇔ (∀y∈F, ∀x∈E, A(x,y))
(∃x∈E, A(x)∨B(x)) ⇔ ((∃x∈E, A(x)) ∨ (∃x∈E, B(x)))
(∀x∈E, A(x)∧B(x)) ⇔ ((∀x∈E, A(x)) ∧ (∀x∈E, B(x)))
(∃x∈E, C∨A(x)) ⇔ ((C ∧ E≠∅) ∨ ∃x∈E, A(x))
(∀x∈E, C∧A(x)) ⇔ ((C ∨ E=∅) ∧ ∀x∈E, A(x))

Quantifiers (Qx,y∈E, ) can be equivalently written (Q(x,y)∈E×E, ) while the notation Qx≠y∈E can be read as one quantifier with domain {(x,y)∈E×E | x≠y} = (E×E) \ 𝛿_E.

Finite products, operations and relations

Beyond the binary operator of cartesian product, there is an n-ary product operator between any number n>1 of sets : E₀×…×E_n−1 is the set of all n-tuples (x₀,…,x_n−1) such that ∀i∈V_n, x_i∈E_i.
For example, the ternary product is

E×F×G = ⋃_x∈E⋃_y∈F {(x,y,z) | z∈G} = {(x,y,z) | ((x,y),z))∈(E×F)×G}

where the latter notation abbreviates the use of the evaluators for this representation of triples. It can also be seen as directly justified by the set generation principle:

(∀(x,y,z)∈E×F×G, A(x,y,z)) ⇔ (∀x∈E, ∀y∈F, ∀z∈G, A(x,y,z))

This finally justifies the most natural formalization of n-ary operations, as functions with domain a product of n sets, with evaluator given in 2.3. It justifies our first notation of 2.3 for operation definers, as a use of the abbreviated notation of 2.6 for binders on graphs, extensible to any arity.

The notion of n-ary relation R will usually be formalized as that of a set of n-tuples, subset of the product of its domains. This way, a binary relation between sets E and F will be a graph R ⊂ E×F. The equality relation on a set E is so formalized as 𝛿_E, called the diagonal of E×E.
For a formalization which specifies the domains E and F of arguments, we can take the triple (E,F,R).

Translating operators into predicates

The use of any functor symbol K in a generic theory is equivalent to that of a binary predicate symbol R with the functionality axiom

∀x, ∃!y, xRy

It is meant as the "graph of K", i.e. defined from K by

xRy ⇔ y = K(x)

Terms of first-order logic using K cannot be re-expressed using R, but formulas can: each formula with each occurrence of K in it, can be written A(K(x)) where x abbreviates a term and A abbreviates a formula as a unary predicate; then equivalently replaced by either of

∃y, xRy ∧ A(y)
∀y, xRy ⇒ A(y)

The same goes for other arities : the role of any n-ary operator can be played by an (n+1)-ary predicate with the functionality axiom. This generalization can be explained as replacing the argument by a tuple.
This construction does not fit for the operators of our set theory, due to its use of open quantifiers. Yet it works when domains are sets: n-ary operations can be represented as functional (n+1)-ary graphs.

More primitive symbols

Let us strengthen set theory by 3 extensions that declare more kinds of classes to be sets : powersets, exponentiations and products. These extensions are equivalent, in the sense that accepting anyone of them as primitive suffices to get both others as developments from it. They are similar to those provided by the set generation principle, but no more fit its condition ; this lack of justification has deep connections with incompleteness aspects of mathematics.
To fit our way of formalizing set theory (unlike the ZF way introduced below), each such extension is made of

A symbol K (namely, two operators and one binder) naming as a set the given class C, with arguments the parameters of C here abbreviated as a family y ranging over the intended definiteness class of K;
The statement ∀_dKy, Set K(y) ∧ ∀x, x ∈ K(y) ⇔ C_y(x).

Powerset. ∀_Set E, Set ℘(E) ∧ ∀F, F∈℘(E) ⇔ (Set F ∧ F ⊂ E)
We shall abbreviate ∈℘ as ⊂ also in binders: for example (∀F⊂E,…) ⇔ (∀F∈℘(E),…).

Exponentiation. ∀_Set E,F, Set F^E ∧ ∀f, f ∈ F^E ⇔ f : E → F

Product of a family of sets. The binder ∏ generalizes the finite product operators to any family of sets (∀i∈I, Set E_i):

∀x, x ∈ ∏
i∈I E_i ⇔ (Fnc(x) ∧ Dom x = I ∧ ∀i∈I, x_i ∈ E_i).

Like with tuples, the function evaluator curried in the reverse way defines a family of projections π_i (keeping implicit their dependence on the given product which is usually fixed in context):

∀i∈I, π_i : ∏_j∈I E_j → E_i.

These symbols preserve inclusion as follows

F ⊂ E ⇒ ℘(F) ⊂ ℘(E)
F ⊂ E ⇒ F^G ⊂ E^G
(∀i∈I, F_i ⊂ E_i) ⇒ ∏_i∈I F_i ⊂ ∏_i∈I E_i

Their equivalence

From any of these 3 symbols, both others can be defined as follows.

∏
i∈I E_i = {x∈ (⋃
i∈I E_i)^I | ∀i∈I, x_i ∈ E_i} = {℩R⃗ | R ⊂ ∐
i∈I E_i ∧ ∀i∈I, ∃!: R⃗(i)}

F^E = ∏_x∈E F = {℩R⃗ | R ⊂ E×F ∧ ∀x∈E, ∃!: R⃗(x)}
℘(E) = {f_•(1) | f ∈ V₂^E}

Even some cases are expressible from previous tools:

F^{a}= {{a}∋x↦y | y ∈ F}
F^∅ = ∏∅_↦ = {∅_↦}
℘({a}) = {∅,{a}}
∏
i∈I∪J E_i = {(i∈I ? x_i : y_i)_i∈I∪J | (x,y) ∈ ∏
i∈IE_i × ∏
i∈JE_i}
(∃i∈I, E_i = ∅) ⇒ ∏
i∈IE_i = ∅
(∀i∈I, ∃!:E_i) ⇒ ∏
i∈IE_i = {(℩E_i)_i∈I}

Cantor's Theorem

This famous theorem is simply expressible as

∀_Fnc f, ℘(Dom f) ⊄ Im f.

Proof for the case when all f(x) are sets (to which the general case is reducible):
(E = Dom f ∧ F = {x∈E| x ∉ f(x)}) ⇒ (∀x∈E, x ∈ F ⇎ x ∈ f(x)) ⇒ (∀x∈E, F ≠ f(x)) ⇒ F ∉ Im f.∎

Russell's paradox may be seen as the particular case of Cantor's theorem for f = Id_E.

The ZF approach

In the traditional ZF formalism for set theory, each such extension is formalized as first made of a mere statement without any special symbol, keeping ∈ as the only primitive structure:

∀_...y, ∃X, ∀x, x ∈ X ⇔ C_y(x).

Namely, the powerset axiom (existence of the powerset) is written ∀E, ∃X, ∀F, F∈X ⇔ F ⊂ E, from which the statements of existence of exponentiations and products come as theorems.
Then, the uses of each symbol K with argument y as above, naming these sets, can be justified as developed from there as abbreviations by the following rules.

∀x∈K means ∀x, C(x)⇒ ;
The equality (X=K) means (∀x, x ∈ X ⇔ C(x)) or equivalently (∀x∈X, C(x)) ∧ (∀_Cx, x ∈ X);
Any other formulas using K with y free, written as A(K), mean the formula so abbreviated as ∃X, (X=K)∧A(X).
To justify binding y on terms using K, involves the axiom schema of replacement.

But our framework does not even allow the first of these cases, because it involves an open quantifier, which cannot be replaced by a bounded formula because these extensions do not fit the condition of the set generation principle.
This impossibility to interpret the equality formula (X=K) means that even a given set identical to a class C, would not be recognizable as such. Hence the need to accept the symbols K as primitive, for giving effective sense to the statement that C coincides with a set.

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 2.4. Uniqueness quantifiers 2.5. Families, Boolean operators on sets 2.6. Graphs ⇦ 2.7. Products and powerset	⇨ 2.8. Injections, bijections 2.9. Properties of binary relations 2.10. Axiom of choice
	Time in set theory Interpretation of classes Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations

Other languages:
FR : 2.7. Produits et ensembles des parties