Encyclopedia > Presburger arithmetic

  Article Content

Presburger arithmetic

Presburger arithmetic is the first-order theory of the natural numbers with addition. It is not as powerful as the Peano axioms because multiplication is omitted. In fact, M. Presburger[?] proved in 1929 that there is an algorithm which decides for any given statement in Presburger arithmetic whether it is true or not. No such algorithm exists for general arithmetic as a consequence of the negative answer to the Entscheidungsproblem. Furthermore, Presburger proved that his arithmetic is consistent (does not contain contradictions) and complete (every statement can either be proven or disproven). Again, this is false for general arithmetic; this is the content of Gödel's incompleteness theorem.

Presburger arithmetic is an interesting example in computational complexity theory and computation because Fischer and Rabin proved in 1974 that every algorithm which decides the truth of Presburger statements has a runtime of at least 2^(2^(cn)) for some constant c. Here, n is the length of the Presburger statement. Hence, the problem is one of the few that provably need more than polynomial run time.

In the formal description of the theory, we use the object constants 0 and 1, the function constant +, and the predicate constant =. The axioms are:

  1. x : ¬ (0 = x + 1)
  2. xy : ¬ (x = y) ⇒ ¬ (x + 1 = y + 1)
  3. x : x + 0 = x
  4. xy : (x + y) + 1 = x + (y + 1)
  5. This is an axiom scheme consisting of infinitely many axioms. If P(x) is any formula involving the constants 0, 1, +, = and a single free variable x, then the following formula is an axiom:   ( P(0) ∧ ∀ x : P(x) ⇒ P(x + 1) ) ⇒ ∀ x : P(x)

Concepts such as divisibility of prime number cannot be formalized in Presburger arithmetic. Here is a typical theorem that can be proven from the above axioms:

xy : ( (∃ z : x + z = y + 1) ⇒ (∀ z : ¬ (((1 + y) + 1) + z = x) ) )
It says that if xy + 1, then y + 2 > x.


References:
  • M. Presburger: "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". In Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa, 1929, pp.92-101
  • M.J. Fischer, M.O.Rabin: "Super-Exponential Complexity of Presburger Arithmetic". Proceedings of the SIAM-AMS Symposium in Applied Mathematics, 1974, vol. 7, pp.27-41



All Wikipedia text is available under the terms of the GNU Free Documentation License

 
  Search Encyclopedia

Search over one million articles, find something about almost anything!
 
 
  
  Featured Article
1399

... 1340s 1350s 1360s 1370s 1380s - 1390s - 1400s 1410s 1420s 1430s 1440s Years: 1394 1395 1396 1397 1398 - 1399 - 1400 1401 1402 1403 1404 Events Henry IV ...