View PDF HTML (experimental)

Abstract:We study the relationship between the existence of optimal proof systems and recursive jump operators, two central open problems in proof complexity. For a set L, an optimal proof system is a strongest proof system in terms of proof length, whereas a recursive jump operator uniformly transforms any proof system for L into a stronger one with respect to proof length, thereby witnessing non-optimality. It is clear that the existence of a recursive jump operator for L rules out optimal proof systems for L. Khaniki (FOCS 2024) is interested in the converse of this implication and explicitly poses the following question, where TAUT denotes the set of propositional tautologies.
Q: Does the non-existence of optimal proof systems for TAUT imply the existence of recursive jump operators for TAUT?
We generalize and address this question from both a relativized and an unrelativized perspective. We show that proving a positive answer for Q is provably hard by constructing the following oracle.
O: The polynomial-time hierarchy is infinite, TAUT has no optimal proof systems, and TAUT has no recursive jump operators.
This shows that Khaniki's question can not be answered in the positive by relativizable means, even under the standard complexity-theoretic assumption that the polynomial-time hierarchy is infinite.
In contrast, we obtain positive results when the question Q is posed for sets different from TAUT. We prove that the existence of recursive jump operators is upward closed under $\leq_{\text{m}}^{\text{p}}$-reducibility, a result that so far was only known for the non-existence of optimal proof systems. Furthermore, we show that the sets known to have no optimal proof systems by Messner (STACS 1999) in fact admit recursive jump operators. Thus, essentially all sets currently known to have no optimal proof systems have recursive jump operators.

Submission history

From: Fabian Egidy [view email]
[v1] Sun, 31 May 2026 13:49:41 UTC (125 KB)