2.3. Curryfication et uplets

Formalisation des opérations et relations

Formaliser en théorie des ensembles chaque notion d'opération (resp. relation) d'arité fixe n > 1, agissant comme structures n-aire entre n ensembles, requiert les symboles suivants (généralisant le cas n = 1 des fonctions, accepté comme primitif): Donnons aux définisseurs d'opérations la notation suivante qui sera plus tard (2.7) justifiée comme reflétant leurs définitions: dans le cas binaire (n = 2) les opérations définies par un opérateur binaire A de domaines E et F seront notées

E×F ∋ (x,y) ↦ A(x,y)

Ayant vu ce que sont les opérations et relations (leurs rôles), discutons comment elles sont réductibles à autre chose. Un aspect est que les relations sont réductibles aux opérations, et vice-versa: Ces constructions sont utiles malgré la circularité (elles ne réduisent pas l'arité). Mais pour des motifs fondateurs on a besoin d'une construction réduisant à des cas d'arité inférieure, jusqu'aux ensembles et aux fonctions. Il y a en fait 2 telles constructions.

Curryfication

Les plus simples constructions des notions d'opérations n-aire à partir de nos outils primitifs pour les fonctions, sont leurs représentations curryfiées, définies comme classes de fonctions en exprimant le définisseur d'opération comme n usages successifs du définisseur de fonction (un pour chaque variable liée); et donc l'évaluateur comme n usages de l'évaluateur de fonctions. Pour n = 2, cela signifie qu'une opération binaire sous forme curryfiée b de domaines E et F se définit par un opérateur binaire B, et s'évalue en retour comme B, par les formules

b = (Ex ↦ (FyB(x,y)))
Dom b = E ∧ ∀xE, Dom b(x) = F ∧ ∀yF, B(x,y) = b(x)(y)

dont l'équivalence, similaire à l'axiome 1. des fonctions, s'en déduit.
Le premier foncteur de domaine vient par Dom b = E, mais le second, donné comme valeur commune de tous les Dom b(x), n'est défini que pour E ≠ ∅. La fonction intermédiaire b(x) = (FyB(x,y)) représente le foncteur défini par B de paramètre x (libre) et d'argument y (lié).
Cela fait en gros fonctionner chaque opération binaire comme un évaluateur de fonction, en donnant à x un rôle de fonction d'argument y; l'évaluateur de fonction curryfié rend simplement chaque fonction qu'il prend: f ↦ ((Dom f) ∋ yf(y)).

De même, la notion de relation n-aire se définit sous forme curryfiée comme une classe, donnant le rôle de définisseur à une succession de n−1 usages du définisseur de fonction et 1 usage du symbole de compréhension. Ainsi la forme curryfiée r d'une relation binaire de domaines E et F, se définit à partir d'un prédicat binaire R, et s'évalue en retour comme R, par les formules équivalentes

r = (Ex ↦ {yF | R(x,y)})
Dom r = E ∧ (∀xE, r(x) ⊂ F ∧ ∀yF, R(x,y) ⇔ yr(x))

Cela ne laisse aucun moyen de définir le second foncteur de domaine (F ne peut pas être restauré à partir de r). Ces constructions ont le défaut de rompre la symétrie des rôles entre les arguments. La méthode de construction suivante, par les uplets, conservera cette symétrie, et sera généralement préférée pour cette raison.

Uplets

Pour toute théorie et tout nombre naturel n, une notion de n-uplet est une notion construite comme domaine de variables servant à abréger une liste de n symboles de variables appartenant à des notions données précédemment acceptées. Un 2-uplet s'appelle un couple, un 3-uplet est un triplet, un 4-uplet est un quadruplet et ainsi de suite. Ainsi, chaque uplet x (objet ainsi construit) représente une méta-fonction d'«interprétation» de cette liste (méta-ensemble) de n variables, vers le modèle.

Les symboles définisseurs et évaluateurs des uplets ont une forme spéciale car, bien qu'étant des méta-fonctions, les uplets jouent dans la théorie un rôle autre que ceux de foncteurs ou fonctions.

Un définisseur de n-uplets n'est pas un symbole liant mais un opérateur n-aire, qui rassemble ses n variables en une en les prenant comme arguments dans une parenthèse et séparées par des virgules: ( ,…, ).

Ainsi, chaque structure (resp. opération, relation) peut être re-formalisée comme une structure unaire (resp. une fonction, une relation unaire) de domaine un type (resp. une classe qui est en fait un ensemble) d'uplets, à utiliser avec le définisseur d'uplets qui convient. Cela peut être implicitement fait en réinterprétant la notation: S(x,y) peut être lu en voyant S soit comme une structure binaire (resp. opération, relation), soit comme une structure unaire prenant comme argument le couple donné par le terme (x,y) formé par le définisseur de couples d'arguments x et y.

Le rôle de l'évaluateur de n-uplets est joué par une liste de n foncteurs appelés projections qui extraient chaque variable de la liste donnée (en donne la valeur). Cette liste joue le rôle de l'évaluateur de fonctions curryfié dans le sens inverse, en fixant son méta-argument dont le domaine (le domaine des uplets en tant que méta-fonctions) n'est pas vu par la théorie comme un ensemble d'objets mais comme une liste de n symboles à prendre séparément.

Les détails formels de cette construction varient selon que nous prenons une théorie générique ou une théorie des ensembles.

Axiome des uplets

Dans les théories génériques, ce doit être un type construit distinct pour non seulement chaque n mais aussi chaque choix du type de chacune de ces n variables (si on part d'une théorie avec plusieurs types - ce choix d'une liste de variables avec leurs types revient au choix d'un type de symbole de prédicat), mais cela forme directement une construction légitime (4.11). Pour n=2 (les autres cas sont similaires), et pour un type P de couples (x,y) où x,y ont les types E et F, les projections π0 et π1 sont liées au définisseur de couples, par l'axiome

E x, ∀F y, ∀P z, (x = π0(z) ∧ y = π1(z)) ⇔ (x,y) = z

qui implique

P z, (π0(z), π1(z)) = z
E x, ∀F y, π0(x,y) = x
E x, ∀F y, π1(x,y) = y
E x,x', ∀F y,y', (x,y) = (x',y') ⇔ (x = x'y = y')

Uplets en théorie des ensembles

La théorie des ensembles n'ayant pas de types n'a besoin que d'une notion de n-uplet pour chaque n. Mais il y a une difficulté: pour justifier rigoureusement que tous les outils de la théorie des ensembles restent applicables aux uplets de la même manière qu'au reste des éléments, les uplets doivent être intégrés parmi les éléments. À savoir, la théorie des ensembles doit développer ses notions d'uplets en les définissant comme des classes d'éléments déjà existants, au lieu de simplement les accepter par les constructions ci-dessus, qui les laissaient comme des types séparés.

Pour cela, les uplets étant des méta-fonctions, ils sont naturellement représentés par des fonctions. Cela suppose de copier leur méta-domaine, qui est une liste de symboles, en un ensemble (d'éléments). À savoir, représentons le domaine des n-uplets considérés par l'ensemble Vn des n nombres de 0 à n−1 tous désignés par des symboles de constantes que nous concevrons simplement comme des chiffres. Pour justifier cela comme un développement de la théorie des ensembles, ces chiffres peuvent être définis par des termes clos de valeurs distinctes, tels que ∅, {∅}, {∅, {∅}} et autant qu'on voudra d'autres ensembles et fonctions exprimables à partir de là. La notion de n-uplet est alors définie comme la classe de toutes les fonctions de domaine Vn.

Puis les projections sont définies par l'évaluateur de fonction appliqué aux chiffres respectifs, ce qui peut être lu comme déguisé dans leurs notations: pour tous n-uplets x,

iVn, πi(x) = x(i).

Cette notation indicielle, jouant sur l'équivalence entre lire l'indice i comme un argument ou un méta-argument visant à prendre le i-ème symbole d'une liste (ici πi est la i-ème projection donnant valeur de la i-ième variable), est également couramment utilisée pour les uplets: xi peut être lu comme la i-ème variable dans l'uplet x = (x0,…,xn−1), ou comme une troisième notation pour le même évaluateur après x(i) et πi(x).

D'autres d'outils doivent être introduits avant de définir en théorie des ensembles les définisseurs d'uplet (2.4) et les définisseurs d'opération utilisant les uplets (2.6).

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles
2.1. Premiers axiomes de théorie des ensembles
2.2. Principe de génération des ensembles
2.3. Curryfication et uplets
2.4. Quantificateurs d'unicité
2.5. Familles, opérateurs booléens sur les ensembles
2.6. Graphes
2.7. Produits et ensembles des parties
2.8. Injections, bijections
2.9. Propriétés des relations binaires
2.10. Axiome du choix
Temps en théorie des ensembles
Interprétation des classes
Concepts de vérité en mathématiques
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
EN : 2.3. Tuples