# Tag Info

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 ...
• 20.5k
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$ ...
• 20.5k
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$ ...
• 7,085
Accepted

### Existence of well-ordering of epsilon_0 in weak theories

The existence of $\epsilon_0$ and its order is not a problem, its well-foundedness is. Cantor normal forms (recursively expanded) of ordinals below $\epsilon_0$ can be written as strings over a ...
• 45.6k

### 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 ...

### 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 ...
• 20.5k
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 ...
• 45.6k
Accepted

• 6,365
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 ...
• 1,372

### 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 ...
• 20.5k
Accepted

### How to build large recursive ordinals using Dillator and/or Ptykes?

There are at least two fundamentally different ways how one could reach Bachmann-Howard ordinal using dilator and ptykes. One way is to allow recursion on ordinals for ptykes for all finite types. ...
• 5,481

### 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)$ ...
• 1,666
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 ...
• 5,481
Accepted

### Does Peano's axioms prove $\alpha$-induction for primitive recursive sequences for every concrete $\alpha < \varepsilon_0$?

I suppose you asked proving Goodstein's theorem for a given primitive recursive base sequence $\langle b_n\mid n\in\mathbb{N}\rangle$ (that is, the $(n+1)$th element of the Goodstein sequence is ...
• 2,910
Accepted

• 6,365