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 (E ∋ x ⟼ t(x)) parfois
abrégée en (x ⟼ t(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:
n foncteurs de domaines (peu utiles en pratique);
un évaluateur f(x1,…,xn)
d'arité n+1, d'arguments l'opération f et ses arguments
x1,…,xn;
un définisseur, liant n variables sur un terme. Celui
liant x et y de domaines E et F sur t
se note (E ∋ x, F ∋ y ⟼ t(x,y)).
On simplifiera (E ∋ x, E ∋ y ⟼ t(x,y))
en (E ∋ x, y ⟼ t(x,y)).
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=(E ∋
x, F ∋ y ⟼ t(x,y))
≅ (E ∋ x
⟼ (F ∋ y ⟼ t(x,y)))=g
f(x,y)
=g(x)(y)=t(x,y)
passant par la fonction g(x)=(F ∋ y ⟼ t(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é {x ∈ E| ℛ (x)} (ensemble des x
dans E tels que ℛ (x)), qualifié de partie ou
sous-ensemble de E: pour tout y,
y ∈ {x ∈ E|
ℛ (x)} ⇔ (y ∈ Eet
ℛ (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 (x ∈ F) 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.