Arithmétique de Presburger - Définition

L'arithmétique de Presburger est une théorie du premier ordre, dans le langage de l'arithmétique de Peano sans la multiplication, c’est-à-dire avec seulement l'addition (et éventuellement l'ordre), en plus du zéro et de l'opération successeur. L'axiomatisation est essentiellement la même que celle de l'arithmétique de Peano, moins les axiomes de la multiplication, et avec la différence essentielle que, si le schéma d'axiomes de récurrence semble s'énoncer de la même façon, il ne couvre plus que les formules du langage de l'arithmétique de Presburger, donc un ensemble de propriétés beaucoup moins riche. Cette restriction rend l'arithmétique de Presburger beaucoup moins puissante que l'arithmétique de Peano, mais la rend également complète et décidable, contrairement à cette dernière.

Mojzesz Presburger a démontré en 1929 que son arithmétique qui est cohérente^[1] et complète^[2]. Cela est impossible pour l'arithmétique de Peano, en vertu du théorème d'incomplétude de Gödel. 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, au vu d'une proposition du langage de l'arithmétique de Presburger, si celle-ci est démontrable ou non. Là encore, cela est impossible pour l'arithmétique de Peano (voir problème de la décision). En revanche, Michael J. Fisher et Michael O. Rabin ont démontré que le problème de la décision a une complexité intrinsèque doublement exponentielle, ce qui devrait rendre tout algorithme inefficace, mais en pratique il existe des implantations qui fonctionnent bien.