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

  • 4
    $\begingroup$ @JoshuaZ Yes: we would need to know ahead of time which computable linear orders are well-ordered in order to rule out false answers. Determining whether a computable linear order is a well-order is much more complicated than the halting problem ($\mathcal{O}$ vs. ${\bf 0'}$). $\endgroup$ Oct 15, 2022 at 14:30
  • 2
    $\begingroup$ I just read Ron Maimon's article, and I find some of the things he says rather misleading. Supposing we take the conjecture you quoted at face value, it still doesn't mean that we can have any realistic hope of "knowing the answer to every [arithmetical] question of mathematics eventually." Even at the level of $\epsilon_0$, we have Noah Schweber on record here as saying that he doesn't regard Gentzen's proof as helping us "know" that PA is consistent if we didn't "know" it already. Also, his comment about iterated consistency statements overstates how far you can get with that idea. $\endgroup$ Oct 16, 2022 at 2:08
  • 3
    $\begingroup$ Maimon mentions Torkel Franzén; I assume he means Franzén's book Inexhaustibility: A Non-Exhaustive Account. I recommend that book highly if you're interested in these sorts of questions. I do agree with Maimon that Hilbert's program is not quite as dead as many make it seem, but I don't think that ordinal analysis is the panacea he seems to make it out to be. Finally, I'd mention that if you look up the literature on "absolute undecidability," you'll find some other interesting ideas about a modern form of Hilbert's program. $\endgroup$ Oct 16, 2022 at 2:14
  • 3
    $\begingroup$ Ron has some... eccentric... beliefs about the foundations of mathematics. $\endgroup$
    – Asaf Karagila
    Oct 16, 2022 at 23:25
  • 2
    $\begingroup$ @QiaochuYuan I see. It still seems a bit misleading because most sentences in the language of arithmetic are much more complicated than $\Sigma^0_1$ and some people might believe that $\Sigma^0_1$ sentences have definite truth values while more complicated sentences do not. $\endgroup$ Oct 19, 2022 at 16:51

2 Answers 2


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.

  • $\begingroup$ Thanks! Can you elaborate a little more on that last sentence? What's artificial about this to you and what would a less artificial version of this idea (speaking very vaguely) look ilke? $\endgroup$ Oct 15, 2022 at 0:46
  • $\begingroup$ @QiaochuYuan See my edit. $\endgroup$ Oct 15, 2022 at 3:12
  • $\begingroup$ Thanks very much for the clarification, this is helpful. So one would somehow like a computable order $\alpha$ which is "not tautologically related to $\varphi$," which one can stare at on its own terms to build intuition about whether one believes that $\varphi$ is true or false? I seem to recall a similar situation came up in one of Scott Aaronson's questions about the proof-theoretic ordinal of ZF. Can we make precise this notion of $\alpha$ "not being tautological"? (The tautological version is already interesting to me, for now!) $\endgroup$ Oct 15, 2022 at 17:49
  • 3
    $\begingroup$ @QiaochuYuan I think that "not being tautological" is a reference to the concept of ordinal analysis. So for example, one could argue that "well-foundedness of the Feferman–Schütte ordinal settles every theorem of $\mathsf{ATR}_0$." This is basically what Dmytro Taranovsky is addressing in his answer. $\endgroup$ Oct 15, 2022 at 21:12

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.