Toward a Characterization of Simulation Between Arithmetic Theories

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}+\phi }(n)$ for a true sentence $\phi$. Equivalently, we ask when $\mathcal{S}$, viewed as a proof system, simulates $\mathcal{S}+\phi$. 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}+\phi }$, then $\mathcal{S}$ interprets $\mathcal{S}+\phi$, implying $\mathcal{S}{⊢}^{n^{O(1)}}Co{n}_{\mathcal{S}}(p(n))\to Co{n}_{\mathcal{S}+\phi }(n)$ for some polynomial $p$, and hence $\mathcal{S}{⊢}^{n^{O(1)}}Co{n}_{\mathcal{S}+\phi }(n)$. Second, if $\mathcal{S}$ fails to simulate $\mathcal{S}+\phi$ for some true $\phi$, then for all sufficiently large $k$ it also fails to simulate $S_2^1+{\phi }_{BB}(k)$, where ${\phi }_{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}+\phi }$, then for every constant $c>0$, $\mathcal{S}\mathrm{̸}{⊢}^{n^c}Co{n}_{\mathcal{S}+\phi }(n)$. Under this proposal, hardness follows when $\phi$ is $Co{n}_{\mathcal{S}}$ or a Kolmogorov-randomness axiom. The latter yields further conjectural consequences and extensions.