Timeline for Proof-theoretic ordinals: inevitable consistency?
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Aug 19, 2023 at 7:45 | history | suggested | C7X | CC BY-SA 4.0 |
Clarifying that the link is to citation [1], and https
|
| Aug 19, 2023 at 6:32 | review | Suggested edits | |||
| S Aug 19, 2023 at 7:45 | |||||
| Jun 8, 2019 at 9:20 | comment | added | Fedor Pakhomov | @NoahSchweber You don't need to have fixed system of fundamental sequences. You just quantify over all compuable objects that constitute a pair of a linear order and system of fundamental sequences for it. | |
| Jun 8, 2019 at 9:17 | comment | added | Fedor Pakhomov | @NoahSchweber And there is a definition recently proposed by James Walsh and me ( arxiv.org/abs/1805.02095 ). Namely, one could consider the order on computably axiomatizable extensions $T$ of $\mathsf{ACA}_0$: $T_1<_{\Pi^1_1\text{-}RFN}T_2$ iff $T_2$ proves that $T_1$ is $\Pi^1_1$-sound. It happen that all $\Pi^1_1$-sound theories lie in the well-founded part of this order. Thus we have well-founded ranks for elements of this order. The correspondence with the standard proof-theoretic ordinals is that the theory with rank $\alpha$ have the proof-theoretic ordinal $\varepsilon_\alpha$. | |
| Jun 8, 2019 at 9:14 | comment | added | Noah Schweber | Since that one requires a fixed system of fundamental sequences I think I still consider it notation-dependent. But it's definitely interesting! | |
| Jun 8, 2019 at 9:11 | comment | added | Fedor Pakhomov | @NoahSchweber The notation-independent definitions that I am aware of are equivalent to the standard suprema of the order types of well-founded relations (at least for strong enough systems). I note couple that have a flavour that is a bit different from the standard one. People have considered the supremas of order types of all notation systems $\alpha$ with fixed systems of fundamental seuqneces such that given system $T$ proves that in any infinite set there is an $\alpha$-large finite subset. | |
| Jun 8, 2019 at 9:03 | comment | added | Fedor Pakhomov | In the initial answer I claimed that my argument is essentially identical to the argument of Beklemishev, which isn't correct since Beklemishev actually proved stronger result. I have edited the answer accordingly. | |
| Jun 8, 2019 at 9:02 | history | edited | Fedor Pakhomov | CC BY-SA 4.0 |
More correctly referred to Beklemishev's paper
|
| Jun 8, 2019 at 8:55 | comment | added | Noah Schweber | Out of curiosity, do you know of any other notation-independent definitions of proof-theoretic ordinals other than the sup of the ordertypes of primitive recursive relations the theory proves are well-founded? I remember hearing of such, but now that I think about it I can't recall any details. | |
| Jun 8, 2019 at 8:54 | comment | added | Noah Schweber | Thanks for the added detail - this is great! | |
| Jun 8, 2019 at 8:53 | vote | accept | Noah Schweber | ||
| Jun 8, 2019 at 8:49 | history | answered | Fedor Pakhomov | CC BY-SA 4.0 |