Timeline for "The" axiom of induction up to recursive ordinal $\alpha$ in $\mbox{PRA}$
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 3, 2020 at 22:22 | comment | added | Mykola Pochekai | @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)? | |
| May 3, 2020 at 22:10 | comment | added | Gro-Tsen | (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”. | |
| May 3, 2020 at 22:07 | comment | added | Gro-Tsen | 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…) | |
| May 3, 2020 at 21:07 | history | asked | Mykola Pochekai | CC BY-SA 4.0 |