Return to Answer

The platonic view (with a touch of omniscience) is that every true $Π^1_1$ statement is provable from well-foundedness of a reasonable ordinal notation system for some recursive ordinal (dependent on the statement). However, this would make reasonableness 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). Still, the view has held up so far for theories for which have an ordinal analysis. The well-ordering of large cardinal consistency strengths leads support to the view, at least as a guiding (but for a formalist, limited) heuristic.

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.

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.

The platonic view (with a touch of omniscience) is that every true $Π^1_1$ statement is provable from well-foundedness of a reasonable ordinal notation system for some recursive ordinal (dependent on the statement). However, this would make reasonableness noncomputable; and to handle all true $Π^1_1$ (or just $Π^0_1$) statements of length $n$, the description of the notation system would need $2^{Ω(n)}$ symbols (for a fixed alphabet). Still, the view has held up so far for theories for which have an ordinal analysis. The well-ordering of large cardinal consistency strengths leads support to the view, at least as a guiding (but for a formalist, limited) heuristic.

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.

The platonic view (with a touch of omniscience) is that every true $Π^1_1$ statement is provable from well-foundedness of a reasonable ordinal notation system for some recursive ordinal (dependent on the statement). However, this would make reasonableness 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). Still, the view has held up so far for theories for which have an ordinal analysis. The well-ordering of large cardinal consistency strengths leads support to the view, at least as a guiding (but for a formalist, limited) heuristic.

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.

The platonic view (with a touch of omniscience) is that every true $Π^1_1$ statement is provable from well-foundedness of a reasonable ordinal notation system for some recursive ordinal (dependent on the statement). However, this would make reasonableness noncomputable; and to handle all true $Π^1_1$ (or just $Π^0_1$) statements of length $n$, the description of the notation system would need $2^{Ω(n)}$ symbols (for a fixed alphabet). Still, the view has held up so far for theories for which have an ordinal analysis. The well-ordering of large cardinal consistency strengths leads support to the view, at least as a guiding (but for a formalist, limited) heuristic.

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.

The platonic view (with a touch of omniscience) is that every true $Π^1_1$ statement is provable from well-foundedness of a reasonable ordinal notation system for some recursive ordinal (dependent on the statement). However, this would make reasonableness noncomputable; and to handle all true $Π^1_1$ (or just $Π^0_1$) statements of length $n$, the description of the notation system would need $2^{Ω(n)}$ symbols (for a fixed alphabet). Still, the view has held up so far for theories for which have an ordinal analysis. The well-ordering of large cardinal consistency strengths leads support to the view, at least as a guiding (but for a formalist, limited) heuristic.