Uniform incomparable consistency strengths

Question

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.

Answer 1

This does not answer your question, but I find it relevant. You ask for uniform incomparable statements $A_\tau$ and $B_\tau$, and then ask also for monotonicity. But I claim that if one asks for the mapping on all consistent sentences, rather than just the true sentences, then we can't even get independent sentences $A_\tau$ one at a time in a uniform monotone manner.

Kindly allow me to work over PA in place of EA.

Theorem. There is no assignment $\tau\mapsto A_\tau$ mapping sentences $\tau$ in the language of arithmetic to sentences $A_\tau$ with the following properties:

1. (Independence) If PA${}+\tau$ is consistent, then so are PA${}+\tau+A_\tau$ and PA${}+\tau+\neg A_\tau$.

2. (Monotonicity) If PA${}\vdash\tau\to\sigma$ then PA${}\vdash A_\tau\to A_\sigma$.

Proof. Since the trivial assertion $1=1$ is consistent with PA, it follows by the independence property that $A_{1=1}$ is independent of PA. In particular, the theory PA${}+\neg A_{1=1}$ is consistent. By the independence property applied to this statement, we see that the statement $A_{\neg A_{1=1}}$ is independent of PA${}+\neg A_{1=1}$. Thus, PA${}+\neg A_{1=1}+A_{\neg A_{1=1}}$ is consistent. The key thing to notice next is that because $\neg A_{1=1}$ provably implies $1=1$, it follows by monotonicity that we can prove in PA that $A_{\neg A_{1=1}}\to A_{1=1}$. This contradicts the previous consistency assertion. So there is no such mapping with those two principles. $\Box$

What the theorem shows at bottom is that there is no monotone version of the Rosser sentence. The Rosser sentence $\rho_\tau$ is the sentence asserting that for every proof of $\rho_\tau$ in PA${}+\tau$, there is a smaller proof of the negation. It is well known that the Rosser sentences fulfill the independence property. It follows by the theorem, therefore, that Rosser sentences do not satisfy the monotonicity property.

Note that monotonicity is a strengthening of:

(Uniformity) If PA${}\vdash\tau\iff\sigma$, then PA${}\vdash A_\tau\iff A_\sigma$.

I am not yet sure how to undertake the argument if we weaken monotonicity to uniformity, but I suspect a version of this will be possible.

Note that the theorem makes no requirement on the logical complexity of $A_\tau$ or on the computability of the map $\tau\mapsto A_\tau$.

If we insist on the two properties only for sentences $\tau$ that are true (in the standard model $\mathbb{N}$), then of course $A_\tau={}$Con(PA${}+\tau$) will satisfy both the independence property and the monotonicity property.

(Lastly, for the record, let me say that I disagree with your characterization of the examples in my paper (Nonlinearity in the hierarchy of consistency strength). I proved there, for example, that there are tiling problem instances with incomparable consistency strength over ZFC. These problems are most directly about polygonal figures and whether they tile the plane, a kind of question most mathematicians find to be natural. Such a problem has nothing to do on its face with the minutia of any proof system or whether variables are Latin and Greek letters. Similarly, there are word problems in group theory with incomparable consistency strength, Game of Life problems, and so on. For any $m$-complete c.e. set $A$, I prove, there is a computable listing of problem instances of the form $n\notin A$ that are pairwise incomparable in consistency strength; and similarly for instances of the form $n\in A$. Let me add that I think you have no definition of "natural" and in that sense the questions at the end of your post are not well formulated mathematical questions.)