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

11
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$ ...

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

10
votes

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

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

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

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

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 $\...

7
votes

### Does $\text{ACA}_0$ + True Arithmetic prove the well-foundedness of every recursive ordinal?

There is a result of Kreisel (see [1, Theorem 6.7.4,6.7.5]) that for extensions of $\mathsf{ACA}_0$ the $\Pi^1_1$ proof-theoretic ordinal (suprema of the order types of provable recursive well-...

6
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 $Π^...

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

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

5
votes

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
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)$ ...

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

4
votes

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

4
votes

Accepted

### A possible flaw in Theorem 14.17 in Kurt Schütte's -Proof Theory-

Fortunately, there appears to be no flaw in Schütte's construction. Only in my understanding of it.
Ordinal terms are defined on page 86. The term $\alpha=(0,((0,0),0))$ does NOT represent $\...

4
votes

Accepted

### $Π^0_1$ Proof Ordinals

Modulo the fact that Beklemishev [1] considers consistency with cuts as the basic consistency notion, his $\mathsf{Con}(\mathsf{EA}_\alpha)$ are equivalent to your's $\mathsf{Con}_{\alpha}$. It is ...

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

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

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

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

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 $α&...

2
votes

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

2
votes

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

Pakhomov and Walsh proved the following result:
Theorem. Let $\alpha$ be an ordinal notation. Then $|\mathbf{R}^\alpha_{\Pi^1_1}(\mathsf{ACA}_0)|_{\Pi^1_1}=\varepsilon_\alpha$.
Here $\mathbf{R}^\...

2
votes

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

$\newcommand{\bomega}{\boldsymbol\omega}$Given the definition of bounding ordinal in the post and the potential sensitivity to coding mentioned in edit 2, these seem to be two main ways to formalize ...

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

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

1
vote

### How closely do ordinal collapsing functions relate to Mostowski collapse?

This description seems to be a closer connection to Mostowski collapse than "it is the order type of $C_\Omega(\alpha,\rho)$ when some elements are removed":
A similar comparison appears in ...

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

#### Related Tags

ordinal-analysis × 56lo.logic × 48

proof-theory × 31

ordinal-numbers × 28

set-theory × 17

theories-of-arithmetic × 12

foundations × 9

computability-theory × 5

reverse-math × 4

reference-request × 2

model-theory × 2

constructive-mathematics × 2

ct.category-theory × 1

order-theory × 1

examples × 1

posets × 1

mathematical-philosophy × 1

notation × 1

type-theory × 1

axioms × 1

constructibility × 1

induction × 1

intuitionism × 1

new-foundations × 1

formal-proof × 1