The SPARSE-Relativization Framework and Applications to Optimal Proof Systems

TL;DR

This paper introduces the SPARSE-relativization framework to analyze the existence of optimal proof systems for tautologies and QBF, providing new oracle results that demonstrate independence and barriers for these longstanding open questions.

Contribution

The paper develops the SPARSE-relativization framework, enabling the construction of sparse oracles that establish new independence and barrier results for optimal proof systems.

Findings

No set in PSPACE∩NP has optimal proof systems under certain oracle conditions.

All sets in PSPACE have p-optimal proof systems in a different oracle setting.

Questions about the existence of optimal proof systems are independent of the polynomial hierarchy.

Abstract

We investigate the following longstanding open questions raised by Kraj\'i\v{c}ek and Pudl\'ak (J. Symb. L. 1989), Sadowski (FCT 1997), K\"obler and Messner (CCC 1998) and Messner (PhD 2000). Q1: Does TAUT have (p-)optimal proof systems? Q2: Does QBF have (p-)optimal proof systems? Q3: Are there arbitrarily complex sets with (p-)optimal proof systems? Recently, Egidy and Gla{\ss}er (STOC 2025) contributed to these questions by constructing oracles that show that there are no relativizable proofs for positive answers of these questions, even when assuming well-established conjectures about the separation of complexity classes. We continue this line of research by providing the same proof barrier for negative answers of these questions. For this, we introduce the SPARSE-relativization framework, which is an application of the notion of bounded relativization by Hirahara, Lu, and Ren (CCC 2023). This framework allows the construction of sparse oracles for statements such that additional useful properties (like an infinite polynomial-time hierarchy) hold. By applying the SPARSE-relativization framework, we show that the oracle construction of Egidy and Gla{\ss}er also yields the following new oracle. O1: No set in PSPACE\NP has optimal proof systems, $\mathrm{NP} \subsetneq \mathrm{PH} \subsetneq \mathrm{PSPACE}$, and PH collapses We use techniques of Cook and Kraj\'i\v{c}ek (J. Symb. L. 2007) and Beyersdorff, K\"obler, and M\"uller (Inf. Comp. 2011) and apply our SPARSE-relativization framework to obtain the following new oracle. O2: All sets in PSPACE have p-optimal proof systems, there are arbitrarily complex sets with p-optimal proof systems, and PH is infinite Together with previous results, our oracles show that questions Q1 and Q2 are independent of an infinite or collapsing polynomial-time hierarchy.