# Different arithmetics

The original Peano axioms were based on a single unary operator $\operatorname{succ}$ and one second-order induction axiom: $\lbrace \operatorname{succ} \rbrace + \operatorname{IND}_2$

Peano arithmetic is the first-order theory with additional explicit axioms for additional binary operators $+$ and $\times$ and the second-order induction axiom replaced by a first-order axiom schema: $\lbrace \operatorname{succ}, + ,\times\rbrace + \operatorname{IND}_1$

Presburger arithmetic is the first-order theory with additional axioms for one additional binary operator $+$ and a first-order induction axiom schema: : $\lbrace \operatorname{succ}, + \rbrace + \operatorname{IND}_1$

Skolem arithmetic is $\lbrace \operatorname{\times} \rbrace + \operatorname{IND}_1$ [added]

Robinson arithmetic is Peano arithmetic without induction: : $\lbrace \operatorname{succ}, + ,\times\rbrace - \operatorname{IND}_1$

What about other conceivable arithmetics, e.g.

• $\lbrace \operatorname{succ} \rbrace \pm \operatorname{IND}_1$
• $\lbrace \operatorname{succ, \leq} \rbrace \pm \operatorname{IND}_1$
• $\lbrace \operatorname{succ} , + \rbrace - \operatorname{IND}_1$
• $\lbrace \operatorname{succ}, +, \times, \operatorname{exp}\rbrace \pm \operatorname{IND}_1$

Which of them was given a name, which of them were investigated?

The Peano Axioms, as usually presented these days, include as successor function and induction, but no arithmetic operators ({succ}+IND$_1$ in your notation). Using these axioms along with ordinary logic and set theory, it is possible to construct the $+$, $\times$ and exp functions.
Without induction, $succ(x)=x$ for some number x (and many other oddities) cannot be ruled out.
The only reason you would include the definitions of $+$, $\times$ or exp in your axioms is if you didn't want to use set theory -- very limiting as you can imagine, but fun to see how far you can actually go.
• You don't necessarily need set theory (or second order logic) to define/construct $+$, $\times$ and so on, do you? You can equivalently use the operators to construct recursive functions. – Hans-Peter Stricker Aug 14 '14 at 9:13