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 has polynomial-size proofs of $Co{n}_{\mathcal{S}+\varphi }(n)$ for a true sentence $\varphi$. Our structural result characterizes the nonexistence of a length-optimal propositional proof system: it is equivalent to every such $\mathcal{S}$ failing to simulate $S_2^1+\mathsf{Exp}+{\varphi }_{BB}(k)$ for all sufficiently large $k$. Here ${\varphi }_{BB}(k)$ asserts the exact $k$-state Busy Beaver value, and $\mathsf{Exp}$ asserts total exponentiation. Combining the Krajíček--Pudlák correspondence with our transfer theorem proves this equivalence. For fixed $\mathcal{S}$, a true extension not simulated by $\mathcal{S}$ exists if and only if eventual Busy Beaver non-simulation holds. A finite version transfers lower bounds to Busy Beaver instances with explicit parameter changes and proof-length bounds. For finitely axiomatized sequential $\mathcal{S}$, we prove that $S_2^1⊢Co{n}_{\mathcal{S}}\to Co{n}_{\mathcal{S}+\varphi }$ implies simulation. We refute the earlier conjecture that the corresponding $EA$ implication characterizes simulation. For these finitely axiomatized sequential theories, the Kolmogorov Blindness conjecture predicts exponential proof-length lower bounds for bounded consistency of true logarithmic-deficiency randomness extensions $x\in R^{\log }$, with an encoding-dependent rate and an onset common to all strings of each sufficiently large length. It predicts the same hardness after adjoining a true randomness axiom $y\in R^{\log }$ of equal length, provided $x$ remains random conditional on $y$. For fixed ${\Pi }_1$ axiom families with computable proof-length bounds and a common computable onset, we prove a quantitative equivalence between dense hardness with polynomially small exceptional fractions and hardness above a corresponding Kolmogorov-complexity threshold.

arXiv commentv4: Corrects relative consistency using $S_2^1$ and Busy Beaver transfer using $S_2^1+\mathsf{Exp}$; refutes the earlier Higher Relative Consistency conjecture; adds a Busy Beaver characterization of the nonexistence of length-optimal proof systems, finite transfer, and a quantitative density--randomness equivalence; consolidates the conjectures around Kolmogorov Blindness