1
$\begingroup$

For the example of Presburger Arithmetic, which consists of basic axioms for successor, addition, as well as an infinite set of induction axioms. However, it is well known that Presburger Arithmetic can also be formalized with the following axioms:

  1. Axioms for ordered Abelian groups;
  2. $0 < 1$;
  3. $\forall x\ (x \leq 0\vee x \geq 1)$;
  4. $\forall x\ (P_n(x) \leftrightarrow \exists y\ x = ny)$, for $n=2,3,...$;
  5. $\forall x\ \bigvee_{i=0}^{n-1}\big[ P_n(x+i) \wedge \bigwedge_{j\neq i} \neg P_n(x+j) \big]$.

These axioms are exactly what Cooper's algorithm needs to decide any sentence of Presburger Arithmetic: by converting the sentence into divisibility-equality normal form and then eliminate existential quantifiers.

On the other hand, the set of axioms of divisibility seems “more natural" than induction axioms, since it's very hard to come up with the correct induction axioms to prove a theorem. My question is that, is there any set of "more natural" axioms that is equivalent to induction axioms in Peano Arithmetic? Hopefully, it would seem like this (I borrow the idea from Presburger Arithmetic):

  1. Axioms for discretely ordered ring;
  2. $\forall n\forall m>0\ \big[\exists! p\exists! q\ (n = pm+q \wedge 0\leq q < m)\big]$.
  3. etc...

New edit: I am not seeking for a finite axiomatization since the divisibility axioms of Presburger Arithmetic are infinite schemes. Noah Schweber mentioned that full PA would need arbitrarily large nested quantifier axioms. So would the situation be more possible for $I\Delta_0$, the case that only bounded formulas are used to be induction axioms?

$\endgroup$
  • $\begingroup$ Is it that you find the axiomatization of "proof by induction works" to be unnatural, or that you find induction itself to be unnatural and are looking for phrasings in terms of other things like the well-ordering (every set of natural numbers has a smallest element) or the recursion theorem (you can define functions by recursion)? $\endgroup$ – user14972 Aug 30 '18 at 16:05
  • $\begingroup$ My starting point is to facilitate automatic reasoning. For the case of Presburger arithmetic, it’s pretty hard to come up with the correct induction axioms and complete the proof. However, by rephrasing axioms with divisibility the decision procedure becomes easier. For the case of PA or fragment of it, I dont’t expect a decision procedure but some rephrasing axioms that can simplify proof findinh. $\endgroup$ – Dieqiao Feng Aug 30 '18 at 18:32
0
$\begingroup$

PA is not finitely axiomatizable, so there's no way to replace the induction scheme with a single simpler axiom. Moreover, restricting the induction scheme to $\Sigma_n$ formulas for fixed $n\in\mathbb{N}$ also yields a strictly weaker theory (called "I$\Sigma_n$"), so any equivalent formulation of the induction scheme will have to involve arbitrary-quantifier-complexity formulas. Indeed, any axiomatization of PA has to involve sentences of arbitrarily high quantifier complexity.

While your question is too subjective to really admit a definitely negative answer, I think the above facts give good evidence that there won't be a truly satisfying way to rephrase induction along the lines you're looking for.

$\endgroup$
  • $\begingroup$ Thanks for your reply. I was not seeking for a set of finite axioms. As you can see the divisibility axioms for Presburger Arithmetic are also infinite. Regarded your point that axioms need infinite nested quantifiers, can the situation be possible for $I\Delta_0$? $\endgroup$ – Dieqiao Feng Aug 30 '18 at 15:47

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.