1.8. Symboles liants en théorie des ensembles

Syntaxe des symboles liants

La dernière sorte de symbole formant les expressions est celle des symboles liants.
Un tel symbole lie une (ou plusieurs) variable(s) (disons x), sur une expression F pouvant utiliser x comme variable libre en plus des variables libres présentes (avec une valeur) à l'extérieur. Il sépare donc la sous-expression «intérieure» F utilisant x comme libre, de l'«extérieur» où x est liée. Appliqué à la donnée du symbole x et de l'expression F, il donne une valeur dépendant de la structure unaire définie par F d'argument x (mais ne peut généralement pas donner une copie fidèle de la structure, parfois trop complexe pour être enregistrée par un simple objet).
Leur format diffère entre la théorie des ensembles et les théories génériques, qui gèrent le domaine différemment. Dans les théories génériques, les domaines sont des types, données implicites des quantificateurs. Mais les symboles liants en théorie des ensembles prennent comme domaine un ensemble, objet désigné par un argument supplémentaire (espace pour un terme n'utilisant pas la variable liée).

Une expression est dite close si toutes ses variables sont liées (leurs occurrences sont contenues par des symboles liants).

Présentons les principaux symboles liants en théorie des ensembles.

Définitions des fonctions par des termes

Le définisseur de fonction (  ∋   ↦  ) lie une variable sur un terme, suivant la syntaxe (Ext(x)) où x est la variable, E est son domaine, et t(x) est le terme (ici abrégé en prédicat unaire avec d'éventuels paramètres implicites); on peut l'abréger en (xt(x)) lorsque E est dicté par le contexte. Admissible si t(x) est admissible pour tout x dans E, il prend le foncteur défini par t et en restreint la classe d'admissibilité à E, pour le donner comme fonction de domaine E.
Il convertit donc les foncteurs en fonctions, à l'inverse du rôle de l'évaluateur de fonction qui convertissait les fonctions en leur rôle (signification) comme foncteurs dont les classes d'admissibilité étaient des ensembles. Ceci uniformise en un type unique d'objets les foncteurs qui étaient seulement indirectement utilisables comme fonctions par les termes de complexité illimitée qui les définissaient.
En 1.10 on formalisera cet outil, vu comme cas particulier d'un principe plus général de théorie des ensembles.

Relations et symbole de compréhension

Une relation est un objet semblable à une opération mais à valeurs booléennes: il joue un rôle de prédicat dont les arguments parcourent des ensembles. Mais il n'y a pas besoin d'introduire cela comme une autre sorte d'objets, car les ensembles feront l'affaire.
Pour tout prédicat unaire A admissible dans un ensemble E, la sous-classe de E définie par A est un ensemble (car domaine d'une variable x introduite comme parcourant E, donc liable, dont on sélectionne les valeurs satisfaisant A(x)), donc un sous-ensemble ou une partie de E, noté {xE|A(x)} (ensemble des x dans E tels que A(x)): pour tout y,

y ∈ {xE|A(x)} ⇔ (yEA(y))

Le symbole { ∈  |  } sera appelé symbole de compréhension : {xE | A(x)} lie x de domaine E sur la formule A. Il servira de définisseur de relations unaires sur E, figurées comme parties F de E, et évaluées par ∈ comme prédicats (xF) d'argument x. Mais ces prédicats sont admissibles non seulement sur E mais sur tout l'univers, valant 0 hors de E dont la donnée est perdue. Cette absence d'opérateur Dom n'importe guère, le domaine E étant généralement dicté par le contexte.
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 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).

Paradoxe de Russell

Bien sûr, si la classe de tous les objets était un ensemble alors le symbole de compréhension pourrait l'utiliser pour traduire toutes les classes en ensembles. Mais ce n'est pas possible: la classe de tous les ensembles ne peut pas être un ensemble (aucun ensemble E ne peut contenir tous les ensembles), 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 FE.

Preuve. F={xE | Set(x) ∧ xx} ⇒ (FF ⇔ (FEFF)) ⇒ (FFFE). ∎

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

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
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 en théorie des ensembles
1.9. Quantificateurs
1.10. Formalisation de la théorie des ensembles
1.11. Principe de génération des ensembles
Aspects philosophiques
Temps en théorie des modèles
Temps en théorie des ensembles
Interprétation des classes
Concepts de vérité en mathématiques
2. Théorie des ensembles (suite)
3. Théorie des modèles

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