Presburger arithmetic is a weak arithmetic theory. It is consistent, complete, and decidable, but is not strong enough to form statements about multiplication. The decision problem of determining whether a given statement is a theorem of Presburger arithmetic is in a doubly exponential complexity class.
Definition[]
The language of Presburger arithmetic extends predicate calculus with a constant 0, unary operator S, binary operator +, and relation =. Its axioms are:
- \(\forall n: S(n) \neq 0\)
- \(\forall n \forall m: S(n) = S(m) \Rightarrow n = m\)
- \(\forall n: n + 0 = n\)
- \(\forall n \forall m: n + S(m) = S(n + m)\)
- For every first-order formula \(\varphi(n)\): \((\varphi(0) \wedge (\forall n: \varphi(n) \Rightarrow \varphi(S(n)))) \Rightarrow \forall m: \varphi(m)\).
Properties[]
As mentioned before, Presburger arithmetic is weak enough that it is not very useful as a general foundation for number theory. The fundamental theorem of arithmetic, for example, is arguably one of the most important results of number theory, but it is not expressible in the language of Presburger arithmetic.
The interest in the theory is that it is both consistent and complete. This does not violate Gödel's first incompleteness theorem, which only applies to theories with languages that can make statements about elementary arithmetic.
Presburger arithmetic is also decidable. Unlike its older siblings such as Robinson arithmetic and Peano arithmetic, there is an algorithm that determines whether a given statement is a theorem. Fischer and Rabin showed that the decision problem is in a doubly exponential complexity class; that is, there is a positive constant c such that for every non-deterministic procedure that decides the problem, for all sufficiently large n the procedure takes more than \(2^{2^{cn}}\) steps.[1]
Sources[]
See also[]
Basics: cardinal numbers · ordinal numbers · limit ordinals · fundamental sequence · normal form · transfinite induction · ordinal notation · Absolute infinity
Theories: Robinson arithmetic · Presburger arithmetic · Peano arithmetic · KP · second-order arithmetic · ZFC
Model Theoretic Concepts: structure · elementary embedding
Countable ordinals: \(\omega\) · \(\varepsilon_0\) · \(\zeta_0\) · \(\eta_0\) · \(\Gamma_0\) (Feferman–Schütte ordinal) · \(\varphi(1,0,0,0)\) (Ackermann ordinal) · \(\psi_0(\Omega^{\Omega^\omega})\) (small Veblen ordinal) · \(\psi_0(\Omega^{\Omega^\Omega})\) (large Veblen ordinal) · \(\psi_0(\varepsilon_{\Omega + 1}) = \psi_0(\Omega_2)\) (Bachmann-Howard ordinal) · \(\psi_0(\Omega_\omega)\) with respect to Buchholz's ψ · \(\psi_0(\varepsilon_{\Omega_\omega + 1})\) (Takeuti-Feferman-Buchholz ordinal) · \(\psi_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}})\) (countable limit of Extended Buchholz's function) · \(\omega_1^\mathfrak{Ch}\) (Omega one of chess) · \(\omega_1^{\text{CK}}\) (Church-Kleene ordinal) · \(\omega_\alpha^\text{CK}\) (admissible ordinal) · recursively inaccessible ordinal · recursively Mahlo ordinal · reflecting ordinal · stable ordinal · \(\lambda,\gamma,\zeta,\Sigma\) (Infinite time Turing machine ordinals) · gap ordinal · List of countable ordinals
Ordinal hierarchies: Fast-growing hierarchy · Hardy hierarchy · Slow-growing hierarchy · Middle-growing hierarchy · N-growing hierarchy
Ordinal functions: enumeration · normal function · derivative · Veblen function · ordinal collapsing function · Weak Buchholz's function · Bachmann's function · Madore's function · Feferman's theta function · Buchholz's function · Extended Weak Buchholz's function · Extended Buchholz's function · Jäger-Buchholz function · Jäger's function · Rathjen's psi function · Rathjen's Psi function · Stegert's Psi function · Arai's psi function
Uncountable cardinals: \(\omega_1\) · omega fixed point · inaccessible cardinal \(I\) · Mahlo cardinal \(M\) · weakly compact cardinal \(K\) · indescribable cardinal · rank-into-rank cardinal · Berkeley cardinal · (Club Berkeley cardinal · limit club Berkeley cardinal)
Classes: \(\textrm{Card}\) · \(\textrm{On}\) · \(V\) · \(L\) · \(\textrm{Lim}\) · \(\textrm{AP}\) · Class (set theory)