A Proposed Characterization of p-Simulation Between Theories

2025/07/17 by Hunter Monroe, Monroe, Hunter
Computer Science · Mathematics · #cs.CC #math.LO

paper · pdf · doi:10.48550/arxiv.2507.13576

Abstract

This paper proposes a characterization of when one axiomatic theory, as a proof system for tautologies, p-simulates another, by showing: (i)~if c.e. theory S efficiently interprets S+ϕ, then S p-simulates S+ϕ (Jeřábek in Pudlák17 proved simulation), since the interpretation maps an S+ϕ-proof whose lines are all theorems into an S-proof; (ii)~S proves ``S efficiently interprets S+ϕ'' iff S proves ``S p-simulates S+ϕ'' (if so, S already proves the Π₁ theorems of S+ϕ). To explore whether this framework conceivably resolves other open questions, the paper formulates conjectures stronger than ``no optimal proof system exists'' that imply Feige's Hypothesis, the existence of one-way functions, and circuit lower bounds.

Related

• Toward a Characterization of Simulation Between Arithmetic Theories
• Polynomial Identity Testing and the Ideal Proof System: PIT is in NP if and only if IPS can be p-simulated by a Cook-Reckhow proof system
• Exponential separations using guarded extension variables
• A robust proof-theoretic well-ordering
• Average-Case Hardness of Proving Tautologies and Theorems