1.8. Premiers axiomes de théorie des ensembles

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. Les chaines d'implications se traduisent en chaines d'inclusion:
(EFG) ⇔ (EF et FG) ⇒ EG.
Premiers axiomes:

x,

non
( Ens
(xet  Fon
(x))

Fon x,

Ens
( Dom
x)

Ens E,F,
EFE ⇒ E=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) et implique pour tout prédicat ℛ que (∀xE, ℛ (x)) ⇔ (∀xF, ℛ (x)), et de même pour ∃.

Traduction du définisseur
Le définisseur de fonction se traduit en théorie générique par une infinité de symboles: pour chaque terme t à un argument (et des paramètres), l'expression (Ext) se traduit en bloc par un symbole d'opérateur différent, d'arguments E et les paramètres de t. (Ceux où toute sous-expression sans occurrence de x est la seule occurence d'un paramètre, suffisent à définir les autres).
Les axiomes suivants peuvent se lire comme axiomes de la théorie générique traduisant la théorie des ensembles; ceux dépendant d'un terme t sont des schémas d'axiomes (schéma d'énoncés = infinité d'énoncés obtenus par remplacement d'un symbole de structure annexe par des expressions):

Axiomes des fonctions. Pour tout terme t à un argument, toutes valeurs de ses paramètres, tout ensemble Et est valide, et toutes fonctions f et g, le premier de ces axiomes résume les 3 suivants:

f=(Ext(x)) ⇔ ( Dom
f=E et (∀xE, f(x)=t(x)))



Dom
(Ext(x))=E


xE, (Eyt(y))(x)=t(x)


( Dom
f= Dom
g et ∀x Dom
f, f(x)=g(x)) ⇒ f=g


1.7.  <—
Quantificateurs


Sommaire
>     1.9. Principe de
génération des ensembles