Toward a Characterization of Simulation Between Arithmetic Theories
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2604.27787
curl -X POST /api/v1/records/arxiv/2604.27787/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2604.27787/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'