L'ensemble des parties

2.7. Produits et ensembles des parties

Produit cartésien de deux ensembles

Pour deux ensembles E et F, le produit E×F est l'ensemble des (x,y) où x∈E et 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

Pour tout graphe R,

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

Les quantificateurs sur un produit ont des versions curryfiées equivalentes:

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

Les quantificateurs (Qx,y∈E, ) peuvent s'écrire de façon equivalente (Q(x,y)∈E×E, ) tandis que la notation Qx≠y∈E peut se lire comme un quantificateur de domaine {(x,y)∈E×E | x≠y} = (E×E) \ 𝛿_E.

Produits finis, opérations et relations

Au-delà de l'opérateur binaire de produit cartésien, on a un opérateur de produit n-aire entre tout nombre n>1 d'ensembles: E₀×…×E_n−1 est l'ensemble des n-uplets (x₀,…,x_n−1) tels que ∀i∈V_n, x_i∈E_i.
Par exemple, le produit ternaire est

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

où la dernière notation abrége l'utilisation des évaluateurs pour cette représentation des triplets. On peut aussi la voir comme directement justifiée par le principe de génération des ensembles:

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

Cela justifie finalement la formalisation la plus naturelle des opérations n-aires, comme fonctions de domaine un produit de n ensembles, d'évaluateur donné en 2.3. Cela justifie notre première notation de 2.3 pour les définisseurs d'opérations, comme utilisation de la notation abrégée de 2.6 pour les symboles liants sur les graphes, extensible à toute arité.

La notion de relation n-aire sera habituellement être formalisée comme celle d'un ensemble de n-uplets, partie du produit de ses domaines. Ainsi, une relation binaire entre deux ensembles E et F sera un graphe R ⊂ E×F. La relation d'égalité sur un ensemble E se formalise ainsi par 𝛿_E, appelé la diagonale de E×E.
Pour une formalisation spécifiant les domaines E et F des arguments, on peut prendre le triplet (E,F,R).

Traduction des opérateurs en prédicats

L'usage de tout symbole de foncteur K dans une théorie générique équivaut à celle d'un symbole de prédicat binaire R avec l'axiome de fonctionnalité

∀x, ∃!y, xRy

Il joue le rôle du "graphe de K", étant définissable à partir de K par

xRy ⇔ y = K(x)

Les termes de la logique du premier ordre utilisant K ne peuvent pas être ré-exprimés en utilisant R, mais les formules le peuvent: chaque formule contenant chaque occurrence de K peut être écrite A(K(x)) où x abrège un terme et A abrège une formule comme prédicat unaire; puis remplacée de manière équivalente par

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

Il en va de même pour les autres arités: le rôle de tout opérateur n-aire peut être joué par un prédicat (n+1)-aire avec l'axiome de fonctionnalité. Cette généralisation s'explique en remplaçant l'argument par un uplet.
Cette construction ne convient pas aux opérateurs de notre théorie des ensembles, à cause de son utilisation de quantificateurs ouverts. Mais elle est applicable lorsque les domaines sont des ensembles: les opérations n-aires peuvent être représentées sous forme de graphes fonctionnels (n+1)-aires.

De nouveaux symboles primitifs

Renforçons la théorie des ensembles par 3 extensions qui déclarent d'autres sortes de classes comme ensembles : les ensembles des parties, les puissances et les produits. Ces extensions sont équivalentes, en ce sens qu'accepter l'une d'elles comme primitive suffit pour en tirer les deux autres comme développements. Elles ressemblent à celles fournies par le principe de génération des ensembles, mais n'en satisfont plus la condition; ce manque de justification a des liens profonds avec les aspects d'incomplétude des mathématiques.
Pour convenir à notre formalisation de la théorie des ensembles (contrairement à l'approche ZF introduite ci-dessous), chacune de ces extensions est faite de

Un symbole K (à savoir, deux opérateurs et un symbole liant) désignant comme ensemble la classe donnée C, d'arguments les paramètres de C ici abrégés comme une famile y parcourant la classe d'admissibilité voulue de K;
L'énoncé ∀_dKy, Set K(y) ∧ ∀x, x ∈ K(y) ⇔ C_y(x).

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

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

Produit d'une famille d'ensembles. Le symbole liant ∏ généralise les operateurs de produit fini à toute famille d'ensembles (∀i∈I, Set E_i):

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

Comme pour les uplets, l'évaluateur de fonction curryfié en sens inverse définit une famille de projections π_i (gardant implicite leur dépendance au produit donné qui est généralement fixé dans le contexte):

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

Ces symboles préservent l'inclusion comme suit

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

Leur équivalence

De chacun de ces 3 symboles, les 2 autres peuvent se définir comme suit.

∏
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}

Même certains cas sont exprimables au moyen des outils précédents:

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}

Théorème de Cantor

Ce fameux théorème est simplement exprimable ainsi:

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

Preuve pour le cas où tous les f(x) sont des ensembles (auquel le cas général est réductible):
(E = Dom f ∧ F = {x∈E| x ∉ f(x)}) ⇒ (∀x∈E, x ∈ F ⇎ x ∈ f(x)) ⇒ (∀x∈E, F ≠ f(x)) ⇒ F ∉ Im f.∎

Le paradoxe de Russell peut se voir comme le cas particulier du théorème de Cantor pour f = Id_E.

L'approche ZF

Dans le formalisme traditionnel ZF de la théorie des ensembles, chaque extension de ce style est formalisée comme consistant d'abord en un simple énoncé sans symbole spécial, gardant ∈ comme seule structure primitive:

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

À savoir, l'axiome de l'ensemble des parties s'écrit ∀E, ∃X, ∀F, F∈X ⇔ F ⊂ E; d'où les énoncés d'existence des puissances et produits viennent comme théorèmes.
Puis, les usages de chaque symbole K d'argument y comme précédemment, désignant ces ensembles, peuvent se justifier comme développées de là comme abréviations par les règles suivantes.

∀x∈K signifie ∀x, C(x)⇒ ;
l'égalité X=K signifie (∀x, x ∈ X ⇔ C(x)), ou de manière equivalente (∀x∈X, C(x)) ∧ (∀_Cx, x ∈ X);
Toute autre formule utilisant K laissant y libre, s'écrivant A(K), signifie la formule ainsi abrégée comme ∃X, (X=K)∧A(X).
Pour pouvoir lier y sur des termes utilisant K, on doit utiliser le schéma d'axiomes de remplacement.

Mais même le premier cas n'est pas permis dans notre cadre, car il utilise un quantificateur ouvert, non remplaçable par une formule bornée car ces extensions ne satisfont pas la condition du principe de génération d'ensembles.
Faute de pouvoir interpréter la formule d'égalité X=K, même un ensemble donné identique à une classe C ne serait pas identifiable comme tel. D'où le besoin d'accepter les symboles K comme primitifs, pour donner un sens effectif à l'énoncé que C coïncide avec un ensemble.

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles
2.1. Premiers axiomes de théorie des ensembles 2.2. Principe de génération des ensembles 2.3. Curryfication et uplets 2.4. Quantificateurs d'unicité 2.5. Familles, opérateurs booléens sur les ensembles 2.6. Graphes ⇦ 2.7. Produits et ensembles des parties	⇨ 2.8. Injections, bijections 2.9. Propriétés des relations binaires 2.10. Axiome du choix
	Temps en théorie des ensembles Interprétation des classes Concepts de vérité en mathématiques
3. Algebra - 4. Arithmetic - 5. Second-order foundations

Other languages:
EN : 2.7. Products and powerset