Page obsolete. Nouvelle version : Formalisation de la théorie des ensembles
Le prédicat d'inclusion ⊂ entre deux ensembles E et F,
se définit par E ⊂ F ⇔ (∀x ∈ E,
x ∈ F). 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 E ⊂ E. Les chaines d'implications se
traduisent en chaines d'inclusion:
(E ⊂ F ⊂ G) ⇔ (E
⊂ FetF ⊂ G) ⇒ E
⊂ G.
Premiers axiomes:
∀x,
non
(
Ens
(x) et
Fon
(x))
∀Fonx,
Ens
(
Dom
x)
∀EnsE,F,
E ⊂ F
⊂ E ⇒ E=F
(axiomed'extensionnalité).
Ce dernier axiome redéfinit l'égalité entre ensembles par leur
équivalence comme classes (laissant les éléments en vrac): E ⊂ F
⊂ E signifie que E et F ont les mêmes éléments
(∀x, x ∈ E ⇔ x ∈ F) et
implique pour tout prédicat ℛ que (∀x ∈ E, ℛ (x)) ⇔ (∀x
∈ F, ℛ (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 (E ∋ x ⟼ t) 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 E où t
est valide, et toutes fonctions f et g, le premier de
ces axiomes résume les 3 suivants: