2.5. The powerset axiom
Let us extend set theory by 3 new symbols (powerset, exponentiation,
product) with axioms, that will declare given classes C to
be sets K. These extensions are similar to those provided by
the set generation principle (1.11), but no more satisfy its
requirement.
In the traditional ZF formalization of set theory only accepting ∈
as primitive stucture, such a declaration is done purely by the
axiom (or theorem) (∀ parameters), ∃K, ∀x, x ∈
K ⇔ C(x). Then, the operator symbol K
taking the parameters of C as its arguments, represents the
following abbreviations: ∀x∈K means ∀x, C(x)⇒
; the equality X=K means (∀x,
x ∈ X ⇔ C(x)),
and any other A(K) means
∃X, (X=K)∧A(X).
But these formulas use open quantifiers, forbidden in our framework.
For what the set generation principle justified, ∀_{C}
could be replaced by formulas, while the above ∃X could be
treated by existential elimination (1.9). But otherwise without open
quantifiers, even a given set K identical to a class C,
would not be recognizable as such, so that the very claim that C
coincides with a set remains practically meaningless.
Thus, our set theoretical framework requires the operator symbol K
to be regarded as primitive in the language (instead of a defined
abbreviation), with argument the tuple y of parameters of C,
and the axiom
(∀y…), Set(K(y))∧(∀x,
x ∈ K(y) ⇔ C_{y}(x))
Powerset. ∀_{Set} E, Set(℘(E))
∧ (∀F, F∈℘(E) ⇔ (Set(F) ∧ F
⊂ E)).
We shall also shorten ∈ ℘ into ⊂ in binders: (∀A⊂E,…) ⇔ (∀A∈℘(E),…).
Exponentiation. ∀_{Set} E,F,
Set(F^{E})∧(∀f, f ∈ F^{E} ⇔
f : E → F).
Product of a family of sets. This binder
generalizes the finite product operators (2.3):
∀x, x ∈ ∏
i∈I
E_{i} ⇔ (Fnc(x) ∧ Dom x
= I ∧ ∀i∈I, x_{i} ∈
E_{i}).
For all i ∈ I, the i-th projection is
the function π_{i} from ∏_{j∈I}
E_{j} to E_{i}
evaluating every family x at i : π_{i}(x)=x_{i}.
This is the function evaluator curried in the unnatural order.
These operators are «equivalent» in the sense that they are
definable from each other:
℘(E)={f^{•}(1) | f
∈ V_{2}^{E}}
F^{E}= ∏_{x∈E} F =
{(ϵ
⃗R(x))_{x∈E}
| R ⊂ E×F ∧∀x∈E, ∃!: ⃗R(x)}
{x ∈ (⋃
i∈I E_{i})^{I}|∀i∈I,
x_{i} ∈ E_{i}} =
{(ϵ ⃗R(i))_{i∈I}
| R ⊂ ∐
i∈I
E_{i} ∧∀x∈E, ∃!: ⃗R(x)}
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}}
If F ⊂ F′ then ℘(F) ⊂ ℘(F′), F^{E}
⊂ F′^{E}, and (∀i∈I, E_{i}
⊂ E′_{i}) ⇒ ∏_{i∈I} E_{i}
⊂ ∏_{i∈I} E′_{i} .
Cantor Theorem. ∀_{Set}
E, ∀_{Fnc} f, Dom f = E ⇒ ℘(E) ⊄ Im f.
Proof: F = {x∈E| x ∉ f(x)}
⇒ (∀x∈E, x ∈ F ⇎ x ∈ f(x))
⇒ (∀x∈E, F ≠ f(x)) ⇒ F
∉ Im f.∎
(The Russell paradox may be seen as a particular case)