32 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 ...
user avatar
24 votes
Accepted

Why is there a need for ordinal analysis?

The axioms of first-order arithmetic include the induction schema, which says that, for every formula $A(x)$ with free variable $x$, the conjunction of $A(0)$ and $\forall x\,(A(x)\to A(x+1))$ implies ...
user avatar
22 votes
Accepted

Why isn't this a computable description of the ordinal of ZF?

Theorem. The following are equivalent. The relation on $\mathbb{N}$ computed by your program P is a well-order. ZF is $\Pi^1_1$-sound. Proof. You gave the argument for the reverse implication $(2\...
user avatar
13 votes
Accepted

Regarding Gentzen's note regarding 'Godel-points' (i.e., "Where is the Godel-point hiding?")

Your question seems to boil down to (after fixing an error) the following: Any model $\mathfrak{M}$ of ACA$_0$ has a first-order part $Num(\mathfrak{M})$, which satisfies PA; why doesn't this mean ...
user avatar
12 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 ...
user avatar
12 votes
Accepted

How can any theory prove well-foundedness of ordinals above $\omega_1^{\text{CK}}$?

Just slightly expanding the comment of Emil Jeřábek: on one hand, in ZFC we can define some objects we call ordinals and prove transfinite induction of each of them. This is not what we ...
user avatar
  • 931
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$ ...
user avatar
10 votes

Formalizations of The Matchstick Diagram Representation of Ordinals

I prefer to think of the matchstick representations a little differently than you present them. Namely, your function $f$ provides the amount to jump up by at each step, the difference between each ...
user avatar
10 votes

Formalizations of The Matchstick Diagram Representation of Ordinals

Yes, $\omega_1^{md}$ is just $\omega_1$. Fix some countable limit ordinal $\alpha\ge\omega^2$ (so that there are infinitely many limit ordinals $<\alpha$ - ordinals $<\omega^2$ can be handled ...
user avatar
10 votes
Accepted

What system suffices to show the strength of PRA is $\omega^\omega$?

First, this is not quite the right question. The implication as such is going to be provable in a trivial base theory; the most important question is what “well-foundedness of $\omega^\omega$” means ...
user avatar
10 votes
Accepted

Gentzen's result on PA

Yes, Gentzen found a single "induction instance" which is PA-unprovable: more-or-less $\varphi(\alpha)$ = "Every sentence with a proof of cut-rank $\alpha$ has a cut-free proof." Now, this $\varphi$ ...
user avatar
9 votes
Accepted

What is the proof-theoretic ordinal of bare $\mathsf{NFU}$?

As in the question, I will use $\mathsf{NFU}$ for "bare" $\mathsf{NFU}$, i.e., the result of weakening the extensionality axiom in Quine's $\mathsf{NF}$ so as to allow urelements. Let $\...
user avatar
  • 14.5k
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 ...
user avatar
7 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. ...
user avatar
7 votes

How can any theory prove well-foundedness of ordinals above $\omega_1^{\text{CK}}$?

This is a difference between internal and external quantification. Proof-theoretic ordinal analysis involves an external quantification over (external, recursive) ordinals. What is provable in ZFC ...
user avatar
6 votes
Accepted

A question about ordinal analysis

First of all, note that we don't (yet) have ordinal analyses of subsystems of second order arithmetic beyond $\Pi^1_2$-CA$_0$. Still, we can say something about the pattern you indicate using known ...
user avatar
5 votes
Accepted

Is there a relation between type (maximum linearization) of a computable WQO and the ordinal strength of a theory needed to prove it?

Let me show that for extensions $T\supseteq\mathsf{ACA}_0$ the usual proof-theoretic ordinal $|T|_{WO}$ coincide with $|T|_{WPO}$ that is the suprema of $\mathsf{o}(X)$, for recursive wpo $X$, for ...
user avatar
5 votes

What does "can almost be proven in PA" mean regarding Theorem 2 of Timothy Chow's expository article, "The Consistency of Arithmetic"?

I believe you're overthinking what Chow means by "almost provable." We have an arithmetic statement of the form $$(*)\quad\forall x\varphi(x),$$ which while not provable in PA has the property that ...
user avatar
4 votes

Going beyond the strength of Peano arithmetic "without sets"

A lot of work has been done on (1) various systems of ordinal notations ranging from very weak to very strong and (2) calibrating the proof theoretic strength of various formal systems, say in terms ...
user avatar
  • 37.2k
4 votes

Iterated Gentzen: or, a Sith objection to the proof of consistency of PA

Mathobi is making a different argument in the comments on this post than in the question itself: in the post Mathobi is considering how far we need to justify transfinite induction to prove $G(i)$ ...
user avatar
  • 293
4 votes

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

The easiest way to construct a model $M$ of PRA where the Ackermann function is not total is to take a nonstandard model $M_0$ of, say, PA, fix a nonstandard element $a\in M_0$, and define $M$ as the ...
user avatar
4 votes

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

For every c.e. theory T (extending a weak base theory), we already know a polynomial time computable linear ordering $≺$ that captures the $Π^1_1$ strength of T: Provably in a weak base theory, a $Π^...
user avatar
4 votes
Accepted

Formalizations of The Matchstick Diagram Representation of Ordinals

Noah Schweber already gave a satisfactory answer, but let me make an extended comment that also gives an answer (not in the most efficient way, but in a way that is, I hope, both instructive and "...
user avatar
  • 21.7k
4 votes

Formalizations of The Matchstick Diagram Representation of Ordinals

To add to the answers already given, we can also construct a matchstick diagram for $\omega_1$ over an uncountable nonstandard model of the Rational numbers. The following is a construction of such a ...
user avatar
  • 6,241
3 votes
Accepted

Complexity of induction formulas in proof theoretic ordinals

By a padding argument, for reasonable notation systems, an elementary time computable predicate $P$ in $\mathrm{TI}(β,ECP)$ can be chosen to be polynomial time computable. For example, for limit $α&...
user avatar
2 votes
Accepted

Does this restriction on powersets in ZF have a proof theoretic ordinal?

Your theory interprets $\mathsf{ZF}^-$. In fact, $\mathsf{ZF}-$ (namely, $\mathsf{ZF}$ without Powerset) interprets $\mathsf{ZF}^-+(V=L)$. It answers your questions negatively since the proof-...
user avatar
  • 1,577
2 votes

Regarding Gentzen's note regarding 'Godel-points' (i.e., "Where is the Godel-point hiding?")

Gentzen's remark has some bite in the case the standard first-order arithmetic PA, because we plausibly know a bit more arithmetically. But he apparently did not understand the generality of the ...
user avatar
2 votes

What is the proof-theoretic ordinal of KPh?

Let $\mathsf{KPh}$ denote the theory $\mathsf{KP}+``\textrm{The recursively inaccessibles are unbounded}\! "$. I haven't found an explicit analysis of $\mathsf{KPh}$ in Rathjen's preprints, but there ...
user avatar
  • 293
1 vote

What countable ordinals are called $\kappa_\alpha$?

I think I've blundered into an answer to my own question. In this paper: • Hilbert Levitz, Transfinite ordinals and their notations: for the uninitiated. the author writes: The first ...
user avatar
  • 19.4k

Only top scored, non community-wiki answers of a minimum length are eligible