Toward a Characterization of Simulation Between Arithmetic Theories

Abstract

We study when a sound arithmetic theory $\mathcal{S}\supseteq S_2^1$ with polynomial-time decidable axioms efficiently proves the bounded consistency statements $Co{n}_{\mathcal{S}+\ddot{I}•}(n)$ for a true sentence $\ddot{I}•$. Equivalently, we ask when $\mathcal{S}$, viewed as a proof system, simulates $\mathcal{S}+\ddot{I}•$. The paper gives two unconditional constraints on possible characterizations. First, for finitely axiomatized sequential $\mathcal{S}$, if $EA⊢Co{n}_{\mathcal{S}}\to Co{n}_{\mathcal{S}+\ddot{I}•}$, then $\mathcal{S}$ interprets $\mathcal{S}+\ddot{I}•$, implying $\mathcal{S}{⊢}^{n^{O(1)}}Co{n}_{\mathcal{S}}(p(n))\to Co{n}_{\mathcal{S}+\ddot{I}•}(n)$ for some polynomial $p$, and hence $\mathcal{S}{⊢}^{n^{O(1)}}Co{n}_{\mathcal{S}+\ddot{I}•}(n)$. Second, if $\mathcal{S}$ fails to simulate $\mathcal{S}+\ddot{I}•$ for some true $\ddot{I}•$, then for all sufficiently large $k$ it also fails to simulate $S_2^1+\ddot{I}{•}_{BB}(k)$, where $\ddot{I}{•}_{BB}(k)$ asserts the exact value of the $k$-state Busy Beaver function. Thus any hard true extension yields a canonical Busy Beaver witness to nonsimulation. $\mathcal{B}$-certified simulation of a target $\mathcal{U}$ yields $\mathcal{B}⊢Co{n}_{\mathcal{S}}\to Co{n}_{\mathcal{U}}$, giving certification barriers rather than external lower bounds. The paper's central conjectural proposal is: for sound, finitely axiomatized sequential $\mathcal{S}$, if $EA/⊢Co{n}_{\mathcal{S}}\to Co{n}_{\mathcal{S}+\ddot{I}•}$, then for every constant $c>0$, $\mathcal{S}/{⊢}^{n^c}Co{n}_{\mathcal{S}+\ddot{I}•}(n)$. Under this proposal, hardness follows when $\ddot{I}•$ is $Co{n}_{\mathcal{S}}$ or a Kolmogorov-randomness axiom. The latter yields further conjectural consequences and extensions.

v2: KH and SETH-K-Finite are reformulated with the threshold EACon_SCon_{S+ϕ}, correcting the proof of HRC/KH; the no-mutual-help and density consequences are revised accordingly; figures and subsections on BB hardness and robustness are added

Topics & keywords