Presburger arithmetic

Presburger arithmeticMathworldPlanetmath is a weakened form of arithmeticPlanetmathPlanetmath which includes the structureMathworldPlanetmath , the constant 0, the unary function S, the binary function +, and the binary relationMathworldPlanetmath <. Essentially, it is Peano arithmeticMathworldPlanetmathPlanetmath without multiplicationPlanetmathPlanetmath.

The axioms are:

  1. 1.


  2. 2.


  3. 3.


  4. 4.


  5. 5.

    For each first order formulaMathworldPlanetmath P(x), P(0)x[P(x)P(x+1)]xP(x)

Presburger arithmetic is decidable, but is consequently very limited in what it can express.

Title Presburger arithmetic
Canonical name PresburgerArithmetic
Date of creation 2013-03-22 12:51:11
Last modified on 2013-03-22 12:51:11
Owner Henry (455)
Last modified by Henry (455)
Numerical id 8
Author Henry (455)
Entry type Definition
Classification msc 03B10
Related topic PeanoArithmetic