26
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)\rightarrow A(x+1))$ ...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

#### Related Tags

ordinal-analysis × 52lo.logic × 45

proof-theory × 30

ordinal-numbers × 24

set-theory × 14

theories-of-arithmetic × 11

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