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 gives two unconditional constraints on 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 to simulate $S^1_2+φ_{BB}(k)$, where $φ_{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{\vdash}Con_{\mathcal S}{\rightarrow}Con_{\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\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 when $φ$ is $Con_{\mathcal S}$ or a Kolmogorov-randomness axiom. The latter yields further conjectural consequences and extensions.

翻译：暂无翻译