2.5. L'ensemble des parties

Etendons la théorie des ensembles par 3 nouveaux symbols (ensemble des parties, puissance, produit) avec des axiomes, déclarant certaines classes C comme ensembles K. Ces extensions ressemblent à celles fournies par le principe de génération des ensembles (1.11), mais ne satisfont plus sa condition.
Dans le formalisme traditionnel ZF de la théorie des ensembles n'acceptant que ∈ comme stucture primitive, une telle déclaration se fait uniquement par l'axiome (ou théorème) (∀ paramètres), ∃K, ∀x, xK ⇔ C(x). Puis, le symbole d'opérateur K prenant les paramètres de C comme arguments, represente les abréviations suivantes: ∀xK signifie ∀x, C(x)⇒ ; l'égalité X=K signifie (∀x, xX ⇔ C(x)), et tout autre A(K) signifie ∃X, (X=K)∧A(X). Mais ces formules utilisent des quantificateurs ouverts, interdits dans notre cadre.
Pour ce que le principe de génération des ensembles justifiait, ∀C était remplaçable par des formules, et le ∃X ci-dessus était traitable par élimination existentielle (1.9). Mais sinon sans quantificateurs ouverts, même un ensemble donné K identique à une classe C, ne serait pas identifiable comme telle, de sorte que l'énoncé même que C coïncide avec un ensemble reste pratiquement vide de sens.
Donc, notre cadre ensembliste nécessite de regarder le symbole d'opérateur K comme primitif dans le langage (au lieu d'une abréviation définie), d'argument l'uplet y de paramètres de C, et l'axiome
(∀y…), Set(K(y))∧(∀x, xK(y) ⇔ Cy(x))

Ensemble des parties. Set E, Set(℘(E)) ∧ (∀F, F∈℘(E) ⇔ (Set(F) ∧ FE)).
On abrégera aussi ∈ ℘ par ⊂ dans les symboles liants: (∀AE,…) ⇔ (∀A∈℘(E),…).

Puissance. Set E,F, Set(FE)∧(∀f, fFE ⇔ f : EF).

Produit d'une famille d'ensembles. Ce symbole liant généralise les operateurs de produit fini (2.3):

x, x
iI
Ei ⇔ (Fnc(x) ∧ Dom x = I ∧ ∀iI, xiEi).
Pour tout iI, la i-ième projection est la fonction πi de ∏jI Ej dans Ei qui évalue toute famille x en i : πi(x)=xi. C'est l'évaluateur de fonction vu comme curryfié dans l'ordre inhabituel. Ces trois opérateurs sont «équivalents» au sens de définissables les uns par les autres:

℘(E)={f(1) | fV2E}
FE= ∏xE F={(ϵ R(x))xE | RE×F ∧∀xE, ∃!: R(x)}
  {x(
iI
 Ei)I|∀iI, xiEi} = {(ϵ R(i))iI | R
iI
Ei ∧∀xE, ∃!: R(x)}
Même certains cas sont exprimables au moyen des outils précédents:

F{a}= {{a}∋xy | yF}
 F= {∅}
℘({a}) = {∅,{a}}
   ∏
iIJ
Ei={(iI ? xi : yi)iIJ | (x,y) ∈
iI
Ei×
iJ
Ei}
(∃iI, Ei=∅) ⇒
iI
Ei =∅ 
(∀iI, ∃!:Ei) ⇒
iI
Ei = {(ϵEi)iI}

If FF′ then ℘(F) ⊂ ℘(F′), FEFE, et (∀iI, EiEi) ⇒ ∏iI Ei ⊂ ∏iI Ei .

Théorème de Cantor. Set E, ∀Fnc f, Dom f = E ⇒ ℘(E) ⊄ Im f.
Proof: F = {xE| xf(x)} ⇒ (∀xE, xFxf(x)) ⇒ (∀xE, Ff(x)) ⇒ FIm f.∎
(Le paradoxe de Russell peut se voir comme un cas particulier).



Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles (suite)
2.1. Uplets, familles
2.2. Opérateurs booléens sur les ensembles
2.3. Produits, graphes et composition
2.4. Quantificateurs d'unicité, graphes fonctionnels
2.5. L'ensemble des parties
2.6. Injectivité et inversion
2.7. Relations binaires, ensembles ordonnés
2.8. Bijections canoniques
2.9. Relations d'équivalence et partitions
2.10. Axiome du choix
2.11. Correspondance de Galois
3. Théorie des modèles