1
$\begingroup$

As far as I understand, Kriesel proved that there exists a recursive relation $R$ of order type $\omega$ such that $\mbox{PRA}+TI(R)$ proves $\mbox{Con}(PA)$, and Beklemishev proved that for any recursive ordinal $\alpha$, there is a recursive relation $R$ of order type $\alpha$ such that $\mbox{PRA}+TI(R)$ does not prove $\mbox{Con}(PA)$. This is somehow unsatisfactory that the provability strength of transfinite induction up to recursive ordinal $\alpha$ depends on the specific recursive encoding. But, intuitively, we can formulate "the" axiom $TI(\alpha)$ for any specific recursive ordinal $\alpha$, if we choose somehow natural and not very pathologic recursive relation $R_\alpha$ which encodes order type $\alpha$. For example, we expect that if $R_\omega$ is not very pathologic encoding of ordinal $\omega$ then $\mbox{PRA}+TI(R_\omega)$ does not prove $\mbox{Con}(PA)$. Can we somehow formalize what it means to be "the natural recursive encoding" of the specific recursive ordinal $\alpha$? Can we construct the good recursive encoding $R_\alpha$ for each recursive ordinal $\alpha$?

$\endgroup$
3
  • $\begingroup$ The key word you might be looking for is Kleene ordinal notations. For certain small ordinals $\alpha$, e.g., at least up to the Bachmann-Howard ordinal and in fact well beyond that, there are indeed explicitly defined “standard” notations (well-defined up to primitive recursive equivalence) given by systems of ordinal collapsing functions and hierarchies. (contd…) $\endgroup$
    – Gro-Tsen
    May 3, 2020 at 22:07
  • $\begingroup$ (contd…) As far as I can tell, the largest computable ordinal to have an explicitly defined system of notations published in the literature is described in Jan-Carl Stegert's 2010 thesis, “Ordinal Proof Theory of Kripke-Platek Set Theory Augmented by Strong Reflection Principles” and his paper with Wolfram Pohlers, “Provably Recursive Functions of Reflection”. But it is not known how to define such a standard notation for any given recursive ordinal (and believed that it cannot be done?): I think this is essentially the “subrecursive stumblingblock”. $\endgroup$
    – Gro-Tsen
    May 3, 2020 at 22:10
  • $\begingroup$ @Gro-Tsen Thank you! Is there any hope that we can define the property "R is a (proof-theoretically) good recursive encoding of recursive ordinal $\alpha$", and prove (in metatheory) that each recursive ordinal have such a good representation, without direct construction? If would be nice if we could define the theory $\mbox{PRA} + \bigcup_{\alpha < \omega_1^{CK}} TI(\alpha)$ and ask some questions about it. Is it too naive to hope to define such (noncomputable) theory in a natural canonical way (from a proof-theoretical strength perspective, at least)? $\endgroup$ May 3, 2020 at 22:22

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.