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$?
$\begingroup$
$\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-TsenCommented 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-TsenCommented 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$– Mykola PochekaiCommented May 3, 2020 at 22:22
Add a comment
|