En mathématiques, on manipule souvent des égalités, mais il n’est pas habituel, si l’on n’est pas logicien, de s’interroger sur ce que recouvre cette notion d’égalité. J’aimerais évoquer ici quelques problèmes que le traitement de l’égalité peut poser ; j’ai essayé dans la mesure du possible de donner des exemples familiers de tous. J’ai mis entre crochets des digressions plus techniques.

On définit parfois l’« égalité de Leibniz » ainsi : « deux objets sont égaux si toute propriété vraie de l’un est vraie de l’autre » ; autrement dit, ils sont indistinguables. Cette définition est séduisante, mais souffre de difficultés, comme nous allons le voir.

(Une petite parenthèse. On appelle cette définition « égalité de Leibniz », mais j’ignore si Leibniz l’a effectivement posée comme telle. En mathématiques, il n’est pas rare d’attribuer à des auteurs des définitions qu’ils n’ont pas posées mais qui sont dans le fil de leurs idées ou de définitions qu’ils ont posées. J’invite les historien·ne·s des mathématiques à laisser des commentaires...)

Prenons l’égalité d’école primaire, 1+3=3+1. Le membre de gauche, 1+3, est distinguable du membre de droite, 3+1 : le premier commence par 1 (ou, si on le voit comme arbre syntaxique, est un nœud + dont la branche de gauche est 1), le second par 3 ! Il est faux que toute proposition vraie de l’un est vraie de l’autre !

On m’objectera que mon critère est trop syntaxique et omet la sémantique de l’opération d’addition. Bien. Tentons donc de définir celle-ci : si l’on définit les entiers naturels comme étant soit 0 soit le successeur S(x) d’un naturel x, et que l’on considère 1 comme une notation pour S(0) et 3 comme une notation pour S(S(S(0))), on peut définir x+S(y) comme S(x+y) et x+0 comme x. Cela induit une notion de calcul : tant qu’on a une expression de la forme x+S(y) on peut la remplacer par S(x+y), jusqu’à ce qu’il ne soit plus possible de procéder à pareils remplacements — on dit que l’on obtient alors une forme normale. En termes techniques, on parle de système de réécriture, et effectivement les formes normales associées à 1+3 et 3+1 sont bien identiques.

[Cette définition par réécriture est séduisante, mais elle suppose que chaque terme ait une forme normale unique, ce qui n’est pas vrai en général ; on devra donc démontrer des propriétés de confluence et de terminaison du système de réécriture.]

Cette intervention du calcul n’est toutefois pas suffisante pour démontrer une égalité tout aussi familière, à savoir 0+x=x+0. En effet, si la réécriture transforme le membre de droite en x, le membre de gauche reste 0+x. Pour parvenir à démontrer l’égalité, on doit faire intervenir un raisonnement par récurrence sur x : on constate que c’est vrai pour x=0, que si c’est vrai pour x alors c’est vrai pour x+1, donc on conclut que c’est vrai pour tout x.

[La vision syntaxique n’est pas si stupide qu’il n’y paraît. Ceux qui ont fait de la logique se rappelleront peut-être comment on définit le domaine de Herbrand des termes, et que l’on peut construire (pour démontrer le théorème de compacité, le théorème de complétude ou le théorème de Lowenheim-Skolem) un modèle en quotientant ce domaine par une relation d’équivalence. La relation d’égalité sémantique est ainsi une relation d’équivalence entre termes (vus syntaxiquement) compatible avec les opérations et les prédicats (on parle de congruence) et avec le système d’axiomes.]

Prenons maintenant un autre exemple familier : les « fractions », ou, pour parler en termes plus savants, les nombres rationnels. On sait que 2/3=4/6. Pourtant, là encore, on peut distinguer 2/3 et 4/6 : ils n’ont pas le même numérateur ! Une notion d’égalité à la Leibniz n’est donc utilisable que si l’on restreint les propriétés par lesquelles on est autorisé à distinguer les éléments : on va ainsi interdire de faire intervenir des questions sur le numérateur ou le dénominateur. On va donc considérer comme égaux des éléments indistinguables selon une certaine définition de l’observabilité.

On peut également, en l’espèce, définir l’égalité sur les formes « réduites » des fractions, c’est-à-dire celles où un calcul a éliminé les facteurs communs au numérateur et au dénominateur (par exemple, dans 4/6, il y a un facteur commun 2 au numérateur et au dénominateur). Là encore, c’est une commodité appréciable…

Lorsque l’on définit les fractions, on parle de couples d’entiers — par exemple ici (2,3) et (4,6). Nous avons vu que ce n’est pas tout à fait exact, vu que l’on considère comme égaux tous les couples d’entiers qui se réduisent identiquement, bref toute une classe d’équivalence d’entiers — mais passons. Évoquons maintenant le fait bien connu que 2=4/2. 2 est un entier, 4/2 est une fraction donc un couple d’entiers ; a priori ces deux objets ne vivent pas dans le même univers — un entier, ce n’est pas la même chose qu’un couple d’entiers ! Nous les identifions pourtant ; si nous étions parfaitement rigoureux, nous devrions évoquer le fait que l’entier x et le rationnel x/1 se comportent exactement pareil du point de vue des opérations arithmétiques et des comparaisons, ce qui nous permet de les identifier (en termes savants, faire intervenir l’injection canonique des entiers dans les rationnels, préservant la structure d’anneau ordonné).

D’une façon générale, les écrits mathématiques usuels abondent de ces « abus de notation », de ces raisonnements « à équivalence près ». Il y a souvent, outre le discours de la preuve elle même, un méta-discours expliquant au lecteur comment combler les omissions et raccourcis : les « sans perte de généralité », les avertissements que certains objets distincts seront identifiés, etc. Tout ceci aide à alléger un discours mathématique qui, sinon, deviendrait trop lourd donc peu lisible et compréhensible pour les humains.

Les difficultés arrivent lorsque l’on transcrit des raisonnements rédigés pour des humains en des raisonnements destinés à être vérifiés étape par étape par une machin, par des logiciels tels que Coq. En effet, dans ce cas, il faut soit expliciter les identifications, abus de notation et autres détails de raisonnement qui avaient permis d’alléger la rédaction, soit utiliser des mécanismes du logiciel destinés à les reconnaître (par exemple, certains allègements de rédaction se traitent en Coq avec le mécanisme des structures canoniques ; les raisonnements à équivalence près se traitent par les setoids, etc.).

[Ces mécanismes ne sont toutefois par parfaits, loin s’en faut ; mon collègue Pierre Corbineau, lorsque je lui ai demandé à quel point on évitait les problèmes avec les setoids m’a dit « ça marche… sauf quand ça ne marche pas » (il me semble notamment qu’il est très difficile de raisonner modulo équivalence sur l’argument d’un type dépendant). On pourrait également mentionner le fait qu’en Coq, donner un élément vérifiant une certaine propriété (par exemple, donner un entier n inférieur à une certaine borne) revient à donner un couple formé de l’élément et d’une preuve que l’élément vérifie la propriété ; bien que rien d’effectivement observable ne dépende de quelle preuve est utilisée (on peut prouver le même fait mathématique d’une multitude de façons), on peut entrer dans de grandes complications en raison de la non identification d’objets ne différant que par les preuves. D’une façon générale, en Coq, on gagne à travailler avec des objects syntaxiquement uniques, ou, à défaut, avec des formes normales.]

On parle beaucoup, ces dernières années, de remplacer le traitement de l’égalité en théorie des types (notamment en Coq) par des fondations univalentes. Si j’ai bien compris, il s’agit de donner un meilleur traitement de l’égalité. Je ne comprends cependant pas le rapport entre d’une part les problèmes de raisonnement modulo équivalence et la solution proposée, basée sur des notions d’homotopie !