Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’ve started ordinal analysis, mostly because I was beginning to forget a lot of what I once knew, and I had occasion to look into it again.
I mainly wanted to get the big table in there for future reference, but I tried to say few general remarks as well. I know there’s not much of an npov on ordinal analysis (yet), but it’s certainly of interest concerning strength of type theories for example.
I may try to fill in more explanations of undefined terms later, but I’m done for today.
What is lacking from $RCA_0$ to get $RCA_0^*$?
It’s the other way around: $RCA_0$ is stronger than $RCA_0^*$ by having $\Sigma^0_1$-induction instead of $\Delta^0_1$-induction (over a language with addition, multiplication and exponentiation as function symbols).
I’ve added some more explanations to this effect.
Thanks for the contribution. In order for this entry to be visible, it would be good to have some more cross-links from and to related entries. (Think about how a user might find the entry who is looking for information on its content but who does not yet know about the existence of the entry.) I have now added minimal cross-links with the entries theory and ordinal, but certainly you’ll have a better idea of what could be done.
Ulrike, sorry, that’s what I meant, it just came out weird.
Cool! What is the $TI(-)$ in the first display? I can’t see it defined anywhere.
TI is transfinite induction, now added to that paragraph.
I’ve added links at countable ordinal and proof theory (and expanded the latter).
Thanks! I have touched the formatting at proof theory and have added more hyperlinks. For instance to a stub for Hilbert’s program.
We made a little edit to ordinal analysis, making it clearer that the first paragraph is the actual definition of proof-theoretic ordinal.
BTW, the reason for this change was an added link from Coq, that used to be linking to predicativity.
1 to 12 of 12