pith. sign in

arxiv: 2606.01242 · v1 · pith:2U2E2RUPnew · submitted 2026-05-31 · 💻 cs.CC

Recursive Jump Operators and Optimal Proof Systems

Fabian Egidy This is my paper

Pith reviewed 2026-06-28 15:57 UTC · model grok-4.3

classification 💻 cs.CC
keywords optimal proof systemsrecursive jump operatorsTAUTrelativizationpolynomial hierarchyproof complexityoracle separation
0
0 comments X

The pith

An oracle shows that TAUT can lack both optimal proof systems and recursive jump operators even when the polynomial-time hierarchy is infinite.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines whether the absence of optimal proof systems for TAUT necessarily produces recursive jump operators for TAUT. It builds an oracle relative to which the polynomial-time hierarchy remains infinite, TAUT has no optimal proof systems, and TAUT also has no recursive jump operators. The construction demonstrates that any positive answer to this implication cannot be proved by relativizing arguments. For sets other than TAUT the paper proves that recursive jump operators are upward closed under polynomial-time many-one reductions and that every set previously shown to lack optimal proof systems does possess recursive jump operators.

Core claim

We construct an oracle O such that, relative to 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 Q cannot receive a positive answer by relativizable means, even under the assumption that the polynomial-time hierarchy is infinite.

What carries the argument

The oracle O that simultaneously enforces an infinite polynomial-time hierarchy, the non-existence of optimal proof systems for TAUT, and the non-existence of recursive jump operators for TAUT.

If this is right

  • Khaniki's question Q cannot be settled positively by any relativizing proof.
  • Existence of recursive jump operators is closed upward under polynomial-time many-one reductions.
  • Every set previously known to lack optimal proof systems (via Messner's results) in fact possesses recursive jump operators.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Any proof of the implication for TAUT would have to use non-relativizing techniques.
  • The separation may extend to other central objects in proof complexity that are currently studied only through relativization.
  • Similar oracles could be built to separate further pairs of non-existence statements while preserving standard assumptions such as an infinite hierarchy.

Load-bearing premise

A single oracle can be defined that makes the polynomial-time hierarchy infinite while also removing both optimal proof systems and recursive jump operators from TAUT without internal contradiction.

What would settle it

Either a relativizing proof that non-existence of optimal proof systems for TAUT implies existence of recursive jump operators for TAUT, or a proof that no oracle can satisfy all three properties at once.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper examines the relationship between optimal proof systems and recursive jump operators for TAUT and other sets in proof complexity. It constructs an oracle O such that the polynomial-time hierarchy is infinite, TAUT has no optimal proof systems, and TAUT has no recursive jump operators. This demonstrates that a positive answer to Khaniki's question Q (whether non-existence of optimal proof systems for TAUT implies existence of recursive jump operators) cannot be obtained via relativizing techniques, even assuming PH is infinite. It further proves that existence of recursive jump operators is upward closed under ≤_m^p-reducibility and that sets shown by Messner (STACS 1999) to lack optimal proof systems in fact possess recursive jump operators.

Significance. If the oracle construction is correct, the result establishes a relativized separation showing that the two notions are independent in a strong sense, even under standard assumptions like infinite PH; this limits the power of relativization for resolving Q. The upward-closure and positive results for non-TAUT sets provide new structural information about proof systems and extend prior work on non-existence of optimal proof systems. The manuscript ships an explicit oracle construction addressing the compatibility of the three properties.

minor comments (2)
  1. [Abstract] Abstract: the phrasing 'proving a positive answer for Q is provably hard' should be clarified to 'cannot be established by relativizable means' to avoid suggesting an absolute hardness result.
  2. [§2] §2 (Preliminaries): the definition of recursive jump operator could include an explicit reference to the proof-length ordering to make the contrast with optimal proof systems immediate.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our results on the oracle separating optimal proof systems and recursive jump operators for TAUT, even with infinite PH, and for recommending minor revision. The assessment that our work limits relativizing techniques for Khaniki's question Q is accurate. No specific major comments appear in the report, so we provide no point-by-point responses below.

Circularity Check

0 steps flagged

No circularity; explicit oracle construction is independent of target claim

full rationale

The derivation consists of a standard relativizing oracle construction that simultaneously enforces PH infinitude, absence of optimal proof systems for TAUT, and absence of recursive jump operators. This is achieved by diagonalization against external complexity assumptions rather than by redefining the target properties in terms of themselves or by fitting parameters to the conclusion. No self-citation is load-bearing for the central existence claim, and the construction is presented as evidence that a positive answer to Q cannot be obtained relativizably. The result is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the existence of a specific oracle with three simultaneous properties, constructed using standard techniques from relativized complexity theory. No new entities, free parameters, or ad-hoc axioms beyond background set theory are introduced.

axioms (1)
  • standard math ZFC set theory or equivalent foundations for defining oracles and relativized computations
    Standard background for all relativized complexity results.

pith-pipeline@v0.9.1-grok · 5857 in / 1222 out tokens · 37623 ms · 2026-06-28T15:57:41.731662+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

68 extracted references · 24 canonical work pages

  1. [1]

    2009 , isbn =

    Arora, Sanjeev and Barak, Boaz , title =. 2009 , isbn =

    2009

  2. [2]

    The polynomial-time hierarchy and sparse oracles , year =

    Balc\'. The polynomial-time hierarchy and sparse oracles , year =. J. ACM , month = may, pages =. doi:10.1145/5925.5937 , abstract =

    work page doi:10.1145/5925.5937

  3. [3]

    Bovet and Pierluigi Crescenzi and Riccardo Silvestri , doi =

    Daniel P. Bovet and Pierluigi Crescenzi and Riccardo Silvestri , doi =. Complexity Classes and Sparse Oracles , url =. Journal of Computer and System Sciences , number =

  4. [4]

    Beyersdorff , title =

    O. Beyersdorff , title =. Proceedings 24th International Conference on Foundations of Software Technology and Theoretical Computer Science , pages =. 2004 , series =

    2004

  5. [5]

    Beyersdorff , title =

    O. Beyersdorff , title =. Proceedings of Third International Conference on Theory and Applications of Models of Computation , pages =. 2006 , series =

    2006

  6. [6]

    Beyersdorff , title =

    O. Beyersdorff , title =. Theoretical Computer Science , volume =. 2007 , doi =

    2007

  7. [7]

    On the Existence of Complete Disjoint

    Beyersdorff, Olaf , booktitle=. On the Existence of Complete Disjoint. 2009 , volume=

    2009

  8. [8]

    Beyersdorff , title =

    O. Beyersdorff , title =. Theory of Computing Systems , volume =. 2010 , doi =

    2010

  9. [9]

    Baker and John Gill and Robert Solovay , title =

    Theodore P. Baker and John Gill and Robert Solovay , title =. 1975 , url =. doi:10.1137/0204037 , timestamp =

    work page doi:10.1137/0204037 1975

  10. [10]

    Nondeterministic functions and the existence of optimal proof systems , volume =

    Olaf Beyersdorff and Johannes Köbler and Jochen Messner , doi =. Nondeterministic functions and the existence of optimal proof systems , volume =. Theoretical Computer Science , keywords =

  11. [11]

    Proof systems that take advice , url =

    Olaf Beyersdorff and Johannes Köbler and Sebastian Müller , doi =. Proof systems that take advice , url =. Information and Computation , keywords =

  12. [12]

    Do there exist complete sets for promise classes? , volume =

    Olaf Beyersdorff and Zenon Sadowski , doi =. Do there exist complete sets for promise classes? , volume =. Mathematical Logic Quarterly , number =

  13. [13]

    Buss , school =

    Sam R. Buss , school =. Bounded Arithmetic , year =

  14. [14]

    Buss , title =

    Sam R. Buss , title =

  15. [15]

    On p-Optimal Proof Systems and Logics for PTIME

    Chen, Yijia and Flum, J \"o rg. On p-Optimal Proof Systems and Logics for PTIME. Automata, Languages and Programming. 2010. doi:10.1007/978-3-642-14162-1_27

    work page doi:10.1007/978-3-642-14162-1_27 2010

  16. [16]

    On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT

    Chen, Yijia and Flum, J \"o rg. On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT. Computer Science Logic. 2010. doi:10.1007/978-3-642-15205-4_18

    work page doi:10.1007/978-3-642-15205-4_18 2010

  17. [17]

    Hard Instances of Algorithms and Proof Systems , url =

    Chen, Yijia and Flum, J\". Hard Instances of Algorithms and Proof Systems , url =. ACM Trans. Comput. Theory , keywords =. doi:10.1145/2601336 , issn =

    work page doi:10.1145/2601336

  18. [18]

    Cook and Jan Krajíček , doi =

    Stephen A. Cook and Jan Krajíček , doi =. Consequences of the Provability of. The Journal of Symbolic Logic , number =

  19. [19]

    and Reckhow, Robert A

    Cook, Stephen A. and Reckhow, Robert A. , doi =. The relative efficiency of propositional proof systems , volume =. Journal of Symbolic Logic , pages =

  20. [20]

    An Oracle with no

    Dingel, David and Egidy, Fabian and Gla. An Oracle with no. 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) , pages =. 2024 , volume =

    2024

  21. [21]

    37th International Symposium on Theoretical Aspects of Computer Science,

    Titus Dose and Christian Gla. 37th International Symposium on Theoretical Aspects of Computer Science,. 2020 , doi =

    2020

  22. [22]

    Theoretical Computer Science , volume =

    Titus Dose , title =. Theoretical Computer Science , volume =. 2020 , doi =

    2020

  23. [23]

    Further oracles separating conjectures about incompleteness in the finite domain , volume =

    Titus Dose , doi =. Further oracles separating conjectures about incompleteness in the finite domain , volume =. Theoretical Computer Science , keywords =

  24. [24]

    Oracle with

    Ehrmanntraut, Anton and Egidy, Fabian and Gla. Oracle with. 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) , pages =. 2022 , volume =. doi:10.4230/LIPIcs.MFCS.2022.45 , annote =

    work page doi:10.4230/lipics.mfcs.2022.45 2022

  25. [25]

    Optimal Proof Systems for Complex Sets Are Hard to Find , year =

    Egidy, Fabian and Gla. Optimal Proof Systems for Complex Sets Are Hard to Find , year =. Proceedings of the 57th Annual ACM Symposium on Theory of Computing , pages =. doi:10.1145/3717823.3718182 , abstract =

    work page doi:10.1145/3717823.3718182

  26. [26]

    Fabian Egidy , year=. The. 2602.02294 , archivePrefix=

    arXiv

  27. [27]

    Are there interactive protocols for

    Lance Fortnow and Michael Sipser , keywords =. Are there interactive protocols for. Information Processing Letters , volume =. 1988 , issn =. doi:https://doi.org/10.1016/0020-0190(88)90199-8 , url =

    work page doi:10.1016/0020-0190(88)90199-8 1988

  28. [28]

    Selman and Nils Wisiol , title =

    Christian Glaßer and Andrew Hughes and Alan L. Selman and Nils Wisiol , title =. Aspects of Computation and Automata Theory with Applications , chapter =. 2023 , doi =

    2023

  29. [29]

    Grollmann and A

    J. Grollmann and A. L. Selman , title =. SIAM Journal on Computing , year = 1988, volume = 17, number = 2, pages =

    1988

  30. [30]

    Disjoint

    Christian Gla. Disjoint. SIAM Journal on Computing , year = 2004, volume = 33, number = 6, pages =

    2004

  31. [31]

    C. Gla. Canonical Disjoint. Theoretical Computer Science , volume =. 2007 , pages =

    2007

  32. [32]

    C. Gla. The Informational Content of Canonical Disjoint. International Journal of Foundations of Computer Science , volume =. 2009 , doi =

    2009

  33. [33]

    , title =

    Hirsch, Edward A. , title =. Proceedings of the 7th Annual Conference on Theory and Applications of Models of Computation , pages =. 2010 , isbn =. doi:10.1007/978-3-642-13562-0_4 , abstract =

    work page doi:10.1007/978-3-642-13562-0_4 2010

  34. [34]

    38th Computational Complexity Conference (CCC 2023) , pages =

    Hirahara, Shuichi and Lu, Zhenjian and Ren, Hanlin , title =. 38th Computational Complexity Conference (CCC 2023) , pages =. 2023 , volume =. doi:10.4230/LIPIcs.CCC.2023.6 , annote =

    work page doi:10.4230/lipics.ccc.2023.6 2023

  35. [35]

    and Rubinstein, Roy S

    Hemachandra, Lane A. and Rubinstein, Roy S. , title =. 1992 , issue_date =. doi:10.1016/0304-3975(92)90318-A , journal =

    work page doi:10.1016/0304-3975(92)90318-a 1992

  36. [36]

    An Average-Case Depth Hierarchy Theorem for Boolean Circuits , year =

    H. An Average-Case Depth Hierarchy Theorem for Boolean Circuits , year =. Journal of the ACM , month = aug, articleno =. doi:10.1145/3095799 , abstract =

    work page doi:10.1145/3095799

  37. [37]

    and Sekoni, Adewale and Shafei, Hadi , title =

    Hitchcock, John M. and Sekoni, Adewale and Shafei, Hadi , title =. ACM Trans. Comput. Theory , month = jan, articleno =. 2021 , issue_date =. doi:10.1145/3434389 , abstract =

    work page doi:10.1145/3434389 2021

  38. [38]

    New relations and separations of conjectures about incompleteness in the finite domain , volume =

    Khaniki, Erfan , doi =. New relations and separations of conjectures about incompleteness in the finite domain , volume =. The Journal of Symbolic Logic , number =

  39. [39]

    Jump Operators, Interactive Proofs and Proof Complexity Generators , year=

    Khaniki, Erfan , booktitle=. Jump Operators, Interactive Proofs and Proof Complexity Generators , year=

  40. [40]

    and Lipton, Richard J

    Karp, Richard M. and Lipton, Richard J. , booktitle =. Some connections between nonuniform and uniform complexity classes , url =. doi:10.1145/800141.804678 , isbn =

    work page doi:10.1145/800141.804678

  41. [41]

    The Journal of Symbolic Logic , year =

    Kleene, Stephen Cole , title =. The Journal of Symbolic Logic , year =

  42. [42]

    1952 , address =

    Kleene, Stephen Cole , title =. 1952 , address =

    1952

  43. [43]

    Complete problems for promise classes by optimal proof systems for test sets , url =

    Johannes K. Complete problems for promise classes by optimal proof systems for test sets , url =. Proceedings of the 13th Annual. doi:10.1109/CCC.1998.694599 , pages =

    work page doi:10.1109/ccc.1998.694599 1998

  44. [44]

    Optimal proof systems imply complete sets for promise classes , volume =

    Johannes Köbler and Jochen Messner and Jacobo Torán , doi =. Optimal proof systems imply complete sets for promise classes , volume =. Information and Computation , keywords =

  45. [45]

    SIAM Journal on Computing , volume =

    Ko, Ker-I , title =. SIAM Journal on Computing , volume =. 1989 , doi =

    1989

  46. [46]

    Propositional proof systems, the consistency of first order theories and the complexity of computations , volume =

    Jan Krajíček and Pavel Pudl. Propositional proof systems, the consistency of first order theories and the complexity of computations , volume =. doi:10.2307/2274765 , journal =

    work page doi:10.2307/2274765

  47. [47]

    Journal of Symbolic Logic , author=

    Implicit proofs , volume=. Journal of Symbolic Logic , author=. 2004 , pages=. doi:10.2178/jsl/1082418532 , number=

    work page doi:10.2178/jsl/1082418532 2004

  48. [48]

    Diagonalization in proof complexity , volume =

    Jan Krajíček , year =. Diagonalization in proof complexity , volume =. Fundamenta Mathematicae , doi =

  49. [49]

    Proof Complexity , DOI=

    Krajíček, Jan , year=. Proof Complexity , DOI=

  50. [50]

    Krajíček, J. , year=. Bounded Arithmetic, Propositional Logic and Complexity Theory , DOI=

  51. [51]

    Journal of Computer and System Sciences , volume =

    Turing machines with few accepting computations and low sets for. Journal of Computer and System Sciences , volume =. 1992 , issn =. doi:https://doi.org/10.1016/0022-0000(92)90022-B , url =

    work page doi:10.1016/0022-0000(92)90022-b 1992

  52. [52]

    and Selman, Alan L

    Long, Timothy J. and Selman, Alan L. , doi =. Relativizing complexity classes with sparse oracles , url =. Journal of the ACM , number =

  53. [53]

    , booktitle =

    Lutz, Jack H. , booktitle =. The quantitative structure of exponential time , year =

  54. [54]

    On the Simulation Order of Proof Systems , year =

    Jochen Messner , school =. On the Simulation Order of Proof Systems , year =

  55. [55]

    On Optimal Algorithms and Optimal Proof Systems , year =

    Jochen Messner , booktitle =. On Optimal Algorithms and Optimal Proof Systems , year =. doi:10.1007/3-540-49116-3_51 , pages =

    work page doi:10.1007/3-540-49116-3_51

  56. [56]

    Learning Algorithms Versus Automatability of Frege Systems , booktitle =

    Pich, J\'. Learning Algorithms Versus Automatability of Frege Systems , booktitle =. 2022 , volume =. doi:10.4230/LIPIcs.ICALP.2022.101 , annote =

    work page doi:10.4230/lipics.icalp.2022.101 2022

  57. [57]

    P. Pudl. On reducibility and symmetry of disjoint. Theoretical Computer Science , volume =. 2003 , pages =

    2003

  58. [58]

    Incompleteness in the Finite Domain , volume =

    Pavel Pudl. Incompleteness in the Finite Domain , volume =. doi:10.1017/bsl.2017.32 , journal =

    work page doi:10.1017/bsl.2017.32 2017

  59. [59]

    Pudlák , year=

    P. Pudlák , year=. The lengths of proofs , editor =. Handbook of Proof Theory , publisher=

  60. [60]

    1994 , number =

    Alexander Razborov , title =. 1994 , number =

    1994

  61. [61]

    On an optimal quantified propositional proof system and a complete language for

    Zenon Sadowski , bibsource =. On an optimal quantified propositional proof system and a complete language for. Fundamentals of Computation Theory , doi =

  62. [62]

    On an Optimal Deterministic Algorithm for SAT , year =

    Sadowski, Zenon , booktitle =. On an Optimal Deterministic Algorithm for SAT , year =. doi:https://doi.org/10.1007/10703163_13 , isbn =

    work page doi:10.1007/10703163_13

  63. [63]

    A. L. Selman , title =. Information and Computation , year = 1988, volume = 78, pages =

    1988

  64. [64]

    Journal of the ACM , month = oct, pages =

    Shamir, Adi , title =. Journal of the ACM , month = oct, pages =. 1992 , issue_date =. doi:10.1145/146585.146609 , abstract =

    work page doi:10.1145/146585.146609 1992

  65. [65]

    On Some Subrecursive Reducibilities

    Simon, István , school =. On Some Subrecursive Reducibilities. , year =

  66. [66]

    , title =

    Soare, Robert I. , title =. 1987 , doi =

    1987

  67. [67]

    SIAM Journal on Computing , volume =

    Tang, Shouwen and Watanabe, Osamu , title =. SIAM Journal on Computing , volume =. 1989 , doi =

    1989

  68. [68]

    Separating the polynomial-time hierarchy by oracles , url =

    Yao, Andrew , booktitle =. Separating the polynomial-time hierarchy by oracles , url =. doi:10.1109/SFCS.1985.49 , isbn =

    work page doi:10.1109/sfcs.1985.49 1985