🔢 mathematics

Generalized Decidability via Brouwer Trees

Cet article introduit un cadre dans la théorie des types homotopiques qui généralise la décidabilité en utilisant les ordinaux de Brouwer pour établir une hiérarchie de propositions $\alpha$ -décidables, caractérisant leurs propriétés de clôture sous les opérations logiques et les quantificateurs, l'ensemble des résultats étant formalisé dans Cubical Agda.

Auteurs originaux : Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

Publié 2026-07-10

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

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 êtes un détective essayant de résoudre un mystère. Dans le monde de l'informatique, nous classons habituellement les mystères dans trois catégories : Décidable (nous pouvons trouver la réponse rapidement), Semi-décidable (nous pouvons trouver la réponse si c'est "oui", mais si c'est "non", nous pourrions attendre éternellement) et Indécidable (nous ne pouvons pas le résoudre du tout).

Mais que se passerait-il s'il existait des mystères qui sont "plus" semi-décidables que d'autres ? Et si certains "oui" prenaient un peu plus de temps à être trouvés que d'autres, tout en ne prenant pas pour autant une éternité ?

C'est exactement ce que Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh et Fredrik Nordvall Forsberg explorent dans leur nouvel article. Ils suggèrent une façon de mesurer précisément combien de temps il faut pour trouver une réponse "oui", en utilisant un type spécial de système de nombres appelé ordinaux d'arbres de Brouwer. Voyez cela non pas comme des nombres réguliers comme 1, 2, 3, mais comme une échelle magique de paliers de temps qui va bien au-delà de l'infini.

L'échelle magique du temps

Dans leur cadre, ils ne se contentent pas de dire "c'est soluble". Ils disent : "C'est $\alpha$ -décidable", où $\alpha$ est un barreau spécifique de leur échelle magique.

Niveau 1 (Décidable) : Si un problème est 1-décidable, cela signifie que vous pouvez trouver la réponse (ou prouver qu'elle est impossible) en un nombre fini d'étapes. C'est comme vérifier si un nombre est premier ; vous comptez simplement, et vous finissez par savoir avec certitude.
Niveau $\omega + 1$ (Semi-décidable) : Si un problème est $(\omega + 1)$ -décidable, cela signifie que si la réponse est "oui", vous la trouverez en $\omega$ étapes. Mais $\omega$ n'est pas un nombre normal ; il représente le fait de "compter pour toujours". Ainsi, si la réponse est "oui", vous la trouverez éventuellement, mais si la réponse est "non", vous pourriez continuer à compter éternellement sans jamais vous arrêter. C'est la définition classique de "semi-décidable".

Les auteurs prouvent que ce nouveau système s'ajuste parfaitement à l'ancien. Si vous avez un problème qui est "décidable", il se situe sur le barreau 1. S'il est "semi-décidable", il se situe sur le barreau $\omega + 1$ . Mais la magie réside dans le fait qu'ils peuvent désormais parler de barreaux entre ces deux-là, ou bien au-dessus d'eux.

Le mystère des nombres premiers jumeaux

Pour montrer comment cela fonctionne, ils utilisent un célèbre casse-tête mathématique : la Conjecture des nombres premiers jumeaux. Celle-ci demande : "Existe-t-il toujours une paire de nombres premiers (comme 3 et 5, ou 11 et 13) qui sont séparés par seulement deux nombres, peu importe jusqu'où l'on compte ?"

Vérifier si une paire spécifique existe est facile (décidable).
Vérifier si n'importe quelle paire existe au-dessus d'un certain nombre est semi-décidable (vous continuez simplement à chercher ; si vous en trouvez une, vous vous arrêtez).
Mais la grande question est de savoir si cela est vrai pour chaque nombre.

Les auteurs montrent que cette question spécifique est $\omega^2$ -décidable. Imaginez que $\omega$ est une seule ligne infinie d'étapes. $\omega^2$ est comme si vous aviez un nombre infini de ces lignes de $\omega$ empilées les unes sur les autres. Cela signifie que si un contre-exemple à la Conjecture des nombres premiers jumeaux existe, vous pourriez le trouver, mais cela pourrait prendre un laps de temps équivalent à parcourir une pile infinie de lignes infinies.

Ils ont également examiné ce qui se passe lorsque vous combinez ces problèmes :

ET : Si vous avez deux problèmes qui sont $\alpha$ -décidables, leur "ET" (les deux doivent être vrais) est aussi $\alpha-décidable$ . C'est comme cocher deux cases ; si vous pouvez vérifier les deux dans le même intervalle de temps, c'est bon.
OU : Ceci est plus délicat. Si vous avez deux problèmes, leur "OU" (l'un ou l'autre est vrai) n'est garanti d'être décidable que si le limite de temps est suffisamment petit (spécifiquement, si le niveau est quelque chose comme $\omega \cdot k + n$ ). Si la limite de temps devient trop grande, le "OU" pourrait briser les règles de leur système.

Le problème du "Choix"

C'est ici que cela devient vraiment intéressant. Les auteurs ont découvert que si vous voulez combiner un nombre infini de problèmes "semi-décidables" (comme vérifier la Conjecture des nombres premiers jumeaux pour chaque nombre de départ), vous vous heurtez à un mur. Sans une règle mathématique spéciale appelée Choix dénombrable, vous ne pouvez pas prouver que le résultat combiné est semi-décidable.

En fait, ils ont prouvé que si vous pouviez prouver cela sans cette règle, cela briserait d'autres lois fondamentales de la logique. Ils suggèrent donc que pour que les combinaisons infinies fonctionnent de manière fluide, vous avez besoin de supposer le Choix dénombrable.

Cependant, ils ont également trouvé une solution de contournement ! Ils ont examiné un autre type de "semi-décidable" appelé Sierpiński-semi-décidable. C'est une version légèrement plus faible qui permet de combiner des listes infinies sans avoir besoin de la règle du Choix dénombrable. C'est comme avoir un type de lampe de poche différent qui ne brille pas aussi intensément que l'original, mais qui n'a pas besoin de pile (la règle du Choix) pour s'allumer.

Ce qu'ils n'ont pas résolu

Il est important de savoir ce que cet article ne fait pas. Les auteurs sont très clairs : ils n'ont pas résolu la Conjecture des nombres premiers jumeaux. Ils l'ont simplement utilisée comme un exemple de démonstration pour montrer comment leur nouveau système de mesure fonctionne.

Ils admettent également qu'ils ne connaissent pas encore la forme complète de leur échelle. Ils supposent que si vous avez un problème sur le barreau $\alpha$ et un autre sur le barreau $\beta$ , et que $\alpha$ est inférieur à $\beta$ , alors le problème sur $\alpha$ devrait également être soluble sur $\beta$ . Mais ils n'ont pas encore prouvé cela pour chaque barreau de l'échelle. C'est une "conjecture" (une hypothèse forte), pas un fait.

L'essentiel à retenir

Cet article suggère une nouvelle façon de parler de la difficulté de trouver une réponse "oui" en mathématiques et en informatique. Au lieu de simplement dire "nous pouvons la trouver" ou "nous ne pouvons pas", ils nous donnent une règle précise faite d'étapes infinies. Ils ont prouvé que cette règle fonctionne pour ce que nous connaissons déjà (décidable et semi-décidable), et ils l'ont utilisée pour mesurer des problèmes complexes comme la Conjecture des nombres premiers jumeaux, trouvant qu'ils se situent à une hauteur mesurable spécifique de $\omega^2$ .

Ils ont également montré que si leur règle est puissante, elle a des limites : combiner des listes infinies de problèmes nécessite une hypothèse spécifique (le Choix dénombrable), à moins de passer à un type de règle légèrement différent (la semi-décidabilité de Sierpiński).

Tout cela a été construit et vérifié à l'intérieur d'un programme informatique appelé Cubical Agda, qui agit comme un arbitre extrêmement strict pour s'assurer que chaque étape de leur logique est parfaite. Ainsi, bien que les idées soient nouvelles et passionnantes, la rigueur mathématique derrière elles est inattaquable.

Résumé Technique : Décidabilité Généralisée via les Arbres de Brouwer

Énoncé du Problème
En mathématiques constructives et en théorie de la calculabilité synthétique, la classification standard des propositions en « décidables », « semi-décidables » ou « indécidables » est souvent trop grossière. Par exemple, si la décidabilité de la primalité est claire, le statut de la conjecture des nombres premiers jumeaux (si une paire de nombres premiers jumeaux existe au-dessus de tout $n$ ) implique une structure de $\omega$ -nombreux sous-problèmes semi-décidables. Classiquement, cela pourrait être vu comme une limite de limites, mais les cadres constructifs nécessitent un moyen plus précis de mesurer la « durée » ou la complexité de la recherche de preuves. Les notions existantes d'ordinaux (par exemple, les formes normales de Cantor syntaxiques ou les relations bien fondées sémantiques) échouent à fournir une hiérarchie appropriée : les approches syntaxiques rendent toutes les comparaisons décidables (effondrant ainsi la hiérarchie), tandis que les approches sémantiques échouent souvent à rendre les comparaisons semi-décidables. Le présent article traite de la nécessité d'un cadre permettant de distinguer plus finement la décidabilité, spécifiquement pour caractériser les propositions qui nécessitent des étapes transfinies pour être vérifiées.

Méthodologie
Les auteurs travaillent au sein de la Théorie des Types Homotopiques (HoTT), en utilisant les ordinaux d'arbres de Brouwer ( $\text{Brw}$ ) comme fondement de leur hiérarchie. Ces ordinaux sont définis via un type inductif-inductif quotient (QIIT) contenant des constructeurs pour zéro, les successeurs et les limites de séquences strictement croissantes. Crucialement, le constructeur de limite n'accepte que des séquences strictement croissantes, ce qui garantit que la finitude est décidable tout en préservant la nature constructive de la théorie.

La définition centrale introduite est la $\alpha$ -décidabilité : une proposition $P$ est $\alpha$ -décidable s'il existe un ordinal $y$ tel que $P \leftrightarrow (\alpha \leq y)$ . Cette définition généralise les concepts existants :

La $1$-décidabilité (ou $\omega$ -décidabilité) correspond à la décidabilité standard.
La $(\omega + 1)$ -décidabilité (équivalente à la $\omega \cdot 2$ -décidabilité) correspond à la semi-décidabilité.

Les auteurs formalisent tous les résultats dans Cubical Agda, en exploitant le support natif pour les QIIT et l'univalence. Ils emploient des techniques spécifiques pour gérer la complexité de la définition de fonctions sur les QIIT, notamment en définissant d'abord des relations sur les constructeurs de points, puis en extrayant les fonctions plus tard afin d'éviter l'explosion combinatoire dans la gestion des constructeurs de chemins.

Contributions Clés et Résultats

Hiérarchie de la Décidabilité :
- L'article établit que la $\alpha$ -décidabilité généralise la décidabilité et la semi-décidabilité.
- Il est démontré que pour tout ordinal $\alpha$ , la $(\alpha+1)$ -décidabilité est équivalente à la $(\alpha+\omega)$ -décidabilité. Par conséquent, la hiérarchie peut être indexée efficacement par des ordinaux limites (ordinaux non-successeurs).
- Les auteurs prouvent que si $P$ est $\alpha$ -décidable et $Q$ est $\alpha$ -décidable, alors $P \land Q$ est $\alpha$ -décidable. Cela repose sur la construction d'une fonction de minimum binaire pour les non-successeurs, ce qui n'est pas généralement possible pour des ordinaux arbitraires sans impliquer le Principe de l'Omniscience Limitée (LPO).
Disjonction et Maxima :
- Bien que la conjonction soit close au même niveau, la disjonction binaire ne l'est pas pour un $\alpha$ arbitraire. Cependant, les auteurs prouvent que les propositions $(\omega \cdot k + n)$ -décidables sont closes sous la disjonction binaire. Cela nécessite la construction d'une fonction de maximum binaire relative aux ordinaux de la forme $\omega \cdot k$ .
- L'existence de maxima binaires globaux pour les non-successeurs est montrée comme impliquant le LPO, un tabou constructif.
Quantificateurs Comptables et Familles :
- Rencontres Comptables (Meets) : Pour une famille de propositions semi-décidables $P: \mathbb{N} \to \text{Prop}$ , la rencontre dénombrable $\forall i. P(i)$ est prouvée être $\omega^2$ -décidable. Ce résultat est appliqué à la conjecture des nombres premiers jumeaux, en la caractérisant comme $\omega^2$ -décidable.
- Jonctions Comptables (Joins) : La jonction dénombrable $\exists i. P(i)$ de propositions semi-décidables est montrée comme étant $(\omega \cdot 3)$ -décidable.
- Alternances de Quantificateurs : L'article analyse les formules avec alternance de quantificateurs. Pour une famille $P(n, m)$ telle que $P(n, m) \to P(n, m+1)$ , la proposition $\exists m. \forall n. P(n, m)$ est montrée comme étant $(\omega^2 + \omega)$ -décidable. Cela fournit une borne ordinale précise pour la recherche de contre-exemples à la conjecture des nombres premiers jumeaux.
Relation avec les Principes de Choix :
- Les auteurs étudient l'impact du Choix Dénombrable (AC). En supposant AC, la jonction dénombrable de propositions semi-décidables devient semi-décidable (c'est-à-dire que la $(\omega \cdot 3)$ -décidabilité s'effondre en $(\omega \cdot 2)$ -décidabilité).
- Cependant, même avec AC, les propositions $\omega^2$ -décidables ne s'effondrent pas en propositions semi-décidables, à moins que le Principe de Markov n'implique le LPO.
- L'article introduit la semi-décidabilité de Sierpiński (basée sur le type de Sierpiński, l'ordre partiel $\omega$ -complet libre) comme une notion alternative de semi-décidabilité qui est close sous les jonctions dénombrables sans supposer le Choix Dénombrable. Il est montré que la semi-décidabilité de Sierpiński est plus faible que la semi-décidabilité standard.

Signification et Revendications
Les auteurs positionnent ce travail comme la première étape vers une théorie de la décidabilité généralisée. Ils affirment fournir un cadre où la « durée » des algorithmes (dans un sens constructif et abstrait) peut être précisément spécifiée et prouvée en utilisant l'arithmétique des ordinaux.

L'article note modestement qu'il ne résout pas les problèmes ouverts comme la conjecture des nombres premiers jumeaux ; il fournit plutôt un langage formel pour décrire la complexité de tels problèmes. Il souligne que la hiérarchie de la décidabilité n'est pas entièrement comprise, notant spécifiquement qu'il reste une question ouverte de savoir si la $\alpha$ -décidabilité implique la $\beta$ -décidabilité pour tout $\alpha \leq \beta$ (bien que des résultats partiels soient fournis). Le travail laisse également ouvert la question de savoir si les arbres de Brouwer sont la notion d'ordinal optimale pour cette théorie ou si d'autres constructions d'ordinaux pourraient produire des hiérarchies différentes, potentiellement plus riches.

Tous les résultats sont rigoureusement formalisés dans Cubical Agda, garantissant que la nature constructive des preuves est maintenue et que les définitions des ordinaux et de leurs propriétés sont informatiquement saines au sein de la théorie des types.

L'échelle magique du temps

Le mystère des nombres premiers jumeaux

Le problème du "Choix"

Ce qu'ils n'ont pas résolu

L'essentiel à retenir

Articles similaires