0
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

I found this a valuable resource:

A Survey of Arithmetical Definability by Alexis Bès

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Hans-Peter Stricker Aug 14 '14 at 9:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.