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.

muchmore complicated than the halting problem ($\mathcal{O}$ vs. ${\bf 0'}$). $\endgroup$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$7more comments