Timeline for Which ordinals can be proof-theoretic ordinals of a reasonable theory?
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 24 at 8:46 | history | edited | gmvh |
Added top-level tag
|
|
| Jun 24 at 6:49 | answer | added | Hanul Jeon | timeline score: 2 | |
| Jun 24 at 4:08 | comment | added | Hanul Jeon | @C7X I will try to re-read the references and will post an answer. | |
| Jun 24 at 3:57 | comment | added | C7X | @HanulJeon Thank you for the references, the fact in "Reducing $\omega$-model reflection" may answer the question! Unfortunately I am not familiar with some of the conventions used in this paper, specifically the meaning of the dot over $\alpha$ in the definition of proof-theoretic dilator. If it denotes an arbitrary ordinal notation for $\alpha$ (and if the choice of ordinal notation does not affect PTO), then it does show that every recursive epsilon is bounding as you had hoped. About $\vert\mathsf{ACA}_0+0\text{ is well-founded}\vert_{\Pi^1_1}$, see Wojowu's second comment on this post. | |
| Jun 23 at 8:22 | history | edited | Martin Sleziak | CC BY-SA 4.0 |
a minor typo
|
| Jun 22 at 13:08 | comment | added | Hanul Jeon | I am unsure if I understand the definition of a bounding ordinal: As far as I understand, $\varepsilon_0$ cannot be bounding since the PTO of $\mathsf{ACA}_0$ (=$\mathsf{ACA}_0$ + "$0$ is well-founded") is $\varepsilon_0$, so if $\varepsilon_0$ is bounding, then $\varepsilon_0 = |\mathsf{ACA}_0 + 0\text{ is well-founded}|_{\Pi^1_1}<\varepsilon_0$, which does not make sense. | |
| Jun 22 at 13:05 | comment | added | Hanul Jeon | @C7X Also, it is known that the PTO of $\mathsf{ACA}_0$ + "$\alpha$ is well-founded" for a recursive well-order $\alpha$ is the least epsilon number greater than $\alpha$. It follows from Aguilera-Pakhomov's unpublished result on the proof-theoretic dilator of $\mathsf{ACA}_0$ (but it appears in Pakhomov-Walsh's paper Reducing $\omega$-model reflection to iterated syntactic reflection.) | |
| Jun 22 at 12:50 | comment | added | Hanul Jeon | @C7X The result is available in a paper by Pakhomov-Walsh titled Reflection ranks and ordinal analysis. The theory takes the form of iterated $\Pi^1_1$-reflection over a recursive linear order (Theorem 5.11), and it is not quite clear for me that this theory takes the form you mentioned. | |
| Jun 22 at 9:39 | comment | added | C7X | @HanulJeon Do you recall if such theories can always be found that are of the form $\mathsf{ACA}_0+'\{e\}\textrm{ computes a well-ordering}'$? If so, then every recursive epsilon ordinal is limiting: given a recursive epsilon $\gamma$, find an $\{e\}$ that computes $\gamma$ such that $\vert\mathsf{ACA}_0+'\{e\}\text{ computes a well-ordering}'\vert_{sup}=\gamma$, then for any $\alpha<\gamma$, chop $\{e\}$ at $\alpha$ to obtain an ordinal notation for $\alpha$ such that its well-foundedness statement has PTO $\leq\gamma$ over $\mathsf{ACA}_0$ as desired. | |
| Jun 21 at 10:57 | comment | added | Hanul Jeon | I heard that every recursive epsilon number could be a proof-theoretic ordinal of a recursive $\Pi^1_1$-sound extension of $\mathsf{ACA}_0$. Does it answer your question if it holds? | |
| Jun 21 at 10:08 | answer | added | C7X | timeline score: 2 | |
| Jun 7 at 10:30 | comment | added | Wojowu | @C7X I'm uncertain what I meant 10 years ago but I think replacing it with "PTO of ... is $\leq\gamma$" would match what I was after. But then again by now I am aware this is very sensitive to how the well-orders are coded and just speaking of ordinals on their own doesn't make sense here, so I'm not sure how meaningful that question is. | |
| Jun 7 at 6:40 | comment | added | C7X | Is $\varepsilon_0$ bounding? For example if $\alpha=\omega^\omega$, then the PTO of $\mathsf{ACA}_0$+"$\omega^\omega$ is well-founded" is $\varepsilon_0$, which is not less than $\varepsilon_0$. | |
| S Nov 2, 2022 at 6:24 | history | suggested | C7X |
Relevant tag, in particular Gentzen-style proof theory outside PA alone
|
|
| Nov 2, 2022 at 4:55 | review | Suggested edits | |||
| S Nov 2, 2022 at 6:24 | |||||
| Nov 16, 2014 at 11:48 | history | edited | Wojowu | CC BY-SA 3.0 |
added 688 characters in body
|
| Oct 28, 2014 at 17:36 | history | edited | Wojowu | CC BY-SA 3.0 |
added 650 characters in body
|
| Oct 28, 2014 at 10:39 | history | edited | Wojowu | CC BY-SA 3.0 |
added 140 characters in body
|
| Oct 27, 2014 at 22:45 | answer | added | Henry Towsner | timeline score: 9 | |
| Oct 27, 2014 at 22:06 | comment | added | Wojowu | Yes, you are right. I actually had induction up to $\epsilon_0$ in mind. I edited the question. | |
| Oct 27, 2014 at 22:05 | history | edited | Wojowu | CC BY-SA 3.0 |
added 39 characters in body
|
| Oct 27, 2014 at 21:59 | comment | added | Emil Jeřábek | See mathoverflow.net/questions/123713 for a related question. In particular, there is no such thing as PA + “$\varepsilon_0$ is well-founded”, as well-foundedness is a $\Pi^1_1$ property, so you need to be more precise. | |
| Oct 27, 2014 at 21:49 | history | asked | Wojowu | CC BY-SA 3.0 |