Toward a Characterization of Simulation Between Arithmetic Theories
For researchers in proof complexity and arithmetic, this work provides a candidate characterization of when one theory simulates another, with implications for the hardness of consistency statements.
The paper characterizes when a sound arithmetic theory S with polynomial-time decidable axioms efficiently proves bounded consistency statements for a true sentence φ, showing that if EA proves Con_S → Con_{S+φ} then S interprets S+φ and efficiently proves Con_{S+φ}(n), and if S fails to simulate S+φ for some true φ then it also fails for Busy Beaver statements. The central conjecture is that the sufficient condition is also necessary.
We study when a sound arithmetic theory $\mathcal S{\supseteq}S^1_2$ with polynomial-time decidable axioms efficiently proves the bounded consistency statements $Con_{\mathcal S{+}ϕ}(n)$ for a true sentence $ϕ$. Equivalently, we ask when $\mathcal S$, viewed as a proof system, simulates $\mathcal S{+}ϕ$. The paper's two unconditional contributions constrain possible characterizations. First, for finitely axiomatized sequential $\mathcal S$, if $EA{\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}ϕ}$, then $\mathcal S$ interprets $\mathcal S{+}ϕ$, implying ${\mathcal S}{\vdash^{n^{O(1)}}}Con_{\mathcal S}(p(n)){\rightarrow}Con_{\mathcal S{+}ϕ}(n)$ for some polynomial $p$, and hence ${\mathcal S}{\vdash^{n^{O(1)}}}Con_{\mathcal S{+}ϕ}(n)$. Second, if $\mathcal S$ fails to simulate $\mathcal S{+}ϕ$ for some true $ϕ$, then for all sufficiently large $k$ it also fails for $ϕ_{BB}(k)$ asserting the exact value of the $k$-state Busy Beaver function. Informally, any argument showing that $\mathcal S$ fails to simulate some $\mathcal S{+}ϕ$ also yields unprovable $ϕ_{BB}(k)$ witnessing the same obstruction. These results suggest that relative consistency strength is a serious candidate for governing when simulation is possible, while leaving open whether it is the correct criterion. The paper's central conjectural proposal is that the above sufficient condition is also necessary: if $EA{\not\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}ϕ}$, then for every constant $c{>}0$, ${\mathcal S}{\not\vdash^{n^c}}Con_{\mathcal S{+}ϕ}(n)$. Under this proposal, hardness follows in canonical cases where $ϕ$ is $Con_{\mathcal S}$ or a Kolmogorov-randomness axiom. The latter yields further conjectural consequences and extensions.