1.10. Formalisation de la théorie des ensembles

Le prédicat d'inclusion

Le prédicat d'inclusion ⊂ entre deux ensembles E et F, se définit par
EF ⇔ (∀xE, xF).
Il se lit: E est inclus dans F, ou E est une partie (ou un sous-ensemble) de F, ou F englobe E.
On a toujours EE (qui signifie: ∀x, xExE).
Les chaines d'implications se traduisent en chaines d'inclusions:
(EFG) ⇔ (EF ∧ FG) ⇒ EG.

Traduction du définisseur en logique du premier ordre

La traduction de la théorie des ensembles en théorie générique, convertit le définisseur de fonction en une infinité de symboles d'opérateurs: pour chaque terme t à un argument (et des paramètres), l'expression (Ext(x)) est vue en bloc comme le grand nom d'un symbole d'opérateur distinct, d'arguments E et les paramètres de t. (Ceux où toute sous-expression dans t sans occurrence de x est l'unique occurence d'un paramètre, suffiraient à définir les autres). Il en va de même pour le symbole de compréhension, ce qui viendra comme cas particulier en 1.11.
Par cette traduction, la liste des axiomes de la théorie des ensembles peut se voir comme étant la liste des axiomes de la théorie générique en laquelle elle se traduit. Tous les axiomes dépendant d'une expression (un terme pour le définisseur, ou une formule pour le symbole de compréhension) sont des schémas d'axiomes. (Un schéma d'énoncés, à savoir axiomes ou théorèmes, est une liste infinie d'énoncés, habituellement obtenus en remplaçant un symbole de structure annexe par toute expression pouvant le définir).

Premiers axiomes

x,
Fnc x,
¬(Set(x) ∧ Fnc(x))
Set(Dom x)
E, ∀(paramètres),
SetE, ∀SetF,
Fnc(Ext(x)) pour tout terme t
EFEE=F (Axiome d'Extensionnalité)
Ce dernier axiome redéfinit l'égalité entre ensembles par leur équivalence comme classes (laissant les éléments en vrac): EFE signifie que E et F ont les mêmes éléments (∀x, xE ⇔ xF) de sorte que pour tout prédicat R,

(∀xF, R(x)) ⇔ (∀xE, R(x))

et de même pour ∃.

Axiomes des fonctions. Pour tout foncteur t (à remplacer par tous les termes pouvant le définir), on a les axiomes suivants, dont le premier résume les 3 autres: pour toutes valeurs des paramètres de t, tout ensemble E inclus dans la classe d'admissibilité de t (cette condition ∀xE, dt(x) est la condition d'admissibilité de (Ext(x))), et toutes fonctions f et g,

f = (Ext(x)) ⇔ ( Dom f = E ∧ (∀xE, f(x) = t(x)))
Dom (Ext(x)) = E
xE, (Eyt(y)) (x) = t(x)
(Dom f = Dom g ∧ ∀x ∈ Dom f, f(x) = g(x)) ⇒ f = g

Un principe général en théorie des ensembles

Pour toute sorte de méta-objets indirectement exprimables et utilisables comme des objets dans les expressions, la théorie des ensembles s'enrichira d'outils les présentant directement comme objets. Ainsi, les classes utilisables comme des ensembles seront convertibles en ensembles (1.11), et les éléments indirectement spécifiés deviendront directement spécifiés (2.4). Mais quand l'expression indirecte des méta-objets (ici, foncteurs) peut parcourir une infinité d'expressions possibles (ici, tout terme), une autre raison est nécessaire pour considérer tous ces méta-objets comme des objets concrets d'un seul type (ici, des fonctions): la raison ici est que les domaines de ces foncteurs sont des ensembles, donnés comme argument au définisseur. Sinon, on ne pourrait pas admettre de classe de tous les foncteurs, ni de classe de toutes les classes: tenter naïvement de les insérer dans le même univers pourrait mener à des contradictions par des raisonnements semblables à la preuve du paradoxe de Russell.

Les méta-objets se comportant comme des objets d'une forme autre que celles d'ensembles ou de fonctions, seront représentés comme un autre type d'objets (opérations, relations, uplets), et les outils de conversion des rôles (méta-objets) en objets, seront complétés par de nouveaux outils de conversion des objets en leurs rôles. Mais cela peut être fait à l'intérieur de la même théorie des ensembles (juste en la développant), comme des objets déjà présents (ensembles ou fonctions) se trouvent pouvoir naturellement jouer les rôles de ces nouveaux objets. Ainsi, les nouvelles notions sont définissables comme classes d'objets existants (offrant leurs structures aux nouveaux objets), et les outils d'interprétation et de définition des objets (convertissant les objets en leurs rôles de méta-objets et inversement), se définissent comme abréviations de certaines expressions fixes. Dès lors, les seules foncteurs utiles de traductions entre objets jouant le même rôle de méta-objet par différentes méthodes (expressions), relieront les différents objets d'anciennes sortes représentant utilement de diverses manières le même objet de la nouvelle sorte.

Formalisation des opérations et curryfication

La notion d'opération n-aire, objets agissant comme des opérateurs n-aires entre n ensembles, se formaliserait par: La notion d'opération peut se représenter comme classe de fonctions, par le procédé suivant nommé curryfication. Le rôle du définisseur d'opérations (liant n variables) est joué par la succession de n usages du définisseur de fonction (un pour chaque variable à lier), et donc de même comme évaluateur, n usages de l'évaluateur de fonction. Par exemple (n=2), l'opération binaire f définie par le terme (prédicat binaire) t d'arguments x dans E et y dans F, peut se formaliser par

f ≈ (Ex ↦ (Fyt(x,y))) = g
f
(x,y) = g(x)(y) = t(x,y)

La fonction intermédiaire g(x) = (Fyt(x,y)) d'argument y, voit x fixe et y liée. Mais cela rompt la symétrie des rôles entre arguments, et perd la donnée de F lorsque E est vide sans que l'inverse n'ait lieu. Une formalisation sans ces défauts sera possible à l'aide des uplets (2.1.).

Les relations n-aires s'évaluent par un prédicat d'arité n+1, et se définissent par un symbole liant n variables sur une formule. On peut soit voir les relations n-aires comme cas particuliers d'opérations n-aires (en traduisant les booléens en objets), soit voir les opérations n-aires comme cas particuliers de relations (n+1)-aires (voir 2.3). Et comme pour les operations, les relations sont réductibles au cas unaire de 2 manières : par curryfication (avec n−1 usages du définisseur de fonction et 1 usage du symbole de compréhension, comme sera fait en 2.3 avec n=2), ou par les uplets (2.1).

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
1.1. Introduction au fondement des mathématiques
1.2. Variables, ensembles, fonctions et opérations
1.3. Forme des théories: notions, objets, méta-objets
1.4. Structures mathématiques
1.5. Expressions et structures définissables
1.6. Connecteurs
1.7. Classes en théorie des ensembles
1.8. Symboles liants en théorie des ensembles
1.9. Quantificateurs

1.10. Formalisation de la théorie des ensembles
1.11. Principe de génération des ensembles
Aspects philosophiques
Temps en théorie des modèles
Temps en théorie des ensembles
Interprétation des classes
Concepts de vérité en mathématiques
2. Théorie des ensembles (suite) 3. Théorie des modèles
Other languages:
EN : 1. First foundations of mathematics : 1.10. Formalization of set theory