Do we expect that sufficiently large computable ordinals settle every question of arithmetic?

Question

I came across a post by Ron Maimon on physics.SE that makes what seems to me to be a very interesting conjecture I've never seen before about what it would take to settle every question of arithmetic. First I'll try to be more precise: a question of arithmetic is a first-order statement in Peano arithmetic, e.g. a statement about whether some Turing machine halts. I believe these are exactly the mathematical statements which, for example, Scott Aaronson regards as having definite truth values independent of our ability to prove or disprove them from any particular system of axioms, unlike e.g. the continuum hypothesis.

If I've understood Ron correctly, he seems to believe the following:

Conjecture: Every question of arithmetic is settled by the claim that some sufficiently large computable ordinal $\alpha$ is well-founded.

For example, Gentzen showed that the well-foundedness of $\alpha = \epsilon_0$ can prove the consistency of PA.

Question: Has this been stated as a conjecture somewhere in the literature? Do people expect it to be true?

A possibly more helpfully specific version of this question: does there exist for every positive integer $n$ a computable ordinal $\alpha_n$ whose well-foundedness determines the value of the Busy Beaver number $BB(n)$?

Answer 1

The question of whether a computable linear order is well-founded is $\Pi^1_1$-complete, so this is true in a sense:

There is a computable function $F$ such that, for every sentence $\varphi$ in the language of arithmetic with Godel number $\ulcorner\varphi\urcorner$, $F(\ulcorner\varphi\urcorner)$ is an index for a computable well-ordering iff $\varphi$ is true.

(To be precise, this is provable in - say - $\mathsf{ZF}$ or indeed much less.) Here's one way to visualize $F$:

There is a computable tree $\mathcal{T}\subseteq\mathbb{N}^{<\mathbb{N}}$ with a unique path $p$ which codes the set of true arithmetic sentences. Essentially, a node of height $k$ on $\mathcal{T}$ consists of a truth assignment to the first $k$-many sentences in the language of arithmetic and additional "partial Skolemization data" which so far looks consistent (the details are a bit tedious). Given a sentence $\varphi$, let $\mathcal{T}_\varphi$ be the subtree of $\mathcal{T}$ consisting of all nodes on $\mathcal{T}$ which (when "read" in the appropriate way) do not declare $\varphi$ to be true; this is a computable subtree of $\mathcal{T}$, uniformly in $\varphi$, and is well-founded iff $\varphi$ is true. We then set $F(\ulcorner\varphi\urcorner)$ to be the Kleene-Brouwer ordering of $\mathcal{T}_\varphi$.

Of course, this is all rather artificial. To be clear, the map $F$ itself is perfectly natural/interesting/important, but the result $F(\ulcorner\varphi\urcorner)$ is not particularly interesting to me. Contrast the construction above, where the connection between $\varphi$ and $F(\ulcorner\varphi\urcorner)$ is boringly tautological, with Gentzen's theorem that well-foundedness of (the usual notation for) $\epsilon_0$ implies $Con(PA)$. Even if one doesn't buy this as making $Con(PA)$ more believable - and I don't - it's certainly a deep and interesting fact. The interesting version of the conjecture, to me, would be: "For every sentence of arithmetic $\varphi$ there is a computable linear order $\alpha$ such that $(i)$ $WF(\alpha)\leftrightarrow\varphi$ and $(ii)$ knowing this somehow sheds light on $\varphi$ (unless $\varphi$ was already so simple as to be boring)." And nothing like what I've described can possibly do that, obviously.

Answer 2

The claim of well-foundedness depends not only on the ordinal $α$, but also on how $α$ is represented by a recursive well-ordering.

Pathological representations

Strong statements from small ordinals: For every true $Π^0_2$ statement $∀x \, ∃y \, \varphi(x,y)$, there is a computable representation of $ω$ whose well-foundedness is equivalent to the statement. For example, set $n_0 ≺ n_0-1 ≺ \cdots ≺ 1 ≺ 0 ≺ n_1 ≺ n_1-1 ≺ \cdots ≺ n_0+1 ≺ n_2 ≺ \cdots$, where $n_i$ is the least natural number such that $∀x≤i \, ∃y≤n_i - i \,\, \varphi(x,y)$. A similar claim with a higher ordinal (I think $ω^ω$ suffices) applies to all arithmetic statements, and similarly for higher levels of the hyperarithmetic hierarchy, with the ordinal depending on the level but not on the statement. To see this, for a fixed computable $α$, the set of all true $Π^0_α$ statements is $Δ^1_1$, so adding all such statements to a base theory does not suffice to reach all ordinals $<ω_1^{\text{CK}}$. I think $ω^α$ suffices for $Π^0_1(0^{(α)})$ where $0^{(α)}$ is the $α$th Turing jump of $0$. This should be optimal (for $α>0$); true $Π^1_1$ statements can require arbitrarily large recursive ordinals.

Large ordinals with weak strength: On the other hand, a sound theory can prove well-ordering for an arbitrarily large recursive ordinal without proving consistency of (for example) second order arithmetic $\text{Z}_2$. For example, pick a reasonable recursive pseudowellordering based on the Kleene-Brouwer ordering of a tree searching for an $ω$-model of $\text{Z}_2$. Its well-foundedness is equivalent to non-existence of $ω$-models of $\text{Z}_2$, and hence is $Σ^1_1$ conservative over $\text{Z}_2$. Thus, $\text{Z}_2$ with the schema for well-foundedness of the initial length $<ω_1^{\text{CK}}$ segments of the pseudowellordering (note that this is not a c.e. schema) is $Σ^1_1$ conservative over $\text{Z}_2$ despite being sound and proving well-foundedness of some representations of arbitrarily large recursive ordinals.

Canonical representations

However, for ordinals within reasonable ordinal notation systems so far, given two reasonable ordinal notation systems $T_1$ and $T_2$ for $α$, provably in a weak base theory (such as EFA, and with a constructive proof), there is an order-preserving bijection between $T_1$ and $T_2$. Thus, intuitively, we can speak of well-foundedness of $α$ (such as $ε_0$) with the use of a reasonable representation being implicit. Larger ordinals correspond to stronger consistency and other statements. Canonical $Π^0_1$ statements tend to be equivalent to some $α$-iterated consistency here (even in EFA, if we iterate cut-free consistency of EFA), and similarly with $Π^0_2$ and many higher level statements.

We do not yet have a canonical ordinal analysis of $\text{Z}_2$, with its extensive impredicativity being an obstacle here. However, ordinal analysis of weaker systems, existence of canonical inner models (at least up to many Woodin cardinals), the well-ordering of large cardinal consistency strengths, and other factors all suggest that every $Π^1_1$ consequence of known large cardinal axioms is provable from well-foundedness of a reasonable ordinal notation system.

A natural platonic view (with a touch of omniscience) is that this extends to every true $Π^1_1$ statement (and with extensions for higher levels of expressiveness). However, this would make being a reasonable ordinal notation system noncomputable; and to handle all true $Π^1_1$ (or just $Δ^0_2$, or for bounded compute time, $Π^0_1$) statements of length $n$, the description of the notation system would need $2^{Ω(n)}$ symbols (for a fixed alphabet). By contrast, one formalist view treats symmetry and related constructs (such as the cumulative hierarchy or ordinal notation systems based on recursively large ordinals) as a guiding (but limited) heuristic.