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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 × 38lo.logic × 34

proof-theory × 21

ordinal-numbers × 15

set-theory × 10

theories-of-arithmetic × 10

foundations × 6

computability-theory × 5

reverse-math × 3

model-theory × 2

constructive-mathematics × 2

reference-request × 1

order-theory × 1

posets × 1

mathematical-philosophy × 1

notation × 1

constructibility × 1

induction × 1

intuitionism × 1

new-foundations × 1

formal-proof × 1

ultrafinitism × 1