1.6. Variables liées en théorie des ensembles

La dernière sorte de symbole formant les expressions est celle des symboles liants, qui lient une (ou plusieurs) variable(s) (disons x), séparant l'intérieur (la sous-expression, utilisant x comme libre) de l'extérieur (où x est liée). Un tel symbole donne une valeur dépendant de la structure, d'argument x, définie par la sous-expression sur laquelle il s'applique. Cette valeur ne peut pas fidèlement décrire toute la structure (qui n'est pas un objet), mais en extrait une information.
Leur format diffère entre la théorie des ensembles et les théories génériques, qui gèrent les domaines différemment: contrairement aux théories génériques (où les domaines étant des types sont des données implicites des symboles liants), le domaine d'une variable liée en théorie des ensembles est un objet (ensemble), donné comme argument du symbole liant (lieu à remplir par un terme de valeur un ensemble), s'ajoutant aux données du symbole x à lier et de l'expression visée (seule à utiliser x).
Une expression est dite close si toutes ses variables sont liées.
Présentons les principaux symboles liants en théorie des ensembles.

Définitions de fonctions par des termes
Le définisseur de fonction ∋   ⟼ lie une variable x de domaine E sur un terme t dépendant de x, suivant la syntaxe (Ext(x)) parfois abrégée en (xt(x)) lorsque E est donné par le contexte.
Valide si t est valide pour tout x dans E, il traduit en fonction de domaine E, le foncteur défini par t considéré sur E (de validité réduite à E). C'est en gros la traduction inverse de celle, de fonction en foncteur valide sur un ensemble, opérée par l'évaluateur de fonction.
D'autres notions seront définies comme classes d'objets avec des outils traduisant chaque objet en son rôle et inversement. Des objets déjà présents (ensembles ou fonctions) pourront jouer les nouveaux rôles, offrant leurs outils aux nouveaux objets. Les seules traductions nécessaires entre objets jouant un même rôle, relieront différentes représentations utiles d'un nouvel objet par des anciens.

Formalisation des opérations et curryfication
Les opérations n-aires jouant le rôle d'opérateurs n-aires entre n ensembles, se formalisent par:
Une représentation des opérations comme classe de fonctions, nommée curryfication, consiste à employer comme définisseur liant n variables la succession de n usages du définisseur de fonction (un pour chaque variable à lier), et donc de même comme évaluateur, n usages de l'évaluateur de fonction:

f=(Ex, Fyt(x,y))
≅ (Ex ⟼ (Fyt(x,y)))=g


f(x,y)
=g(x)(y)=t(x,y)
passant par la fonction g(x)=(Fyt(x,y)) d'argument y, voyant x libre et y liée. Mais cela rompt la symétrie des rôles entre arguments en leur choisissant un ordre, et perd la donnée de F lorsque E est vide. Une formalisation sans ces défauts sera possible une fois introduits les n-uplets.

Relations et symbole de compréhension
Une relation est comme une opération mais à valeurs booléennes, jouant le rôle de prédicat dont la validité (les domaines des arguments) est réduite à des ensembles. Les relations n-aires se formalisent par un prédicat évaluateur d'arité n+1, et un définisseur liant n variables sur une formule. On pourrait les construire comme opérations en traduisant les booléens en objets. Mais voici l'autre méthode.
Pour tout prédicat unaire ℛ valide dans un ensemble E, la sous-classe de E définie par ℛ est un ensemble (car domaine d'une variable x parcourant E, donc liable, telle que ℛ (x)), noté {xE| ℛ (x)} (ensemble des x dans E tels que ℛ (x)), qualifié de partie ou sous-ensemble de E: pour tout y,
y ∈ {xE| ℛ (x)} ⇔ (yE et  ℛ (y))
Le symbole de compréhension {  ∈  | }, liant x à E sur ℛ , servira de définisseur de relations unaires sur E figurées comme parties F de E, évaluées par ∈ comme prédicats (xF) d'argument x. Mais ces prédicats sont valides sur tout l'univers, valant faux 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.
Les symboles de définisseur et de compréhension enregistrant toute la structure définie par l'expression sur l'ensemble donnés, suffisent à définir tout autre symbole liant comme structure exercée dessus. Les relations n-aires sont définissables par 1 compréhension et n−1 définisseurs de fonction.
Plus généralement, pour toute sorte de méta-objets indirectement utilisables dans les expressions comme des objets (une classe comme un ensemble...), la théorie des ensembles s'enrichira d'outils les concrétisant et désignant directement comme objets.


1.5.  <—
Classes en théorie des ensembles

Sommaire
>     1.7.
Quantificateurs