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é {xE | A(x)} (ensemble des x dans E tels que A(x)): pour tout y,

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

Cette combinaison de caractères { ∈  |  } forme la notation d'un symbole liant appelé symbole de compréhension : {xE | 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 FE. Ainsi aucun ensemble E ne peut contenir tous les ensembles.

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

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 (Ext(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 xt(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 ↦ (xS). 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).

Définisseurs de structure dans diverses théories

Appelons définisseur de structure tout symbole liant B qui, utilisé dans diverses expressions A, enregistre fidèlement la structure unaire définie par A sur un domaine E (type ou classe définie par un argument ici implicite), à savoir que son résultat S = (Bx, A(x)) peut restaurer cette structure par un évaluateur V (symbole ou expression): V(S, x) = A(x) pour tout x dans E. Admettant l'utilisation de la négation et la possibilité d'interpréter des booléens par des objets (dans un ensemble à au moins deux objets, comme cela arrive souvent), le paradoxe de Russell montre que l'ajout des deux exigences suivantes à un définisseur de structure dans une théorie conduirait à une contradiction:
  1. Tous ces S appartiennent à E
  2. V peut apparaître dans l'expression A et utiliser x n'importe comment dans ses arguments, à savoir que V(x, x) est autorisé, ce qui est normal comme 1. garantit l'admissibilité de tout V(S, S).
Enumérons les options restantes. La théorie des ensembles rejette 1. mais conserve 2. Mais puisque 1. est rejeté, conserver 2. peut être un problème ou non suivant les cas plus précis.

Comme sera expliqué en 4.9, étendre une théorie générique (dont les domaines des symboles liants étaient les types) par un nouveau type K donné comme l’ensemble de toutes les structures définies par une expression fixe A pour toutes les combinaisons de valeurs de ses paramètres, constitue un développement légitime de la théorie (une construction). En effet, un symbole liant sur un symbole de structure variable S parcourant un tel ensemble K abrége une utilisation successive de symboles liants sur tous les paramètres de A qui remplace S. Ici, A et le système l’interprétant viennent d'abord, puis l'ensemble K des S résultants et leurs interprétations par V sont créés en dehors: A n'a pas de sous-terme de type K, donc n'utilise pas V (qui a un argument de type K).

La notion de structure en logique du premier ordre en tant que théorie du modèle, présente cette similitude avec la notion d'ensemble en théorie des ensembles: pour chaque type de symbole donné au-delà des constantes, la classe de toutes les structures de ce type n'est généralement pas un ensemble, appelant "ensembles" de tels domaines K (ensembles de structures définies par une expression fixe avec des paramètres variables), ou des sous-classes de ceux-ci. La théorie entièrement développée avec l'infinité de ces nouveaux types construits pour toutes les expressions possibles A, peut devenir similaire à la théorie des ensembles en regroupant en un seul type U tous les types construits K de structures variables du même type de symbole (structures sur les mêmes ensembles), interprété par le même symbole V (qui pourrait déjà être utilisé par A). Ceci ne fait que réunir en V différentes structures sans conflit, car venant de différents types K du premier argument. Cela reste innocent (une réécriture de ce qui peut être fait sans cela) tant que, dans la nouvelle théorie, les symboles liants de type U restent limités à l'un de ces "ensembles" K (ou sont couverts par un nombre fini d'entre eux, qui sont en fait inclus dans un autre).

En théorie des ensembles, les domaines des symboles liants sont les ensembles. Ainsi, au-delà de l'avantage simplificateur de supprimer les types, la théorie des ensembles gagnera de la puissance en acceptant plus de classes comme ensembles.

D'autres théories, que nous ignorerons dans la suite de ce travail, suivent des options plus audacieuses:
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