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.

翻译：本文研究当声音算术理论 $\mathcal S{\supseteq}S^1_2$ 具有多项式时间可判定的公理时，它在何种条件下能高效证明真实语句 $φ$ 的有界一致性陈述 $Con_{\mathcal S{+}φ}(n)$。等价地，我们询问将 $\mathcal S$ 视为证明系统时，它能否模拟 $\mathcal S{+}φ$。本文的两项无条件贡献限制了可能的表征。首先，对于有限公理化的序列理论 $\mathcal S$，如果 $EA{\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}φ}$，那么 $\mathcal S$ 可解释 $\mathcal S{+}φ$，从而存在某个多项式 $p$ 使得 ${\mathcal S}{\vdash^{n^{O(1)}}}Con_{\mathcal S}(p(n)){\rightarrow}Con_{\mathcal S{+}φ}(n)$，进而有 ${\mathcal S}{\vdash^{n^{O(1)}}}Con_{\mathcal S{+}φ}(n)$。其次，如果对于某个真实 $φ$，$\mathcal S$ 无法模拟 $\mathcal S{+}φ$，那么对所有充分大的 $k$，它也无法模拟断言 $k$ 状态繁忙海狸函数精确值的 $φ_{BB}(k)$。非正式地说，任何表明 $\mathcal S$ 无法模拟某个 $\mathcal S{+}φ$ 的论证，都能产生不可证明的 $φ_{BB}(k)$ 来见证相同的障碍。这些结果表明相对一致性强度是判定模拟可能性的重要候选条件，但仍未明确这是否为正确准则。本文的核心猜想性提议是上述充分条件同时也是必要的：若 $EA{\not\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}φ}$，则对任意常数 $c{>}0$，有 ${\mathcal S}{\not\vdash^{n^c}}Con_{\mathcal S{+}φ}(n)$。在此提议下，当 $φ$ 是 $Con_{\mathcal S}$ 或柯尔莫哥洛夫随机性公理时，在典型情形中可推导出困难性。后者进一步产生了猜想性的推论与扩展。