{"id":"arxiv/2604.27787","url":"https://arxiv.org/abs/2604.27787","tags":["cs.CC","math.LO"],"score":0,"title":"Toward a Characterization of Simulation Between Arithmetic Theories","domain":"cs.CC","source":"arxiv","authors":["Hunter Monroe"],"reviews":0,"subject":"cs.CC","summary":"We study when a sound arithmetic theory $\\mathcal S{\\supseteq}S^1_2$ with polynomial-time decidable axioms has polynomial-size proofs of $Con_{\\mathcal S{+}φ}(n)$ for a true sentence $φ$. 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^1_2{+}\\mathsf{Exp}{+}φ_{BB}(k)$ for all sufficiently large $k$. Here $φ_{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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-04-30","reactions":{}}