2. Théorie des ensembles
2.1. Premiers axiomes de théorie des ensembles
Le prédicat d'inclusion
Le prédicat binaire ⊂ d'inclusion
entre ensembles
se définit par : pour tous ensembles E et F,
E ⊂ F ⇔
∀x∈E, x ∈ F
et se lit: "E est inclus dans F", ou "E est une
partie (ou un sous-ensemble) de F", ou "F inclut E". Les
propriétés de l'inclusion entre classes s'appliquent.
E ⊂ E est logiquement valide.
Les chaines d'implications
se traduisent en chaines d'inclusions:
(E ⊂ F ⊂ G) ⇔ (E ⊂ F
∧ F ⊂ G) ⇒ E ⊂ G.
On peut utiliser la même notation E ⊂ F comme abréviation pour l'inclusion
d'un ensemble E dans une classe F (et de même pour les autres
formules définies à partir de celle-ci):
E ⊂ F ⇔ ∀x∈E, F(x)
Formules et énoncés
La plupart des théories des ensembles (sauf
principalement FST
et certaines versions fortes) n'accepteront que les formules bornées
comme sous-formules de termes (par le symbole de compréhension, et plus tard
par l'opérateur conditionnel)
et comme définitions possibles des prédicats (que ceux-ci abrègent).
Les quantificateurs ouverts ne seront autorisés que dans les énoncés (déclarés
vrais comme axiomes ou théorèmes).
En théorie des ensembles, un énoncé
est une formule close qui peut
combiner les symboles de la logique du premier ordre avec les symboles
réguliers de la théorie des ensembles comme suit: il doit être constitué d'une
chaîne de quantificateurs ouverts, généralement tous ∀ et souvent écrits en mots
("pour tous"), suivis d'une formule bornée. Les preuves utiliseront naturellement les règles de
déduction pour les quantificateurs ouverts (introduction et élimination) sous forme verbable.
La définition ci-dessus de ⊂, déclarant formellement que le symbole de prédicat ⊂ abrège
la formule bornée (∀x∈E, x ∈ F), peut aussi être vue comme
exemple d'énoncé avec quantificateurs ouverts (∀SetE,F, ) pris
comme un axiome.
Le rôle des axiomes
Comme expliqué en 1.9, le rôle des axiomes
d'une théorie générique, est d'exprimer sa diversité de modèles voulus comme une sélection
(classe) partant d'une notion plus large
de «tous les systèmes» dont les structures sont nommées par le même langage. Le cadre
logique, qui contient (décrit) cette notion
plus large, peut interpréter les axiomes dans chacun de ces systèmes, puis exclure ceux où il
trouve que certains axiomes sont faux. Les systèmes exclus restent des modèles possibles
de différentes théories décrites par le même cadre. Tout énoncé vrai dans tous les systèmes
(énoncé logiquement valide) est inutile (redondant) comme axiome.
Mais exprimer la théorie des ensembles dans son cadre logique spécial non utilisé pour
d'autres théories, laisse a priori indéfinie la distinction entre ses énoncés logiquement
valides et ses autres vérités de base acceptées qui doivent être déclarées comme axiomes
en raison de leur fausseté dans certains "non-univers". Or cette distinction peut prendre un
sens en convertissant la théorie des ensembles en théorie générique: appelons axiomes
d'une théorie des ensembles une liste de ses "vraie" énoncés de base dont les versions
traduites en logique du premier ordre ne sont pas logiquement valides, mais forment une
liste d'axiomes rendant cette théorie générique équivalente à la version voulue de la théorie
des ensembles. De là, la prouvabilité dans une théorie des ensembles peut être
définie comme celle donnée par la logique du premier ordre avec ces axiomes.
Conversion des symboles liants
Lors de la conversion d'expressions ensemblistes en logique du premier ordre,
les seuls symboles modifiés
sont les liants, leur format d'utilisation différant entre les deux cadres. Décrivons les
règles de cette conversion.
Le définisseur de fonction (1.8)
devient une infinité de symboles d'opérateurs: pour chaque terme t à un argument
et une liste quelconque de paramètres, le terme entier (E ∋
x ↦ t(x)) est vu 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,
qui viendra comme cas particulier en 2.2.
La traduction des quantificateurs vient en exprimant
leurs domaines comme des classes:
(∃x∈E,
A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x
∈ E ⇒ A(x))
Classification des axiomes
Les axiomes des théories des ensembles (parfois avec d'autres composants primitifs)
peuvent être classifiés ainsi suivant
leurs rôles, par ordre des composants les plus "primitifs" (nécessaires) aux plus optionnels
et discutables (ouvrant une diversité de théories des ensembles acceptables).
- Les axiomes techniques donnent aux
notions et symboles primitifs leurs rôles corrects:
- Les notions d'ensembles et de fonctions, symbolisés en
1.7, sont axiomatisés ici en 2.1 : axiomes des notions, axiome d'extensionnalité,
axiomes des fonctions.
- Elément unique (2.4)
- Axiomes issus du principe de génération des ensembles (2.2);
- Axiomes renforçants, introduits
en 1.A;
- D'autres axiomes techniques optionnels viendront ensuite:
- Axiome du choix (2.10) peut être considéré comme une spécification complétant
l'axiome des parties.
- Axiome de fondation (évoqué en 2.A et exprimé en 5.3)
Axiomes des notions
La formalisation des notions primitives par des symboles de classe suivant 1.7,
doit être complétée par les axiomes suivants.
| ∀x, ¬(Set(x) ∧ Fnc(x)) |
: les ensembles ne sont pas des fonctions (même si cela n'a pas d'importance) |
| ∀Fnc f, Set(Dom f) |
: le domaine de toute fonction est un ensemble |
| (Fc) ∀(t,E), Fnc(E ∋ x ↦ t(x))
|
: tout (E ∋ x ↦ t(x)) admissible est une fonction
|
Ici et dans les axiomes ci-dessous pour les fonctions, ∀(t,E) vise à
déclarer un schéma d'axiomes par élimination universelle du second ordre sur le
foncteur variable t avec E inclus dans la classe d'admissibilité
du terme définissant t pour les valeurs données des paramètres (c'est
la condition d'admissibilité de (E ∋ x ↦ t(x))).
Ainsi pour chaque terme définissant t on a un axiome où ∀(t,E)
est remplacé par ∀paramètres, ∀SetE,
(∀x∈E, dt(x, paramètres)) ⇒
Axiome d'extensionnalité
Cet axiome rend les ensembles déterminés par leur rôle (soit comme domaines des quantificateurs,
soit comme classes qu'ils définissent par ∈), disant que deux ensembles jouant
le même rôle sont égaux: pour tous ensembles E et F,
E ⊂ F ⊂ E ⇒ E = F.
En effet, E ⊂ F ⊂ E signifie que E et F ont les
mêmes éléments (∀x, x ∈ E ⇔ x ∈ F),
et pour tout prédicat R,(∀x∈F,
R(x)) ⇔ (∀x∈E, R(x))
et de même pour ∃. De manière informelle, les éléments d'un ensemble sont donnés en vrac.
Axiomes des fonctions.
Les fonctions sont également déterminées par leur rôle, par l'axiome suivant
(=Fnc) :
∀Fnc f,g,
(Dom f = Dom g ∧ ∀x∈Dom f, f(x)
= g(x)) ⇒ f = g.
Les définisseurs de fonctions sont liés à l'évaluateur de fonctions par un axiome
qui peut s'écrire de l'une ou l'autre manière:
- ∀(t,E), ∀Fnc f, f = (E ∋
x ↦ t(x)) ⇔ (Dom f = E ∧ ∀x∈E,
f(x) = t(x))
- ∀(t,E), Dom(E ∋ x ↦ t(x)) = E
∧ ∀x∈E, (E ∋ y ↦ t(y))(x)
= t(x)
En effet (Fc) ⇒ (1.⇔(2.∧(=Fnc))).
La preuve peut être prise comme exercice (cliquer pour voir)
Admettons (Fc) pour que 2. soit admissible.
Abrégeant (Dom f = E ∧ ∀x∈E, f(x) = t(x)) par
[f : E, t], les énoncés ci-dessus se réécrivent
- ∀(t,E), ∀Fnc f, f = (E ∋
x ↦ t(x)) ⇔ [f : E, t]
- ∀(t,E), [E ∋ x ↦ t(x) : E, t]
1. ⇔ (2. ∧ 1b.) où
1b. ∀(t,E), ∀Fnc f, [f : E, t] ⇒
f = (E ∋ x ↦ t(x))
Preuve de 1b. ⇒ (=Fnc)
∀Fnc g,
appliquant 1b. à (g, E) par E = Dom g comme
∀x∈Dom g, dg(x) :
∀Fnc f, [f : E, g] ⇒
f = (E ∋ x ↦ g(x))
[g : E, g] ∴ g = (E ∋ x ↦ g(x))
∀Fnc f, [f : E, g] ⇒ f = g
Preuve de (2.∧(=Fnc)) ⇒ 1b.
∀(t,E), ∀Fnc f, ([f : E, t]
∧ [E ∋ x ↦ t(x) : E, t]) ⇒
f = (E ∋ x ↦ t(x)).
∎
Note: on réécrire (Fc) ∧ 1. comme
1'. ∀(t,E), ∀f,
f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f =
E ∧ ∀x∈E, f(x) = t(x)).
Other languages:
EN : 2.1. First axioms
of set theory