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$

2 Answers 2

1
$\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.

$\endgroup$
1
  • 1
    $\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$ Aug 14, 2014 at 9:13
1
$\begingroup$

I found this a valuable resource:

A Survey of Arithmetical Definability by Alexis Bès

$\endgroup$
1
  • $\begingroup$ I've taken the liberty of fixing the broken link. $\endgroup$ Oct 25, 2022 at 20:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .