2026/04/30 by Hunter Monroe · 1 citation
Computer Science · Mathematics · #cs.CC #math.LO
We study when a sound arithmetic theory \mathcal S⊇ S12 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→ Con\mathcal S+ϕ, then \mathcal S interprets \mathcal S+ϕ, implying \mathcal S\vdash^nO(1)Con\mathcal S(p(n))→ Con\mathcal S+ϕ(n) for some polynomial p, and hence \mathcal S\vdash^nO(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 S12+ϕ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\vdashCon\mathcal S→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→ Con\mathcal S+ϕ, then for every constant c>0, \mathcal S\not\vdashncCon\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.