pith. sign in

arxiv: 2606.27931 · v1 · pith:AGES4OYLnew · submitted 2026-06-26 · 💻 cs.CC

Provable Reductions in TFNP

Noah Fleming , Stefan Grosser , Toniann Pitassi , Robert Robere This is my paper

Pith reviewed 2026-06-29 02:15 UTC · model grok-4.3

classification 💻 cs.CC
keywords TFNPproof complexityExtended Fregesequent calculus G1implicit proof systemsPLSbounded arithmeticwitnessing theorems
0
0 comments X

The pith

The <EF, Iter> proof system is polynomially equivalent to the sequent calculus G1 and to the implicit Resolution system [EF, Resolution].

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

The paper defines a family of proof systems for any TFNP search problem R. A refutation in consists of a polynomial-time reduction from the search problem of finding a false clause in a CNF formula to the problem R, together with an Extended Frege proof that the reduction is correct. For the specific case where R is the Iter problem, which is complete for the class PLS, the authors prove that has exactly the same polynomial power as the sequent calculus G1 and as the implicit proof system [EF, Resolution]. This yields the first equivalence between an implicit proof system and a classical one beyond prior results. They also show that collapses to plain Extended Frege whenever EF can prove that R lies in FP, and that every sufficiently strong proof system P arises as for some polynomial-time computable R_P.

Core claim

We prove that <EF, Iter> is polynomially equivalent to the sequent calculus G1, and also to the implicit Resolution proof system [EF, Resolution]. Hence G1 and [EF, Resolution] are equivalent, which is the first characterization of an implicit proof system by a classical proof system beyond the work of Wang. We also consider <EF, R> for general TFNP relations R. We observe that if EF can prove that a search problem R is in FP, then <EF, R> is polynomially equivalent to EF. Finally, we show that for any proof system P which is sufficiently strong, there is a polynomial-time computable search problem R_P in FP such that <EF, R_P> is polynomially equivalent to P.

What carries the argument

The <EF, R> proof system, defined by a polynomial-time reduction from the false-clause search problem Search_F to the TFNP problem R together with an Extended Frege proof that the reduction is correct.

If this is right

  • G1 and [EF, Resolution] are polynomially equivalent.
  • If EF proves that a search problem R is in FP then <EF, R> is polynomially equivalent to EF.
  • For any sufficiently strong proof system P there exists an R_P in FP such that <EF, R_P> is polynomially equivalent to P.
  • <EF, Iter> is polynomially equivalent to <EF, R_{[EF, Resolution]}>.

Where Pith is reading between the lines

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

  • Similar equivalences might be provable when Iter is replaced by other TFNP-complete problems such as those for PPA or PPAD.
  • The bounded-arithmetic motivation suggests that lower bounds on G1 could transfer to lower bounds on certain witnessing theorems in bounded arithmetic.
  • The construction of R_P for arbitrary P offers a uniform way to embed any proof system into the <EF, R> framework using only FP search problems.

Load-bearing premise

The equivalence proofs rest on the existence of a specific polynomial-time reduction from Search_F to Iter whose correctness is provable in Extended Frege.

What would settle it

A CNF formula that admits a polynomial-size refutation in G1 but for which no polynomial-time reduction to Iter has a polynomial-size Extended Frege proof of correctness, or vice versa.

Figures

Figures reproduced from arXiv: 2606.27931 by Noah Fleming, Robert Robere, Stefan Grosser, Toniann Pitassi.

Figure 1
Figure 1. Figure 1: The structure of the implicit Resolution proof of [PITH_FULL_IMAGE:figures/full_fig_p028_1.png] view at source ↗
read the original abstract

We introduce a new family of propositional proof systems, denoted <EF, R>, for an arbitrary TFNP search problem $R$. Informally, a refutation of a CNF formula $F$ in <EF, R> is given by a polynomial-time reduction from the false-clause search problem $Search_F$ to $R$, combined with an Extended Frege proof that the reduction is correct. These are motivated in two ways: 1. They are the propositional translations of witnessing theorems in bounded arithmetic, by which proofs of $\forall \Sigma^b_1$ formulas $\phi$ in a theory $T$ imply algorithms solving the search problem for $\phi$ in a TFNP class corresponding to $T$. 2. They are a white-box analogue of the characterizations of proof systems using decision tree reductions to black-box TFNP problems. We consider the proof system <EF, Iter>, where Iter is a complete problem for PLS. We prove that <EF, Iter> is polynomially equivalent to the sequent calculus $G_1$, and also to the implicit Resolution proof system [EF, Resolution]. Hence $G_1$ and [EF, Resolution] are equivalent, which is the first characterization of an implicit proof system by a classical proof system beyond the work of Wang. We also consider <EF, R> for general TFNP relations $R$. We observe that if EF can prove that a search problem $R$ is in FP, then <EF, R> is polynomially equivalent to EF. This contrasts to our above result, which shows that Extended-Frege provable reductions to $Iter$, a problem widely believed not to be in FP, yields a proof system ($G_1$) that is believed to be stronger than Extended Frege. Finally, we show that for any proof system $P$ which is sufficiently strong, there is a polynomial-time computable search problem $R_P \in $ FP such that <EF, $R_P$> is polynomially equivalent to $P$. Letting $P =$ [EF, Resolution] and combining our two results shows that <EF, Iter> is polynomially equivalent to <EF, $R_{[EF, Resolution]}$>.

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

1 major / 2 minor

Summary. The paper introduces a new family of propositional proof systems <EF, R> for TFNP search problems R. A refutation in <EF, R> consists of a polynomial-time reduction from the search problem Search_F to R, together with an Extended Frege proof that the reduction is correct. The main result is that <EF, Iter> is polynomially equivalent to the sequent calculus G1 and to the implicit proof system [EF, Resolution]. Additional results include conditions under which <EF, R> collapses to EF and a general construction showing that for sufficiently strong proof systems P there exists an FP search problem R_P such that <EF, R_P> is equivalent to P.

Significance. If the claimed equivalences hold via explicit constructions, this work significantly advances the understanding of implicit proof systems by providing their first characterization in terms of a classical proof system. It also connects propositional proof complexity with bounded arithmetic through witnessing theorems and TFNP problems. The observation that reductions to PLS-complete problems can yield systems stronger than EF, while reductions to FP problems collapse to EF, is a valuable distinction. The general result for arbitrary P further strengthens the framework.

major comments (1)
  1. [Abstract, motivation and results paragraphs] Abstract, motivation and results paragraphs: The polynomial equivalence of <EF, Iter> to G1 rests on exhibiting a polynomial-time reduction from Search_F to Iter whose correctness is provable in EF with polynomial proof size relative to G1 proofs. The manuscript must detail this reduction and the corresponding EF proof to substantiate the equivalence claim; without explicit construction, the simulation in one direction cannot be verified.
minor comments (2)
  1. The abstract mentions 'the first characterization of an implicit proof system by a classical proof system beyond the work of Wang' but does not provide a citation for Wang's work.
  2. Clarify the definition of the implicit proof system [EF, Resolution] with a brief example or reference to prior work.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the importance of explicit constructions to support the claimed equivalences. We address the major comment below and will revise the manuscript to strengthen the presentation.

read point-by-point responses

  1. Referee: The polynomial equivalence of <EF, Iter> to G1 rests on exhibiting a polynomial-time reduction from Search_F to Iter whose correctness is provable in EF with polynomial proof size relative to G1 proofs. The manuscript must detail this reduction and the corresponding EF proof to substantiate the equivalence claim; without explicit construction, the simulation in one direction cannot be verified.

    Authors: We agree that the equivalence claim requires an explicit construction for verification. While the manuscript outlines the existence of a polynomial-time reduction from Search_F to Iter together with an EF proof of correctness (of size polynomial in the G1 proof), we acknowledge that the current presentation is high-level and does not provide the full step-by-step details. In the revised manuscript we will expand the relevant section (likely Section 4 or 5) to include the complete description of the reduction, the encoding of the Iter instance, and the full EF derivation establishing correctness, making the polynomial simulation explicit in both directions. revision: yes

Circularity Check

0 steps flagged

No circularity: equivalences via explicit constructions between independent systems

full rationale

The paper defines <EF, R> as reductions from Search_F to R accompanied by EF proofs of correctness, motivated independently by bounded arithmetic translations and white-box TFNP characterizations. It then exhibits explicit polynomial-time reductions (with size bounds) in both directions to establish polynomial equivalence of <EF, Iter> to the independently defined sequent calculus G1 and to [EF, Resolution]. G1 is a standard classical system whose rules are not defined in terms of Iter or the new system. No step reduces a claimed prediction or equivalence to a fitted parameter, self-citation, or ansatz imported from the authors' prior work; the final observation constructing R_P in FP for arbitrary P is a separate general result and does not collapse the main equivalences. The derivation is self-contained against external benchmarks (G1, standard TFNP problems like Iter).

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard background from complexity theory and proof theory with no new free parameters or invented entities introduced in the abstract.

axioms (2)
  • domain assumption Iter is PLS-complete
    Invoked to define the specific system <EF, Iter> and its equivalence claims.
  • standard math Standard properties of Extended Frege proofs and TFNP search problems
    Background assumptions for defining reductions and their EF-verifiability.

pith-pipeline@v0.9.1-grok · 5956 in / 1466 out tokens · 59961 ms · 2026-06-29T02:15:49.259913+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

15 extracted references · 1 linked inside Pith

  1. [1]

    From proof complexity to circuit complexity via interactive protocols

    [AKPS24] Noel Arteche, Erfan Khaniki, J ´an Pich, and Rahul Santhanam. From proof complexity to circuit complexity via interactive protocols. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors,51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8- 12, 2024, Tallinn, Estonia, volume 297 ofLIPIcs,...

    2024

  2. [2]

    TFNP characterizations of proof systems and monotone circuits

    [BFI23] Sam Buss, Noah Fleming, and Russell Impagliazzo. TFNP characterizations of proof systems and monotone circuits. In Yael Tauman Kalai, editor,14th Innovations in Theoretical Computer Science Conference, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 ofLIPIcs, pages 30:1–30:40. Schloss Dagstuhl - Leibniz-Zentrum f¨ur ...

    2023

  3. [3]

    Colourful TFNP and propositional proofs

    [DR23] Ben Davis and Robert Robere. Colourful TFNP and propositional proofs. In Amnon Ta-Shma, editor,38th Computational Complexity Conference, CCC 2023, July 17-20, 2023, Warwick, UK, volume 264 ofLIPIcs, pages 36:1– 36:21. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik,

    2023

  4. [4]

    Separations above TFNP from sherali-adams lower bounds.CoRR, abs/2602.16810,

    36 [FGIM26] Noah Fleming, Anna G ´al, Deniz Imrek, and Christophe Marciot. Separations above TFNP from sherali-adams lower bounds.CoRR, abs/2602.16810,

    Pith/arXiv arXiv

  5. [5]

    Total search problems in ZPP

    [FGJ+26] Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Mor- gan Shirley, and Weiqiang Yuan. Total search problems in ZPP. In Shubhangi Saraf, editor,17th Innovations in Theoretical Computer Science Conference, ITCS 2026, Bocconi University, Milan, Italy, January 27-30, 2026, LIPIcs, pages 60:1–60:26. Schloss Dagstuhl - Leibniz-Zent...

    2026

  6. [6]

    Black-box PPP is not turing-closed

    [FGPR24] Noah Fleming, Stefan Grosser, Toniann Pitassi, and Robert Robere. Black-box PPP is not turing-closed. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors,Proceedings of the 56th Annual ACM Symposium on Theory of Com- puting, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1405–

    2024

  7. [7]

    Provably total func- tions in the polynomial hierarchy

    [FIM25] Noah Fleming, Deniz Imrek, and Christophe Marciot. Provably total func- tions in the polynomial hierarchy. In Srikanth Srinivasan, editor,40th Com- putational Complexity Conference, CCC 2025, Toronto, Canada, August 5-8, 2025, LIPIcs, pages 28:1–28:40. Schloss Dagstuhl - Leibniz-Zentrum f ¨ur In- formatik,

    2025

  8. [8]

    Separations in proof complexity and TFNP

    [GHJ+22b] Mika G ¨o¨os, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP. In63rd IEEE Annual Symposium on Foundations of Computer Sci- ence, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 1150–1161. IEEE,

    2022

  9. [9]

    Adven- tures in monotone complexity and TFNP

    [GKRS19] Mika G ¨o¨os, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adven- tures in monotone complexity and TFNP. In10th Innovations in Theoret- ical Computer Science Conference (ITCS 2019), volume 124 ofLeibniz In- ternational Proceedings in Informatics (LIPIcs), pages 38:1–38:19. Schloss Dagstuhl–Leibniz-Zentrum f¨ur Informatik,

    2019

  10. [10]

    Supercritical tradeoffs for monotone circuits

    [GMRS25] Mika G ¨o¨os, Gilbert Maystre, Kilian Risse, and Dmitry Sokolov. Supercritical tradeoffs for monotone circuits. In Michal Kouck´y and Nikhil Bansal, editors, 37 Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC 2025, Prague, Czechia, June 23-27, 2025, pages 1359–1370. ACM,

    2025

  11. [11]

    TFNP intersections through the lens of feasible disjunction

    [HKT24] Pavel Hub ´acek, Erfan Khaniki, and Neil Thapen. TFNP intersections through the lens of feasible disjunction. In Venkatesan Guruswami, editor,15th In- novations in Theoretical Computer Science Conference, ITCS 2024, Berkeley, CA, USA, January 30 - February 2, 2024, LIPIcs, pages 63:1–63:24. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik,

    2024

  12. [12]

    Jump operators, interactive proofs and proof complexity gen- erators.2024 IEEE 65th Annual Symposium on Foundations of Computer Sci- ence (FOCS), pages 573–593,

    [Kha24] Erfan Khaniki. Jump operators, interactive proofs and proof complexity gen- erators.2024 IEEE 65th Annual Symposium on Foundations of Computer Sci- ence (FOCS), pages 573–593,

    2024

  13. [13]

    Metamathematics of resolution lower bounds: A tfnp perspective.arXiv preprint arXiv:2411.15515,

    [LLR24] Jiawei Li, Yuhao Li, and Hanlin Ren. Metamathematics of resolution lower bounds: A tfnp perspective.arXiv preprint arXiv:2411.15515,

    arXiv

  14. [14]

    Intersection classes in TFNP and proof complexity

    [LPR24] Yuhao Li, William Pires, and Robert Robere. Intersection classes in TFNP and proof complexity. In Venkatesan Guruswami, editor,15th Innovations in Theoretical Computer Science Conference, ITCS 2024, Berkeley, CA, USA, January 30 - February 2, 2024, LIPIcs, pages 74:1–74:22. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik,

    2024

  15. [15]

    The provably total search problems of bounded arithmetic.submitted (preprint 2008),

    [ST07] Alan Skelley and Neil Thapen. The provably total search problems of bounded arithmetic.submitted (preprint 2008),

    2008