Editing Presburger arithmetic (section)

==Overview==
The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition.

In this language, the axioms of Presburger arithmetic are the [[universal closure]]s of the following:
# ¬(0 = ''x'' + 1)
# ''x'' + 1 = ''y'' + 1 → ''x'' = ''y''
# ''x'' + 0 = ''x''
# ''x'' + (''y'' + 1) = (''x'' + ''y'') + 1
# Let ''P''(''x'') be a [[first-order logic|first-order formula]] in the language of Presburger arithmetic with a  free variable ''x'' (and possibly other free variables). Then the following formula is an axiom:{{pb}}(''P''(0) &and; ∀''x''(''P''(''x'') → ''P''(''x'' + 1))) → ∀''y'' ''P''(''y'').

(5) is an [[axiom schema]] of [[Mathematical Induction|induction]], representing infinitely many axioms. These cannot be replaced by any finite number of axioms, that is, Presburger arithmetic is not finitely axiomatizable in first-order logic.{{sfn|Zoethout|2015|p=8|loc=Theorem 1.2.4.}}

Presburger arithmetic can be viewed as a [[First-order logic#First-order theories, models, and elementary classes|first-order theory]] with equality containing precisely all consequences of the above axioms. Alternatively, it can be defined as the set of those sentences that are true in the [[Interpretation (logic)#Intended interpretations|intended interpretation]]: the structure of non-negative integers with constants 0, 1, and the addition of non-negative integers.

Presburger arithmetic is designed to be complete and decidable. Therefore, it cannot formalize concepts such as [[divisibility]] or [[primality]], or, more generally, any number concept leading to multiplication of variables. However, it can formulate individual instances of divisibility; for example, it proves "for all ''x'', there exists ''y'' : (''y'' + ''y'' = ''x'') ∨ (''y'' + ''y'' + 1 = ''x'')". This states that every number is either even or odd.