A Naive Encoding of Russell's Paradox in Type Theory

Dans le vaste paysage des mathématiques, il existe une tension fondamentale entre la manière dont nous organisons les idées et les règles que nous utilisons pour les construire. Depuis plus d'un siècle, les mathématiciens s'appuient sur un cadre appelé théorie des types pour garantir que leurs structures logiques sont saines et exemptes de contradictions. Imaginez ce système comme un classeur rigoureux où chaque objet doit appartenir à un dossier spécifique, et où les dossiers ne peuvent pas se contenir eux-mêmes ou d'autres dossiers d'une manière qui créerait une boucle. Cette séparation empêche un célèbre piège logique connu sous le nom de paradoxe de Russell, un casse-tête du début des années 1900 qui a montré comment une question simple — « L'ensemble de tous les ensembles qui ne se contiennent pas eux-mêmes se contient-il lui-même ? » — peut briser un système si les règles sont trop lâches. Bien que les mathématiques modernes aient réussi à éviter ce piège en séparant strictement ces catégories, les chercheurs continuent d'explorer les limites de ces systèmes pour comprendre précisément où et pourquoi ils tiennent bon.

Une note récente de Qu Zhuoyuan, de l'Université de Nagoya, examine directement cette limite, démontrant comment l'on pourrait accidentellement recréer ce paradoxe ancien au sein d'un système moderne de théorie des types. L'auteur ne prétend pas avoir trouvé une faille dans les mathématiques standard, mais montre ce qui se passe si l'on retire délibérément un mécanisme de sécurité spécifique. Dans cette expérience, le chercheur construit un scénario où un « univers » de types est autorisé à se contenir lui-même, une condition connue sous le nom de « type-dans-type » (type-in-type). En combinant cela avec une manière spécifique de traiter l'égalité — où toute preuve que deux choses sont identiques est traitée comme identique — l'auteur parvient à construire une structure logique qui reflète le paradoxe original. Le résultat est une preuve claire et directe que si vous permettez à un univers de se contenir lui-même et que vous supposez que toutes les preuves d'égalité sont identiques, le système s'effondre dans la contradiction.

La construction fonctionne en définissant une collection spéciale qui rassemble tous les types possibles, tel un catalogue maître de toutes les catégories. Au sein de cette collection, le chercheur définit un groupe spécifique : le groupe de toutes les choses qui n'appartiennent pas à elles-mêmes. Dans un système normal et sûr, ce groupe ne peut pas exister car les règles empêchent une catégorie d'être membre d'elle-même. Cependant, dans cette configuration spécifique, l'auteur crée un moyen de demander si ce groupe appartient à lui-même. La logique suit un chemin étroit et inéluctable : si le groupe appartient à lui-même, alors par sa propre définition, il ne le doit pas ; mais s'il n'appartient pas à lui-même, alors il correspond à la définition et doit appartenir à lui-même. Cela crée une boucle où l'énoncé est à la fois vrai et faux en même temps, prouvant que le système est incohérent.

Ce qui rend cette découverte particulièrement significative est l'outil spécifique utilisé pour faire fonctionner le paradoxe. L'auteur s'appuie sur un principe appelé unicité des preuves d'identité, qui stipule essentiellement que si vous pouvez prouver que deux choses sont égales, il n'existe qu'une seule façon de le faire. Ce principe est souvent supposé dans de nombreux systèmes mathématiques standards pour simplifier le raisonnement. L'article montre que cette supposition, combinée à un univers qui se contient lui-même, est suffisante pour déclencher le paradoxe. Crucialement, l'auteur souligne que cette construction échouerait dans un cadre plus moderne appelé théorie de l'homotopie des types, où l'unicité des preuves d'identité n'est pas supposée. Dans ce système alternatif, il existe de nombreuses façons différentes de prouver que deux choses sont égales, et cette variété empêche le paradoxe de se former.

L'article distingue également son approche des tentatives précédentes pour recréer ce paradoxe. Des travaux antérieurs menés par d'autres chercheurs utilisaient des structures complexes, de type arborescentes, pour parvenir à un résultat similaire, ce qui nécessitait des mécanismes plus complexes. Cette nouvelle approche est plus simple et plus directe, utilisant uniquement les éléments de base des types et des connexions logiques sans avoir besoin de ces arbres complexes. Elle réduit le problème à ses composants fondamentaux, montrant que le paradoxe n'est pas le résultat d'une machinerie complexe, mais une conséquence directe de l'autorisation d'un univers à se contenir lui-même tout en traitant toutes les preuves d'égalité comme identiques. Toute la chaîne logique a été vérifiée par des assistants de preuve informatiques, confirmant que les étapes sont valides et que la contradiction est réelle au sein des règles définies.

En fin de compte, ce travail sert de carte précise d'une zone de danger logique. Il ne suggère pas que les mathématiques sont brisées, mais clarifie exactement quelles règles sont nécessaires pour les garder sûres. En montrant que le paradoxe peut être construit avec un ensemble spécifique d'hypothèses, l'auteur renforce l'importance de ces hypothèses pour prévenir l'effondrement logique. C'est un rappel que dans l'architecture des mathématiques, même une seule règle assouplie concernant la manière dont nous traitons l'égalité ou la manière dont nous organisons les univers peut mener à une structure qui supporte sa propre destruction. L'étude constitue une démonstration claire que la cohérence n'est pas un acquis, mais un état soigneusement maintenu qui dépend des contraintes spécifiques que nous choisissons d'imposer.