Skip to main content
Search type Search syntax
Tags [tag]
Exact "words here"
Author user:1234
user:me (yours)
Score score:3 (3+)
score:0 (none)
Answers answers:3 (3+)
answers:0 (none)
isaccepted:yes
hasaccepted:no
inquestion:1234
Views views:250
Code code:"if (foo != bar)"
Sections title:apples
body:"apples oranges"
URL url:"*.example.com"
Saves in:saves
Status closed:yes
duplicate:no
migrated:no
wiki:no
Types is:question
is:answer
Exclude -[tag]
-apples
For more details on advanced search visit our help page
Results tagged with
Search options not deleted user 8991
11 votes
Accepted

Correspondence between proof-theoretic ordinals and fast growing functions?

Yes: for many theories, $\alpha$ is the proof-theoretic ordinal of T exactly when T proves that $f_\beta$ is total for all $\beta<\alpha$, but does not prove $f_\alpha$ is total. (Where $f_\alpha$ is …
Henry Towsner's user avatar
13 votes

Why is there a need for ordinal analysis?

In addition to the reasons Andreas gives, Gentzen's theorem gives additional information that's interesting even if you don't have any qualms about consistency. In particular, ordinal analysis gives …
Henry Towsner's user avatar
8 votes
Accepted

Which ordinals are proof-theoretic ordinals?

If $\alpha$ is a reasonable presentation of a computable ordinal then the proof-theoretic ordinal of $ACA_0+\alpha$ is well-ordered is the smallest $\epsilon$ number $>\alpha$. (There's a proof of th …
Henry Towsner's user avatar
9 votes

Which ordinals can be proof-theoretic ordinals of a reasonable theory?

Regarding the small Veblen ordinal, Rathjen and Weiermann gave an analysis of theories in that range of strength in Proof-theoretic investigations of Kruskal's theorem.1 Working over a reasonable bas …
Henry Towsner's user avatar
8 votes
Accepted

Models of PRA/EFA with induction on $X$ but not $\omega^X$

I suspect the paper you want is Avigad and Sommer, A Model-Theoretic Approach to Ordinal Analysis. As the name suggests, they give an ordinal analysis rooted in the structure of models of arithmetic. …
Henry Towsner's user avatar
33 votes
Accepted

Is there a computable ordinal encoding the proof strength of ZF? Is it knowable?

Rom Maimon is describing the program of proof-theoretic ordinal analysis. First, as you observed in your addendum, it isn't interesting to find some encoding of an ordinal whose well-foundedness im …
Henry Towsner's user avatar
13 votes
Accepted

Nontrivial upper bounds on proof-theoretic ordinals of strong theories: do we have any?

I think the short answer is no, and I'm not sure there really could be: I don't think we "know" any ordinals above the ordinal of $\Pi^1_2-CA$ but below $\omega_1^{CK}$. Theoretically someone could w …
Henry Towsner's user avatar
16 votes
Accepted

What is the proof-theoretic ordinal of PA + Con(PA), PA + Con(PA + Con(PA)) etc., and why?

This is an instance of a general phenomenon: adding true $\Pi_1$ sentences to a reasonable theory doesn't change its proof-theoretic ordinal. $Con(T)$ is $\Pi_1$, so if $T$ is any consistent theory, …
Henry Towsner's user avatar
5 votes

What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

This is a second answer (think of it as part two of the other, already long, answer), in response to the clarification of the question by Keshav Srinivasan in the comments on that question. First, no …
Henry Towsner's user avatar
6 votes

What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

The difficulty is in what it means to go up the ramified hierarchy. When talking about theories, you can't write down a computable or c.e. theory which perfectly captures the whole ramified hierarchy …
Henry Towsner's user avatar
22 votes
Accepted

Why do stacked quantifiers in PA correspond to ordinals up to $\epsilon_0$?

8/14: Substantially edited in response to comments: added to 1st part, added new 2nd and 4th parts There's also some discussion underneath, and a link to a partial write-up of a case of cut-eliminati …
Henry Towsner's user avatar