7
$\begingroup$

Does a theory like Robinson's arithmetic have a proof-theoretic ordinal? If so, what is it?

$\endgroup$
3
$\begingroup$

Well, since $Q$ doesn't even have induction along $\mathbb{N}$, I'm dubious that the notion of proof-theoretic ordinal makes sense for it; but if forced, I'd say the answer has to be $\omega$. Induction along finite orderings is trivial, so $\omega$ is the first ordinal for which it makes sense to ask "Does $Q$ prove induction along this ordinal?," and $Q$ doesn't.

$\endgroup$
5
  • $\begingroup$ Well, I guess I was hoping for some ordinal $\alpha$ such that the principlw of transfinite induction up to $\alpha$ plus some minimal theory (e.g., PRA) proves Con(Q). $\endgroup$ Oct 20 '16 at 3:10
  • $\begingroup$ @CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that. $\endgroup$ Oct 20 '16 at 3:19
  • $\begingroup$ I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful! $\endgroup$ Oct 20 '16 at 3:38
  • $\begingroup$ @CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . . $\endgroup$ Oct 20 '16 at 3:44
  • $\begingroup$ On the other hand, the proof theoretic ordinal of PRA is $\omega^\omega$, while the proof theoretic ordinal of EFA is just $\omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . . $\endgroup$ Oct 20 '16 at 3:46
3
$\begingroup$

Noah is correct that PRA $\vdash$ Con(Q): On p. 139 of the Handbook of Proof Theory, Chapter 2 (available here), Buss shows that $I\Delta_0$ + "tetration is total" $\vdash$ Con($I\Delta_0$), so it certainly proves Con(Q). Since $I\Delta_0 \subseteq$ PRA and PRA proves tetration total, the result follows.

(This is in response to a side question that came up in the comment thread of Noah's answer, but I don't have the karma to post this as a comment).

$\endgroup$

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.