For every true arithmetical statement $T$, there are $T$-incomparable $Π^0_1$ statements, but can we find them uniformly in $\text{Theory}(T)$?

Specifically, are there computable $A$ and $B$ such that for all arithmetical statements $T⊢\text{EA}$:

- $A_T$ and $B_T$ are $Π^0_1$ statements
- uniformity: $\text{Theory}(T') = \text{Theory}(T) ⇒ \text{EA}⊢(A_{T'}⇔A_T)∧(B_{T'}⇔B_T)$
- incomparability: if $T$ is true, then $T⊬A_T⇒B_T$ and $T⊬B_T⇒A_T$.

If yes, can $A$ and $B$ be monotonic, as in $(T⊢T') ⇒ \;\text{EA}⊢A_T⇒A_{T'}$?

*Generalization:* A negative answer perhaps admits the following generalization: If $C$ is computable with each $C_i$ monotonic (or just uniform) and $C_{i,T}$ being (a code for a) $Π^0_1$ statement, then the transitive closure of “$i≽j$ if $∀(\text{true }T') \, ∃(\text{true }T⊢T') \, (T⊢C_{i,T}⇒C_{j,T} )$” is a linear preorder with no computable infinite strict descending sequences. That would partially explain the natural well-ordering of consistency strengths.

*Partial results*

The question (and its monotonic variation) is unaffected by any combination of:

(1) Requiring statements to be $Π^0_2$.

(2) Replacing $\text{EA}$ (Elementary Arithmetic) with a stronger true statement.

(3) Dropping "$\text{EA}⊢$" in the uniformity condition, or in the other direction, requiring $A$ and $B$ to be explicitly uniform, i.e. in the form "for every proof (in first order logic) $T'⇔T$, $C_{T'}$ holds" (and analogously for the monotonicity condition).

*Note:* For (1), use incomparable $Π^0_1$ statements for $\text{1-Con}(T)$. For (3), we get explicitly uniform $T$-equivalents for $A_T$ and $B_T$ if $T$ proves "$A$ and $B$ satisfy the weakened uniformity condition for all $T$" (which is $Π^0_2$). However (using slow consistency), there are (explicitly) monotonic $A$ and $B$ that work for $Π^0_1$ $T$ and incomparability in $S+T$ where $S$ is a fixed $\text{1-Con}$ background theory such as $\text{PA}$.

Likely, there are monotonic $A$ and $B$ that are incomparable for some arbitrarily strong statements. For example, let $A_T$ be $\text{Con}(T+\text{Con}(T))$, and $B_T$ be $\text{Con}(T)$ plus $\text{Con}(T'+\text{Con}(T'+\text{Con}(T')))$ when we prove (from $T$) $T'$ plus incompressibility of some string of length $2^{2^{|T'|}}$. We can also iterate the $T$-consistency operator by various functions in the number of digits of the Chaitin's constant that we get a proof of in $T$.

Some results related to the question are in:

On the inevitability of the consistency operator (Antonio Montalbán and James Walsh)

A note on the consistency operator (James Walsh)

*Motivation*

Natural statements are usually well-ordered by consistency strength. There are no known natural examples of ZFC-incomparable $Π^0_1$ statements, and the examples I know (including Nonlinearity in the hierarchy of large cardinal consistency strength by Joel Hamkins) arbitrarily depend on the minutia of the deduction system, producing presumably inequivalent statements depending on whether say variable names must be in Latin or Greek. Can this dependence be naturally eliminated?

There are three approaches:

- Find a fundamental limitation on $Π^0_1$ provability in ZFC that does not generalize to other theories,
- Use some symmetry (as distinct from strength) of the specific strength of ZFC or a stronger theory, or
- Use something that works for strong theories in general (i.e. this question).

*Higher expressiveness levels*

The well-ordering of natural consistency strengths is part of a broader phenomenon. Natural $Π^1_1$ statements (and similarly for $Π^0_1$, $Π^0_2$, $Π^1_2$, $Σ^1_2$, etc) tend to be well-ordered under provable implication in a base theory; here, these statements include $Π^1_1$ traces of natural higher descriptive complexity statements, but exclude lower complexity statements in 'disguise'. This works if the base theory is strong enough to appropriately fix basic facts at the expressiveness level, such as $\text{EA}$ for $Π^0_2$, $\text{ATR}_0$ for $Π^1_2$, and apparently $\text{Z}_2+\text{PD}$ for general statements in second order arithmetic.

The hierarchy can be partially explained by:

- Essential 'completeness' of appropriate base theories, with known natural incompleteness typically tied to an assertion of symmetry, and in turn to an ordinal in a higher set theory.
- Well-ordered hierarchies of strengths, such as $Π^1_1$ proof ordinals and heights of transitive models.
- Universality: Natural statements that require a certain specific strength tend be universal for that strength and the expressiveness level of the statement (for expressiveness levels sufficiently fixed by the base theory).

There are counterexamples to the universality such as (for PA) Con(ZFC) + 1-Con(PA), but these tend to be composed of universal components, and analogously to this question, there might be mechanisms that 'enforce' well-orderings of natural $Π^0_2$ strengths for theories augmented with all true $Π^0_1$ statements.