I came across a [post](https://physics.stackexchange.com/a/14944/1046) 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)$?



Do we expect that sufficiently large computable ordinals settle every question of arithmetic?
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](https://en.wikipedia.org/wiki/Kleene%E2%80%93Brouwer_order) 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.


