Arithmétique de Presburger

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Pressburger.

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 expressive que l'arithmétique de Peano, mais la rend également complète et décidable (elle admet l'élimination des quantificateurs), contrairement à cette dernière.

Mojżesz Presburger a démontré en 1929 que son arithmétique, qui est cohérente[1], est 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 implémentations qui fonctionnent bien.

Notes et références[modifier | modifier le code]

  1. On ne peut démontrer l'absurde, ou encore il existe un modèle, en fait le modèle standard des entiers naturels.
  2. Toute proposition est démontrable ou sa négation est démontrable.