💻 computer science

On existential Büchi arithmetic in two coprime bases

Cet article établit la décidabilité du fragment existentiel de l'arithmétique de Presburger étendue avec des prédicats de Büchi pour deux bases premières entre elles en fournissant un argument d'élimination des quantificateurs.

Auteurs originaux : Joris Nieuwveld

Publié 2026-08-26

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Joris Nieuwveld

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

Les mathématiques sont depuis longtemps fascinées par les règles qui régissent les nombres, plus précisément par la manière dont nous pouvons les décrire en utilisant des opérations simples comme l'addition et l'ordre. Depuis près d'un siècle, un système connu sous le nom d'arithmétique de Presburger sert de fondement fiable à ce travail. Il permet de poser des questions sur les entiers en utilisant uniquement l'addition et le concept de « moins que », et grâce à une méthode développée en 1929, nous savons que toute question posée dans ce système peut recevoir une réponse par un oui ou un non définitif. Cependant, ce système est limité ; il ne peut pas gérer la multiplication, qui est la clé ouvrant toute la complexité de l'arithmétique. Lorsqu'on ajoute la multiplication, le système devient si puissant qu'aucun algorithme ne peut jamais garantir une réponse à toutes les questions possibles.

Pour combler le fossé entre le monde simple de l'addition et le monde complexe de la multiplication, les chercheurs ont exploré l'ajout d'outils spécifiques et limités au système. L'un de ces outils est un prédicat qui identifie la plus grande puissance d'un nombre spécifique qui divise un autre nombre. Par exemple, si nous regardons le nombre 12, la plus grande puissance de 2 qui le divise est 4, tandis que la plus grande puissance de 3 qui le divise est 3. Cet outil, souvent appelé prédicat de Büchi, permet de parler des puissances de nombres sans introduire pleinement la multiplication. La question centrale depuis des décennies est de savoir ce qui se passe lorsque nous essayons d'utiliser deux de ces outils à la fois, spécifiquement pour deux bases différentes qui ne partagent pas de relation multiplicative simple. Si nous essayons de décrire des nombres en utilisant simultanément les puissances de deux bases différentes, le système reste-t-il soluble, ou s'effondre-t-il dans le chaos insoluble de la multiplication complète ?

Un chercheur de l'Université d'Oxford, Joris Nieuwveld, a désormais apporté une réponse définitive pour un cas spécifique et important de ce problème. L'étude se concentre sur deux bases qui sont premières entre elles, c'est-à-dire qu'elles n'ont aucun facteur commun autre que un, comme 2 et 3. Bien que des travaux antérieurs aient montré que l'utilisation de deux telles bases rend généralement le système indécidable, Nieuwveld a démontré que si nous restreignons nos questions à une forme spécifique et plus simple — demandant seulement si une solution existe sans exiger une description complète de toutes les solutions possibles — le système reste soluble. L'article prouve que pour ces bases premières entre elles, il existe une méthode fiable pour déterminer si une proposition donnée est vraie ou fausse, maîtrisant ainsi un problème qui était auparavant considéré comme insoluble dans cette configuration spécifique.

Le chemin vers cette découverte a nécessité de naviguer dans un paysage de croissance exponentielle et de contraintes modulaires. Le chercheur a commencé par traduire les questions logiques complexes en un système d'inégalités et d'équations modulaires impliquant les puissances des deux bases. Imaginez ces puissances comme des variables qui peuvent croître incroyablement vite, et les équations comme des règles qui dictent comment elles se rapportent les unes aux autres. Le défi était de déterminer s'il existe une combinaison de ces nombres qui satisfait toutes les règles simultanément. L'approche a consisté à décomposer le problème en couches gérables, en regroupant les variables selon la manière dont leurs tailles se rapportent les unes aux autres. En analysant la structure de ces couches, le chercheur a pu identifier quelles variables étaient étroitement liées et lesquelles pouvaient varier indépendamment.

Une partie cruciale de la solution reposait sur une compréhension profonde du comportement des nombres lorsqu'ils sont divisés par des puissances d'autres nombres. L'article utilise un théorème puissant de la théorie des nombres pour montrer que, sous certaines conditions, les restes de ces puissances suivent des modèles prévisibles. Cette prévisibilité a permis au chercheur de simplifier considérablement le problème. Au lieu d'essayer de résoudre pour chaque nombre possible, la méthode a réduit les possibilités infinies à un ensemble fini de cas pouvant être vérifiés. La preuve a montré que si les bases sont premières entre elles, les interactions entre leurs puissances sont suffisamment contraintes pour empêcher le système de devenir trop chaotique pour être résolu.

Le résultat est une clarification significative des limites de la décidabilité en arithmétique. Il confirme que si l'ajout de deux prédicats de Büchi mène généralement à un système insoluble, le fragment existentiel — la partie du système qui demande seulement l'existence d'une solution — reste décidable lorsque les bases sont premières entre elles. Cette découverte règle une question ouverte de longue date pour ce cas spécifique. L'article ne prétend pas avoir résolu le problème pour toutes les paires de bases possibles, particulièrement celles qui ne sont pas premières entre elles, où le comportement des restes devient beaucoup plus erratique et où les méthodes actuelles ne s'appliquent pas. Cependant, pour le cas des bases premières entre elles, le travail fournit une preuve complète et rigoureuse qu'une procédure de décision existe.

Ce travail est important car il affine notre compréhension de la limite entre ce qui peut être calculé et ce qui ne peut pas l'être. Dans le domaine plus large de la logique et de l'informatique, connaître les limites de ce qui peut être décidé est essentiel pour concevoir des systèmes qui vérifient les logiciels, vérifient les preuves mathématiques et modélisent des processus complexes. En montrant qu'une extension naturelle et spécifique de l'arithmétique reste soluble sous certaines conditions, l'article ajoute une pièce précise au puzzle de la logique mathématique. Il démontre que même dans des systèmes qui semblent être sur le point de devenir trop complexes à gérer, il existe encore des îlots d'ordre qui peuvent être cartographiés et compris, à condition de les observer avec les bons outils et le bon niveau de restriction.

Résumé Technique : Sur l'arithmétique de Büchi existentielle dans deux bases coprimes

Énoncé du problème
L'article traite de la décidabilité du fragment existentiel de la logique du premier ordre sur les entiers, étendue par l'ordre, l'addition et deux prédicats de Büchi, notée $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ . Ici, $V_z(x, y)$ est vrai si et seulement si $y$ est la plus grande puissance de $z$ divisant $x$ .

Le contexte est établi par Villemaire (1992), qui a prouvé que la théorie complète du premier ordre $\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ est indécidable lorsque $\alpha$ et $\beta$ sont multiplicativement indépendants, car la structure peut encoder la multiplication. Des recherches ultérieures par Hieronymi et Schulz (2021) ont montré que le remplacement des prédicats de Büchi par des prédicats de puissance plus faibles ( $\alpha^\mathbb{N}, \beta^\mathbb{N}$ ) produit également une théorie indécidable. Cependant, Karimov et al. (2025) ont démontré que le fragment existentiel de la théorie avec les prédicats de puissance est décidable pour des bases multiplicativement indépendantes.

Le problème ouvert abordé dans cet article est de savoir si le fragment existentiel reste décidable lorsque les prédicats sont les prédicats de Büchi plus forts ( $V_\alpha, V_\beta$ ) plutôt que de simples ensembles de puissances. L'auteur résout cette question spécifiquement pour le cas où les bases $\alpha$ et $\beta$ sont coprimes.

Méthodologie
La preuve procède via un argument d'élimination de quantificateurs qui transforme une formule existentielle en un système d'inégalités linéaires et de contraintes modulaires impliquant des puissances de $\alpha$ et de $\beta$ . La méthodologie repose sur plusieurs outils mathématiques clés et réductions structurelles :

Réduction en systèmes d'inégalités :
L'auteur réduit d'abord la formule existentielle à un système impliquant des « variables de pure puissance » ( $z^n$ ) et des « variables de puissance linéaires » ( $x \cdot z^n$ ). Ce système consiste en des inégalités linéaires ( $Ax > v$ ) et des contraintes modulaires, certaines avec des modules constants et d'autres avec des modules variables (de la forme $d \cdot z^n$ ).
Décomposition structurelle (Niveaux et Famille de Base) :
Pour gérer la complexité des variables, l'auteur partitionne les variables en « niveaux » basés sur leurs magnitudes relatives. Les variables d'un même niveau ont des ratios bornés par une constante, tandis que les variables de niveaux différents peuvent avoir des ratios arbitrairement grands.
- Niveaux : Définis via le cône de récession du polyèdre $Ax > v$ .
- Famille de Base (Bottom Family) : Un sous-ensemble de variables (spécifiquement celles ayant de « petits coefficients ») qui sont traitées ensemble. L'auteur définit une « famille de base » telle que la projection du polyèdre sur ces variables n'est pas « mince » (c'est-à-dire non bornée dans une direction linéaire spécifique).
Réduction itérative et normalisation :
Le cœur de l'algorithme consiste à réduire le système pour satisfaire une liste spécifique de propriétés (Propriétés 1–4c). Ces propriétés garantissent que :
- Les variables sont ordonnées strictement ( $x_1 > \dots > x_t > 0$ ).
- Le polyèdre n'est pas mince.
- Les contraintes modulaires avec des modules variables sont gérées de telle sorte que la base du module ne se trouve pas dans la famille de base.
- Les sous-espaces orthogonaux des niveaux satisfont des conditions de non-dégénérescence spécifiques concernant les bases exponentielles.
L'obtention de ces propriétés implique l'application du théorème de Baker (sur les formes linéaires en logarithmes) pour borner les exposants et du théorème de Kronecker sur l'approximation diophantienne pour assurer la densité des ratios.
Gestion des contraintes modulaires :
Une contribution technique critique est la gestion des contraintes modulaires avec des modules variables ( $x \equiv c \pmod{z^n}$ ). L'auteur utilise le Lemme 33, qui repose sur la coprimalité de $\alpha$ et $\beta$ . Ce lemme stipule que l'ensemble des résidus $\{\beta^n \pmod{\alpha^m}\}$ se stabilise dans sa structure pour de grands $m$ . Cela permet à l'auteur de « gonfler » les exposants, convertissant ainsi efficacement les contraintes à module variable en contraintes à module constant (ou en contraintes avec périodicité fixe) en changeant l'échelle des variables.
Élimination des quantificateurs :
Une fois le système normalisé et les modules fixés (ou réduits à des cas constants), l'auteur applique un argument de relèvement (lifting). Il démontre que si le système est satisfaisable, il existe une solution où les variables en dehors de la famille de base sont suffisamment grandes. Les variables restantes (dans la famille de base) sont traitées comme des entiers linéaires au sein de classes modulaires spécifiques. En éliminant ces variables linéaires, le système est réduit à un ensemble strictement plus petit de variables, menant finalement à une décision sans quantificateurs.

Contributions clés et résultats

Théorème principal : L'article prouve que pour des entiers coprimes $\alpha, \beta \ge 2$ , le fragment existentiel $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ est décidable.
Généralisation des travaux antérieurs : Ce résultat étend le résultat de décidabilité de Karimov et al. (qui s'appliquait aux prédicats de puissance $\alpha^\mathbb{N}, \beta^\mathbb{N}$ ) aux prédicats de Büchi $V_\alpha, V_\beta$ plus expressifs, sous la condition plus forte de coprimalité.
Lemmes techniques : Le papier fournit des lemmes spécifiques (par exemple, le Lemme 33) décrivant la structure des puissances modulo les puissances de bases coprimes, qui sont essentiels pour la réduction des contraintes à module variable.
Construction algorithmique : La preuve est constructive, fournissant une méthode pour calculer les bornes, les partitions et les substitutions nécessaires pour éliminer les quantificateurs.

Signification et limites
L'article prétend régler la question de la décidabilité pour le fragment existentiel de l'expansion originale de Villemaire pour les bases coprimes. L'auteur note explicitement que son recours à la coprimalité est une contrainte significative.

Dépendance à la coprimalité : La preuve utilise la coprimalité deux fois : une fois dans l'application du théorème de Baker (Lemme 12) et, plus crucialement, dans le Lemme 33 concernant la structure de $\beta^n \pmod{\alpha^m}$ . L'auteur affirme que pour des bases multiplicativement indépendantes mais non coprimes, l'ensemble des résidus se comporte de manière plus irrégulière (croissance linéaire plutôt que stabilisation), et il ne sait pas comment contourner ce problème.
Portée : Le résultat est spécifique au fragment existentiel. La théorie complète reste indécidable.
Directions futures : L'auteur discute de l'extension de cela à plus de deux prédicats (par exemple, trois prédicats de puissance), ce qui nécessiterait probablement la conjecture de Schanuel pour gérer l'indépendance linéaire des logarithmes. Il note également que le problème pour des bases générales multiplicativement indépendantes (non coprimes) reste ouvert et nécessite probablement de nouvelles idées, possiblement impliquant des versions $p$ -adiques du théorème de Baker.

En résumé, l'article établit une frontière de décidabilité pour l'arithmétique de Büchi existentielle, comblant l'écart entre les prédicats de puissance et les prédicats de Büchi complets, tout en reconnaissant explicitement que le cas général des bases multiplicativement indépendantes demeure un défi ouvert.

Articles similaires