# Arithmétique de Presburger

En logique mathématique, l'arithmétique de Presburger est la théorie du premier ordre des nombres entiers naturels munis de l'addition. Elle a été introduite en 1929 par Mojżesz Presburger. Il s'agit de l'arithmétique de Peano sans la multiplication, c’est-à-dire avec seulement l'addition, en plus du zéro et de l'opération successeur. Contrairement à l'arithmétique de Peano, l'arithmétique de Presburger est décidable. Cela signifie qu'il existe un algorithme qui détermine si un énoncé du langage de l'arithmétique de Presburger est démontrable à partir des axiomes de l'arithmétique de Presburger.

## Définition

La signature du langage de l'arithmétique de Presburger contient les symboles de constantes 0 et 1, le symbole de fonction binaire +. L'arithmétique est définie par les axiomes suivants :
* ∀x, ¬(0 = x + 1)
* ∀x,∀y, x + 1 = y + 1 → x = y
* ∀x, x + 0 = x
* ∀x, ∀y, x + (y + 1) = (x + y) + 1
* Pour toute formule P(x, y$_1$, …, y$_n$) du premier-ordre sur le langage de l'arithmétique de Presburger avec x, y$_1$, …, y$_n$ comme variables libres, la formule suivante est un axiome : ∀y$_1$…∀y$_n$ [(P(0, y$_1$, …, y$_n$) ∧ ∀x(P(x, y$_1$, …, y$_n$) → P(x + 1, y$_1$, …, y$_n$))) → ∀y P(y, y$_1$, …, y$_n$)].
(5) est le schéma d'induction et c'est un ensemble infini d'axiomes. On peut montrer que l'arithmétique de Presburger n'est pas finiment axiomatisable en logique du premier ordre.

## Propriétés

Mojżesz Presburger a démontré en 1929 que son arithmétique, qui est cohérente, est complète$^,$. Comme une théorie axiomatique récursivement axiomatisable et complète est décidable, on en déduit l'existence d'un algorithme qui décide, étant donné une proposition du langage de l'arithmétique de Presburger, si celle-ci est démontrable ou non.
Contrairement à l'arithmétique de Presburger, l'arithmétique de Peano n'est pas complète en vertu du théorème d'incomplétude de Gödel. L'arithmétique de Peano n'est pas décidable (voir problème de la décision).

## Algorithmes

Considérons ici le problème de décision suivant : décider si une formule de l'arithmétique de Presburger est vraie. En 1974, Michael J. Fisher et Michael O. Rabin ont démontré que ce problème de décision a une complexité temporelle intrinsèque doublement exponentielle. En d'autres termes, le problème de décision est 2EXPTIME-dur : il fait partie des problèmes les plus difficiles de la classe de complexité 2EXPTIME, qui est la classe des problèmes décidables en temps doublement exponentiel.
Il existe une procédure de décision non élémentaire reposant sur la théorie des automates finis.
Oppen en 1978 a donné un algorithme triplement exponentiel, c'est-à-dire que le problème de savoir si une formule de l'arithmétique de Presburger est vraie est dans 3EXPTIME, la classe des problèmes décidables en temps triplement exponentiel.
Berman en 1980 a donné un résultat plus précis de théorie de la complexité en utilisant des machines alternantes : l'arithmétique de Presburger est complète pour la classe des problèmes décidés en temps 2$^{2nO(1)}$ et n alternations, où le nombre n est la taille de la formule à vérifier. Cette classe contient 2EXPTIME et est contenu dans 3EXPTIME.
Le solveur SMT Z3 implémente l'arithmétique de Presburger. L'assistant de preuve Rocq fournit la stratégie omega.

## Comparaison avec d'autres arithmétiques

L'arithmétique de Peano est définie sur le langage de l'arithmétique de Presburger avec en plus un symbole de fonction binaire × dont l'interprétation intuitive est la multiplication. L'arithmétique de Peano contient des axiomes supplémentaires. L'arithmétique de Robinson, elle, ne contient pas le schéma d'induction.