2. Théorie des ensembles

2.1. Premiers axiomes de théorie des ensembles

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.

Les axiomes (parfois avec d'autres composants primitifs) peuvent être classés ainsi suivant leurs rôles, ordonnés des composants les plus "primitifs" (nécessaires) aux plus optionnels et discutables (ouvrant une diversité de théories des ensembles acceptables).

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 (Ext(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:

(∃xE, A(x)) → (∃x, xEA(x))
(∀xE, A(x)) → (∀x, xEA(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 pour définir des prédicats. Les quantificateurs ouverts ne seront autorisés que dans les énoncés (déclarés vrais comme axiomes ou théorèmes): chaque énoncé sera constitué d'une chaîne de quantificateurs ouverts, généralement tous ∀ et souvent écrits en mots ("pour tous"), avant une formule bornée. Les preuves utiliseront naturellement les règles de déduction pour les quantificateurs ouverts (introduction et élimination) sous forme verbable.

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(Ext(x)) : tout (Ext(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 (Ext(x))). Ainsi pour chaque terme définissant t on a un axiome où ∀(t,E) est remplacé par

∀paramètres, ∀SetE, (∀xE, dt(x, paramètres)) ⇒

Le prédicat d'inclusion

Le prédicat binaire ⊂ d'inclusion entre ensembles se définit par : pour tous ensembles E et F,

EF ⇔ (∀xE, xF)

et se lit: E est inclus dans F, ou E est une partie (ou un sous-ensemble) de F, ou F englobe E. Les propriétés de l'inclusion entre classes s'appliquent.
EE est logiquement valide. Les chaines d'implications se traduisent en chaines d'inclusions:
(EFG) ⇔ (EFFG) ⇒ EG.

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,

EFEE = F.

En effet, EFE signifie que E et F ont les mêmes éléments (∀x, xExF), et pour tout prédicat R,

(∀xF, R(x)) ⇔ (∀xE, 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:
  1. ∀(t,E), ∀Fnc f, f = (Ext(x)) ⇔ (Dom f = E ∧ ∀xE, f(x) = t(x))
  2. ∀(t,E), Dom(Ext(x)) = E ∧ ∀xE, (Eyt(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 ∧ ∀xE, f(x) = t(x)) par [f : E, t], les énoncés ci-dessus se réécrivent
  1. ∀(t,E), ∀Fnc f, f = (Ext(x)) ⇔ [f : E, t]
  2. ∀(t,E), [Ext(x) : E, t]
1. ⇔ (2. ∧ 1b.) où

1b. ∀(t,E), ∀Fnc f, [f : E, t] ⇒ f = (Ext(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 = (Exg(x))
[g : E, g] ∴ g = (Exg(x))
Fnc f, [f : E, g] ⇒ f = g
Preuve de (2.∧(=Fnc)) ⇒ 1b.
∀(t,E), ∀Fnc f, ([f : E, t] ∧ [Ext(x) : E, t]) ⇒ f = (Ext(x)). ∎
Note: on réécrire (Fc) ∧ 1. comme

1'. ∀(t,E), ∀f, f = (Ext(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀xE, f(x) = t(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.1. First axioms of set theory