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) eq 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)\).
Attributes | Values |
---|---|
rdfs:label |
|
rdfs:comment |
|
sameAs | |
dcterms:subject | |
dbkwik:googology/p...iPageUsesTemplate | |
abstract |
|