💻 computer science

Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

Cet article analyse les quatre paradoxes mécanisés dans la bibliothèque coq-paradoxes pour démontrer comment ils définissent collectivement les limites de conception nécessaires du noyau Rocq — spécifiquement concernant l'imprédicativité, l'élimination large et les contraintes d'univers — en illustrant les raisons précises pour lesquelles le système doit rejeter certaines constructions afin de maintenir la cohérence.

Auteurs originaux : Bernardo Alonso

Publié 2026-05-28

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Bernardo Alonso

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous avez un architecte robot très strict et très intelligent nommé Rocq. Sa tâche consiste à construire des structures logiques (des preuves mathématiques) garanties sûres et cohérentes. Il ne plante jamais, ne ment jamais et ne produit jamais de contradiction.

Mais comment savez-vous que le robot accomplit correctement son travail ? Vous ne vous contentez pas de le regarder construire ; vous essayez de le piéger. Vous essayez de lui fournir un plan qui semble devoir fonctionner mais qui contient en réalité un piège caché capable de faire effondrer tout l'édifice.

Ce papier traite d'une bibliothèque spéciale de « plans pièges » appelée coq-paradoxes. Elle contient quatre tentatives spécifiques pour briser la logique du robot. L'article soutient que ce ne sont pas simplement des énigmes ou des curiosités ; ce sont en réalité le manuel de sécurité du robot écrit à l'envers. Ils montrent exactement où les règles du robot sont tracées pour prévenir les catastrophes.

Voici une analyse des quatre pièges et de ce qu'ils nous enseignent, en utilisant des analogies simples :

1. Le piège de Burali-Forti : « La boîte qui se contient elle-même »

Le Piège : Imaginez une bibliothèque où chaque livre possède une étiquette décrivant son propre contenu. Le paradoxe tente de créer un « Catalogue Maître » qui répertorie chaque livre de la bibliothèque, y compris le Catalogue Maître lui-même.
Le Problème : Si le catalogue est un livre, il doit se répertorier lui-même. Mais s'il se répertorie, il modifie la taille de la bibliothèque, ce qui modifie le catalogue, ce qui modifie la bibliothèque... c'est une boucle qui brise les règles de la taille.
La Leçon : Le robot (Rocq) possède une règle concernant la Hiérarchie des Univers. Il dit : « Une boîte ne peut pas être à l'intérieur d'une boîte de la même taille qu'elle-même. » Le robot refuse de construire le Catalogue Maître car les mathématiques indiquent que la « boîte intérieure » doit être plus petite que la « boîte extérieure ». Ce piège prouve que le robot applique correctement une limite de taille stricte pour prévenir les boucles infinies.

2. Le piège de Diaconescu : « Le lanceur de pièces magique »

Le Piège : Imaginez une machine capable de choisir un « gagnant » parmi n'importe quel groupe d'options à égalité (comme choisir un représentant parmi un groupe de jumeaux identiques). Le paradoxe dit : « Si vous me donnez cette machine, je peux la forcer à me révéler la réponse à n'importe quelle question par oui ou par non (comme « Le ciel est-il bleu ? ») sans connaître réellement la réponse. »
Le Problème : Dans un système constructif (où vous devez construire la réponse, pas simplement la deviner), posséder une machine capable de choisir des gagnants parmi des égalités est trop puissant. Cela force secrètement le système à accepter « Soit A est vrai, soit A est faux » pour tout, même pour des choses que nous ne pouvons pas encore prouver.
La Leçon : Le robot possède une règle concernant l'Élimination Large. Il dit : « Vous pouvez choisir un gagnant parmi un groupe de nombres, mais vous ne pouvez pas utiliser cela pour décider magiquement d'une vérité philosophique. » Ce piège montre que si le robot autorisait ce type de « choix magique », il briserait accidentellement la capacité du système à distinguer entre les choses que nous connaissons et celles que nous ne connaissons pas.

3. Le piège de Reynolds : « Le dictionnaire qui ne peut pas exister »

Le Piège : Imaginez essayer de créer un dictionnaire où chaque définition possible est un mot dans ce dictionnaire. Le paradoxe tente de construire un « Dictionnaire Universel » qui mappe chaque phrase possible vers un seul mot.
Le Problème : C'est comme essayer de faire tenir une carte du monde entier sur un seul timbre-poste. Les mathématiques prouvent que si vous essayez de compresser toutes les déclarations logiques possibles en un seul type d'objet, vous créez une contradiction (similaire au fait que vous ne pouvez pas lister toutes les listes possibles).
La Leçon : Le robot possède une règle concernant l'Impredicativité (permettre à une définition de se référer à l'ensemble entier auquel elle appartient). Le robot l'autorise pour les « Propositions » (des affirmations vraies/fausses simples) mais trace une ligne dure ailleurs. Ce piège montre que si le robot autorisait ce type de « dictionnaire universel » pour des types complexes, tout le système s'effondrerait.

4. Le piège de Hurkens : « Le miroir autoréférentiel »

Le Piège : C'est le plus complexe. Imaginez un miroir qui reflète une réflexion, qui reflète une réflexion, et ainsi de suite, pour toujours. Le paradoxe tente de construire un système où vous pouvez observer un objet « petit » (comme un booléen vrai/faux) et l'utiliser pour définir un objet « grand » (comme tout un univers de types), puis utiliser cet objet grand pour redéfinir le petit.
Le Problème : C'est une « boucle autoréférentielle » qui combine la capacité d'observer les choses grandes et les choses petites d'une manière qui crée un paradoxe logique. C'est comme un serpent qui se mange la queue, mais la queue est faite du corps même du serpent.
La Leçon : Le robot possède une règle concernant l'Impredicativité dans Set. Il dit : « Vous pouvez être autoréférentiel avec des affirmations vraies/fausses simples, mais vous ne pouvez pas mélanger cela avec des types grands et complexes. » Ce piège prouve que si le robot autorisait ce mélange, il serait impossible de maintenir la cohérence du système.

La Grande Image : Pourquoi cela compte

L'article soutient que nous ne devrions pas considérer ces quatre fichiers comme des « mathématiques ratées ». Au contraire, nous devrions les voir comme la preuve du succès du robot.

Spécification Négative : Imaginez ces fichiers comme une affiche « Recherché » pour un criminel. Le criminel est l'« Incohérence ». L'affiche ne montre pas le criminel ; elle montre les exactes conditions sous lesquelles le criminel apparaîtrait.
La Frontière : Le robot (Rocq) a tracé trois lignes invisibles dans le sable :
1. Limites de Taille : Vous ne pouvez pas mettre une boîte à l'intérieur d'une boîte de la même taille.
2. Limites de Choix : Vous ne pouvez pas utiliser un choix simple pour forcer une vérité complexe.
3. Limites de Réflexion : Vous ne pouvez pas mélanger des autoréférences simples avec des types complexes.

À chaque fois qu'un utilisateur tente de construire une structure qui franchit l'une de ces lignes, le robot l'arrête. Ces quatre fichiers sont la preuve que le robot fait exactement ce pour quoi il a été conçu : refuser de construire quoi que ce soit qui finirait par s'effondrer.

En résumé, l'article dit : « Nous avons essayé de briser le système avec ces quatre astuces ingénieuses. Le système a dit "Non". Ce "Non" est la partie la plus importante du système, car il maintient tout en sécurité. »

Résumé technique : quatre paradoxes et un assistant de preuve

Énoncé du problème
L'article traite des limites fondamentales du Calcul des Constructions Inductives (CIC), la théorie des types qui sous-tend l'assistant de preuve Rocq (anciennement Coq). Bien que la cohérence du CIC soit bien établie, les décisions de conception spécifiques qui empêchent l'incohérence — en particulier concernant l'imprédicativité, les contraintes d'univers et l'élimination large — sont souvent traitées comme des contraintes d'ingénierie abstraites. La bibliothèque coq-paradoxes, distribuée avec Rocq, contient quatre dérivations mécanisées de False (Burali-Forti, Diaconescu, Reynolds et Hurkens) qui reposent sur des hypothèses rejetées par le noyau Rocq. Le problème central consiste à interpréter ces dérivations non pas comme de simples curiosités historiques ou des incohérences isolées, mais comme une « spécification négative » qui délimite précisément où le noyau doit tracer ses limites pour maintenir la validité.

Méthodologie
L'article procède à une lecture attentive du code source au sein de la bibliothèque coq-paradoxes, en analysant spécifiquement quatre fichiers : BuraliForti.v, diaconescu.v, Reynolds.v et Hurkens_Set.v. La méthodologie comprend :

Déconstruction de la machinerie partagée : Analyse de Logics.v pour comprendre le prédicat d'accessibilité (ACC) et l'infrastructure de bonne fondation utilisés par plusieurs paradoxes.
Traçage des dérivations : Suivi des étapes logiques dans chaque fichier pour identifier l'hypothèse spécifique (par exemple, un type universel de relations, un principe de choix, ou une injection de Prop vers une seule proposition) qui mène à une contradiction.
Mise en correspondance avec les rejets du noyau : Corrélation du point de contradiction dans la formalisation avec le mécanisme spécifique du noyau Rocq (arithmétique des univers, règles d'élimination ou vérifications d'imprédicativité) qui empêche la construction de se compiler.
Synthèse des décisions de conception : Agrégation des résultats pour extraire trois conditions limites unifiées régissant le comportement du noyau.

Contributions et résultats clés

L'article analyse quatre paradoxes spécifiques, démontrant comment chacun expose une vulnérabilité distincte dans la théorie des types si certaines décisions de conception étaient modifiées :

Paradoxe de Burali-Forti (BuraliForti.v) :
- Mécanisme : Suppose un type universel de relations $A_0$ et une injection $i_0$ qui mappe les relations vers des éléments de $A_0$ . Cela permet la construction d'un « ordinal de tous les ordinaux » ( $\Omega$ ) qui s'incorpore lui-même.
- Rejet par le noyau : Le paradoxe repose sur l'instanciation de $A_0$ par lui-même. Le noyau Rocq impose une stratification stricte des univers ( $Type_j < Type_i$ ) pour empêcher un type de contenir son propre image. La construction déclenche une erreur d'« Incohérence des univers » car le niveau d'univers requis pour le type interne doit être au moins aussi grand que le type externe, violant ainsi les contraintes cumulatives du noyau.
- Résultat : Établit la nécessité de contraintes de hiérarchie des univers pour empêcher les définitions de types autoréférentiels menant à des contradictions de point fixe.
Paradoxe de Diaconescu (diaconescu.v) :
- Mécanisme : Utilise une version typée de l'Axiome du Choix (Tchoice) sur une relation d'équivalence sur bool définie par une proposition $P$ . La fonction de choix $f: bool \to bool$ est utilisée pour décider $P$ en comparant $f(\text{true})$ et $f(\text{false})$ .
- Rejet par le noyau : L'argument extrait une décision computationnelle (une fonction dans Set) d'une preuve existentielle dans Prop. Cela constitue une « élimination large » de Prop vers Set.
- Résultat : Démontre que permettre l'Axiome du Choix dans Set (ou l'élimination large de Prop vers Set) force la Loi du Milieu Exclu (LEM) dans le système constructif. Le noyau restreint l'élimination large pour empêcher cette importation de logique classique dans la couche computationnelle.
Paradoxe de Reynolds (Reynolds.v) :
- Mécanisme : Reformule le résultat de Reynolds selon lequel le Système F n'a pas de modèle ensembliste. Il suppose une injection $I: Prop \to Heyt$ (où $Heyt$ est une seule proposition) et construit une pré-algèbre initiale (encodage de Church) pour un foncteur $\Phi$ . En utilisant le théorème du point fixe de Lawvere, il dérive un point fixe pour la négation, menant à False.
- Rejet par le noyau : La construction repose sur l'imprédicativité de Prop (quantification sur toutes les propositions dans Prop). Cependant, le paradoxe nécessite une injection de Prop vers une seule proposition, ce que le noyau rejette pour des raisons d'univers avant que la contradiction logique ne puisse être atteinte.
- Résultat : Met en évidence le rôle de l'imprédicativité dans Prop. Bien que Prop soit imprédicatif, le noyau empêche les injections structurelles spécifiques qui permettraient à l'argument diagonal de Cantor de faire effondrer l'univers des propositions.
Paradoxe de Hurkens (Hurkens_Set.v) :
- Mécanisme : Une adaptation de la simplification par Hurkens du paradoxe de Girard. Il suppose une rétraction entre Prop et bool (via la double négation) et utilise l'imprédicativité de Set (si activée) combinée à l'élimination large pour construire une relation bien fondée autoréférentielle menant à False.
- Rejet par le noyau : Le paradoxe nécessite à la fois l'imprédicativité dans Set et l'élimination large (extraction de booléens à partir de contenu propositionnel). Le noyau Rocq par défaut maintient Set prédicatif et restreint l'élimination large depuis Prop.
- Résultat : Montre que la combinaison de l'imprédicativité et de l'élimination large dans Set est incohérente avec la logique classique (LEM). La décision du noyau de maintenir Set prédicatif et de restreindre l'élimination est la mesure de protection.

Portée et affirmations

L'article soutient que le paquet coq-paradoxes sert de spécification négative du noyau Rocq. Plutôt que de simplement lister des incohérences, le paquet fournit une preuve formelle par exemple échoué de la validité du noyau.

Trois conditions limites : L'article synthétise les quatre paradoxes en trois décisions de conception spécifiques imposées par le noyau :
1. Hiérarchie des univers : Empêche les types de se quantifier sur eux-mêmes d'une manière qui crée des points fixes (Burali-Forti).
2. Placement de l'imprédicativité : Confiner la quantification imprédicative à Prop (et optionnellement à Set avec des réserves), empêchant les contradictions de Reynolds et Hurkens.
3. Discipline de l'élimination large : Restreint l'extraction de contenu computationnel (comme bool ou des fonctions dans Set) à partir de preuves propositionnelles, empêchant les contradictions de Diaconescu et Hurkens.
Rôle méta-mathématique : L'article affirme que le paquet est une pièce unique de méta-mathématiques écrite à l'intérieur du système qu'il documente. Il ne prouve pas des théorèmes pour application, mais prouve l'insatisfaisabilité d'hypothèses spécifiques. Le « refus » du noyau est montré comme une conséquence de politiques uniformes (arithmétique des univers, règles d'élimination) plutôt que de correctifs ad hoc.
Conclusion : La portée réside dans la démonstration que le refus du noyau Rocq de compiler ces constructions n'est pas arbitraire, mais constitue le mécanisme structurel précis requis pour maintenir la cohérence du CIC. Le paquet valide que les décisions de conception du noyau sont prises pour les « bonnes raisons », traçant efficacement la frontière du système de l'extérieur vers l'intérieur.