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.
翻译:我们研究了最优证明系统的存在性与递归跳跃算子之间的关系,这是证明复杂性中两个核心未解问题。对于集合L,最优证明系统是指在证明长度方面最强的证明系统,而递归跳跃算子则能将L的任何证明系统一致地转化为一个在证明长度上更强的系统,从而表明其非最优性。显然,L上递归跳跃算子的存在排除了L的最优证明系统。Khaniki(FOCS 2024)对该蕴涵的逆命题感兴趣,并明确提出了以下问题,其中TAUT表示命题重言式集合。问:TAUT不存在最优证明系统是否蕴涵TAUT存在递归跳跃算子?我们从相对化和非相对化两个角度对该问题进行了推广和研究。我们通过构造以下谕示证明了Q的肯定回答是难以证明的。O:多项式层次是无穷的,TAUT没有最优证明系统,且TAUT没有递归跳跃算子。这表明,即使在标准复杂性理论假设(多项式层次无穷)下,Khaniki的问题也无法通过相对化方法得到肯定回答。相比之下,当问题Q针对不同于TAUT的集合提出时,我们得到了肯定结果。我们证明了递归跳跃算子的存在性在$\leq_{\text{m}}^{\text{p}}$-可归约性下向上封闭,这一结果此前仅对最优证明系统的不存在性成立。此外,我们证明了Messner(STACS 1999)已知没有最优证明系统的集合实际上承认递归跳跃算子。因此,当前已知没有最优证明系统的所有集合本质上都具有递归跳跃算子。