2.2. Principe de génération des ensembles

Formaliser diverses notions en théorie des ensembles

La théorie des ensembles s'enrichira de composants supplémentaires pour représenter diverses sortes de méta-objets (rôles joués par des systèmes de symboles) directement comme objets (qui peuvent les jouer). Cela n'est applicable qu'aux méta-objets assez "concrets" en un sens à clarifier: suivant 1.8 et 1.D, toutes les classes ne peuvent pas être des ensembles, alors que seuls les foncteurs dont les domaines sont des ensembles sont représentés par des fonctions.
Certaines de ces extensions consisteront en symboles primitifs de "définisseurs" (avec les axiomes pertinents) servant à convertir en une sorte existante d'objets des méta-objets (rôles) de la même sorte : D'autres sortes de méta-objets au-delà des rôles normaux des éléments, ensembles et fonctions, formeront de nouvelles notions: celles d'opération, de relation et d'uplet seront formalisées en 2.3. Les nouveaux symboles requis sont à la fois des définisseurs (convertissant des méta-objets en les nouveaux objets) et des évaluateurs (interprétant ces objets en leurs rôles de méta-objets).
Mais, comme pour les relations unaires (1.8), ces nouvelles notions n'ont pas besoin d'être primitives, car elles peuvent être naturellement représentées par des classes d'objets existants (ensembles ou fonctions), qui peuvent offrir leurs outils (aspects exprimables) aux nouveaux objets. Ainsi, ces extensions de la théorie des ensembles peuvent s'obtenir en donnant des définitions de leurs symboles définisseurs et évaluateurs. Si une nouvelle notion peut être représentée de plusieurs façons utiles par des classes d'anciens objets, qui ne représentent pas chaque nouvel objet par le même ancien objet, alors des foncteurs serviront de traductions entre les classes jouant ainsi différemment ce rôle (2.5, 2.8).

Les ensembles comme domaines de quantificateurs bornés

Les quantificateurs bornés donnent aux ensembles leur rôle fondamental de domaines des variables liées, inconnu du prédicat ∈ qui ne leur donne qu'un rôle de classes. Techniquement, le quantificateur borné (∃ ∈ , ) suffit à définir le prédicat ∈ par

xE ⇔ (∃yE, x=y)

mais n'est pas généralement définissable par lui en retour suivant une formule bornée, sa définition utilisant un quantificateur ouvert. Philosophiquement, la perception d'un ensemble comme classe (capacité à classer chaque objet comme lui appartenant ou non) ne suffit pas à fournir sa pleine perception comme ensemble, à savoir la perspective sur tous ses éléments comme coexistants. Cette vision intuitive d'un ensemble comme coexistence de ses éléments peut être vue comme confirmée par la définition ci-dessus de l'appartenance comme une forme d'existence relative à cet ensemble. Ainsi, le paradoxe de Russell signifie que les objets mathématiques ne peuvent pas tous coexister en une ultime totalité.

Enoncé du principe

Pour toute donnée d'une classe C et d'un quantificateur Q définis par des formules bornées données avec les mêmes paramètres, si l'équivalence entre Q et ∀C, à savoir

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

est prouvé par introduction universelle de second ordre (*) sous une condition donnée sur les paramètres, alors C est un ensemble désignable par un nouveau symbole d'opérateur K ajouté au langage de la théorie des ensembles, avec ces paramètres comme arguments; et l'axiome suivant qui exprime K = C par double inclusion: Pour toutes valeurs des paramètres satisfaisant la condition,

Set(K) ∧ (∀xK, C(x)) ∧ (Qx, xK).

(*) On se contentera des cas dont les preuves n'utilisent aucun axiome obtenu à partir d'un axiome de second ordre en utilisant A dans la définition de sa structure variable, bien que je doute qu'une telle utilisation soit possible.
Ce principe sera justifié en 2.B.
La condition d'équivalence entre Q et ∀C est traduisible en la liste suivante de 3 énoncés, où le quantificateur Q* défini par (Q*x, A(x)) ⇎ (QxA(x)) sera équivalent à ∃C:

(1) ∀x, (C(x) ⇔ Q*y, x=y) (il suffit en fait que ∀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))).

Preuve d'équivalence (cliquer pour voir) Ces 3 propriétés sont déjà des conséquences connues de «Q = ∀C ». Réciproquement,
((2) ∧ (3)) ⇒ ((∀C x, A(x)) ⇒ Qx,A(x))
((1) ∧ ∃C x, A(x)) ⇒ ∃y, (Q*x, x=y) ∧ (∀x, x=yA(x)) ∴ ((3) ⇒ Q*x,A(x)) ∎

Principaux exemples

Les premiers et principaux cas d'utilisation de ce principe sont présentés dans le tableau suivant. Pour les justifier, (1) vient en trouvant que C est la formule ainsi définie à partir de Q, tandis que (3) est assuré par l'absence d'occurrence "négative" de A dans Q (dans une négation, une équivalence, ou à gauche d'un ⇒). Cela laisse (2) comme condition restante facile à vérifier.
La première colonne rappelle les abréviations génériques ci-dessus; les autres sont les exemples. La ligne K donne les notations des symboles ensemblistes ainsi introduits.

K {yE | B(y)} E Im f {y} {y,z}
C(x) xEB(x) yE, xy y∈Dom f, f(y)=x 0
x=y x=yx=z
dK xE, dB(x) Set(E)∧∀yE, Set(y)
Fnc(f) 1
1
1
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)

La valeur du symbole de compréhension K={xE|B(x)}, d'abord définie en 1.8 comme classe, donc avec un quantificateur ouvert (∀x, xK(xEB(x))), est maintenant redéfinie par des axiomes sans quantificateur ouvert au-delà des paramètres:

Set(K) ∧ (∀xK, xEB(x)) ∧ (∀xE, B(x) ⇒ xK)

ou plus simplement Set(K) ∧ KE ∧ (∀xE, xKB(x)). Comme les axiomes pour les fonctions, c'est un schéma d'axiomes par élimination universelle de second ordre sur ∀B, donc avec tous les prédicats unaires B définis par des formules bornées avec paramètres. Ainsi la preuve du paradoxe de Russell s'écrirait
F, (F={xE | Set(x) ∧ xx} ∴ Set(F) ∴ (FF ⇎ (Set(F) ∧ FF))) ∴ FE

Le foncteur ⋃ est le symbole d'union, et ses axiomes constituent l'axiome de la réunion.

L'ensemble Im f des valeurs de f(x) lorsque x parcourt Dom f, est appelé l'image de f.
On définit le prédicat (f : EF) qui se lit «f est une fonction de E dans F» (ou : vers F), E et F étant des ensembles (condition d'admissibilité qu'on peut aussi intégrer à cette définition) par

(f : EF) ⇔ (Fnc(f) ∧ Dom f = E ∧ Im fF)

Un ensemble F tel que Im fF (autrement dit ∀x ∈ Dom f, f(x) ∈ F) est un ensemble d'arrivée de f.
Le cas plus précis (Fnc(f) ∧ Dom f=EImf = F) se notera f:EF (f est une surjection ou fonction surjective de E sur F).

L'ensemble vide ∅ est le seul ensemble sans élément, et est inclus dans tout ensemble (∀SetE, ∅ ⊂ E).
Donc (E=∅ ⇔ E ⊂ ∅ ⇔ ∀xE, 0), et donc (E ≠ ∅ ⇔ ∃xE,1).
La présence du symbole de constante ∅ garantit l'existence d'un ensemble; il s'obtient aussi de tout ensemble E par ∅ = {xE | 0}. On a ⋃∅ =∅.
Comme (Dom f = ∅ ⇔ Im f = ∅) et (Dom f = Dom g = ∅ ⇒ f = g), l'unique fonction de domaine ∅ est appellée la fonction vide.
Le fait qu'une variable puisse être de domaine vide n'empêche pas de la fixer. En particulier, développer une théorie incohérente signifie étudier un système fixe dont le domaine des possibilités est vide. On peut avoir besoin de le faire pour y découvrir une contradiction, autrement dit prouver qu'aucun tel système n'existe.

On pourrait redéfinir ∃ de deux manières:

(∃xE, A(x)) ⇔ {xE | A(x)} ≠ ∅ ⇔ (1 ∈ Im(ExA(x))).

Pour tout x, {x,x}={x}. Un tel ensemble, à un seul élément, est appelé un singleton.

Pour tous x et y on a {x, y}={y, x}. Si xy, l'ensemble {x, y} à deux éléments x et y est appelé une paire.

Pour tout ensemble E, la fonction identité sur E se définit par

IdE = (Exx).

Ainsi,

Dom IdE = E = Im IdE
xE, IdE(x) = x.

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.2. Set generation principle