# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUlrik
• CommentTimeJun 13th 2016

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.

• CommentRowNumber2.
• CommentAuthorDavidRoberts
• CommentTimeJun 13th 2016

What is lacking from $RCA_0$ to get $RCA_0^*$?

• CommentRowNumber3.
• CommentAuthorUlrik
• CommentTimeJun 13th 2016

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.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJun 14th 2016
• (edited Jun 14th 2016)

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.

• CommentRowNumber5.
• CommentAuthorDavidRoberts
• CommentTimeJun 14th 2016

Ulrike, sorry, that’s what I meant, it just came out weird.

• CommentRowNumber6.
• CommentAuthorJonasFrey
• CommentTimeJun 14th 2016

Cool! What is the $TI(-)$ in the first display? I can’t see it defined anywhere.

• CommentRowNumber7.
• CommentAuthorUlrik
• CommentTimeJun 14th 2016

TI is transfinite induction, now added to that paragraph.

I’ve added links at countable ordinal and proof theory (and expanded the latter).

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeJun 14th 2016

Thanks! I have touched the formatting at proof theory and have added more hyperlinks. For instance to a stub for Hilbert’s program.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeJul 22nd 2016

We made a little edit to ordinal analysis, making it clearer that the first paragraph is the actual definition of proof-theoretic ordinal.

• CommentRowNumber10.
• CommentAuthoratmacen
• CommentTimeJun 19th 2019

Added a new “Idea” section that I hope is more layperson-friendly, and which briefly discusses that the systems in the table are predicative-ish. The old “Idea and benefits” section is now the “Definition” section.

• CommentRowNumber11.
• CommentAuthoratmacen
• CommentTimeJun 19th 2019

BTW, the reason for this change was an added link from Coq, that used to be linking to predicativity.

• CommentRowNumber12.
• CommentAuthorUlrik
• CommentTimeOct 1st 2019

Add $\Delta_1^1$-CA$_0$ and $\Sigma^1_1$-AC$_0$ to the line of PA.