1.8. Symboles liants en théorie des ensembles

Syntaxe des symboles liants

Cette dernière sorte de symbole peut former une expression en prenant un symbole de variable, disons ici x, et une expression F pouvant utiliser x comme variable libre (en plus des variables libres disponibles à l’extérieur), pour donner une valeur dépendant de la structure unaire définie par F d'argument x. Ainsi, il sépare la sous-expression «intérieure» F ayant x parmi ses variables libres, de l'«extérieur» où x est liée. Mais dans la plupart des cas (la plupart des théories...), les symboles liants ne peuvent pas conserver la donnée complète de cette structure unaire, trop complexe pour être enregistrée comme objet, comme expliqué ci-dessous.

Nous présenterons d’abord les deux principaux symboles liants en théorie des ensembles: le symbole de compréhension et le définisseur de fonctions. Puis, 1.9 présentera les deux principaux quantificateurs. Enfin 1.10 et 1.11 donnera des axiomes complétant cette formalisation des notions d’ensemble et de fonction en théorie des ensembles.

La syntaxe diffère entre la logique du premier ordre et la théorie des ensembles, qui gèrent le domaine des variables différemment. En logique du premier ordre, les domaines sont des types, données implicites des quantificateurs. Mais les domaines des symboles liants en théorie des ensembles sont des ensembles qui, comme objets, sont désignés par un argument supplémentaire du symbole (un espace pour un terme n'utilisant pas la variable à lier).

Symbole de compréhension

Pour tout prédicat unaire A admissible dans un ensemble E, la sous-classe de E définie par A est un ensemble: c'est le domaine d'une variable x introduite comme parcourant E, donc liable, dont on sélectionne les valeurs satisfaisant A(x). C'est donc un sous-ensemble ou une partie de E, noté {x∈E | A(x)} (ensemble des x dans E tels que A(x)): pour tout y,

y ∈ {x ∈ E|A(x)} ⇔ (y ∈ E ∧ A(y))

Cette combinaison de caractères { ∈  |  } forme la notation d'un symbole liant appelé symbole de compréhension : {x∈E | A(x)} lie x de domaine E sur la formule A.

Paradoxe de Russell

Si l'univers (classe de tous les éléments) était un ensemble alors en l'utilisant, le symbole de compréhension pourrait convertir en ensembles toutes les classes, dont la classe de tous les ensembles. Mais c'est impossible, comme on peut montrer à l'aide du symbole de compréhension lui-même :

Théorème. Pour tout ensemble E il existe un ensemble F tel que F ∉ E. Ainsi aucun ensemble E ne peut contenir tous les ensembles.

Preuve. F = {x∈E | Set(x) ∧ x ∉ x} ⇒ (F ∈ F ⇔ (F ∈ E ∧ F ∉ F)) ⇒ (F ∉ F ∧ F ∉ E). ∎

Cela nous obligera à préserver les distinctions entre ensembles et classes.

Définitions des fonctions par des termes

Le définisseur de fonction (  ∋   ↦  ) lie une variable sur un terme, suivant la syntaxe (E ∋ x ↦ t(x)) où Admissible si t(x) est admissible pour tout x dans E, il prend alors le foncteur défini par t et restreint son domaine (classe d'admissibilité) à E, pour donner une fonction de domaine E.
Il convertit donc les foncteurs en fonctions, à l'inverse du rôle de l'évaluateur de fonction (avec le foncteur Dom) qui convertissait (interprétait) les fonctions en leur rôle (signification) comme foncteurs dont les classes d'admissibilité étaient des ensembles.
La notation abrégée x ↦ t(x) peut être utilisée lorsque E est déterminé par le contexte, ou dans une méta-description pour désigner un foncteur en spécifiant l'argument x du terme qui le définit.

Relations

Une relation est un objet de la théorie des ensembles semblable à une opération mais à valeurs booléennes: il joue un rôle de prédicat dont les classes d'admissibilité (domaines des arguments) sont des ensembles (les prédicats peuvent ainsi se décrire comme relations entre types interprétés).

Les relations unaires (fonctions à valeurs booléennes), seront représentées par des sous-ensembles S de leur domaine E, en utilisant le symbole de compréhension comme définisseur, et ∈ comme évaluateur interprétant S comme prédicat x ↦ (x ∈ S). Ce rôle de S diffère encore de la relation unaire voulue, ignorant son domaine E, mais étant admissible dans tout l'univers, valant 0 hors de E. Cette absence d'opérateur Dom n'a pas d'importance, E étant généralement connu par le contexte (comme variable disponible).

Comme le définisseur de fonction (resp. le symbole de compréhension) enregistre toute la structure définie par l'expression donnée sur l'ensemble donné, il suffit à définir tout autre symbole liant ensembliste de même domaine sur la même expression, comme composé d'une structure unaire appliquée à son résultat (qui est une fonction, resp. un ensemble).
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 et 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
 ⇨1.9. Axiomes et preuves
1.10. Quantificateurs
1.11. Quantificateurs du 2e ordre
Aspects philosophiques
1.A. Temps en théorie des modèles
1.B. Indéfinissabilité de la vérité
1.C. Théorèmes d'incomplétude
1.D. Le cadre ensembliste unifié
2. Théorie des ensembles - 3. Algèbre

Other languages:
EN : 1. First foundations of mathematics : 1.8. Bound variables in set theory