{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreib7jchm7aayi5txt4hv3hpmysc5wsxfa77sfzqdq5ugpeoe43ryze",
    "uri": "at://did:plc:4rgrdigiftglskeax4wvmsev/app.bsky.feed.post/3mpe24ik23bd2"
  },
  "path": "/report/2026/109",
  "publishedAt": "2026-06-28T10:23:51.000Z",
  "site": "https://eccc.weizmann.ac.il",
  "textContent": "We introduce a new family of propositional proof systems, denoted $\\langle EF, R \\rangle$, for an arbitrary TFNP search problem $R$. Informally, a refutation of a CNF formula $F$ in $\\langle EF, R \\rangle$ is given by a polynomial-time mapping reduction from the false-clause search problem ${\\mathrm{Search}}_F$ to $R$, combined with an Extended Frege proof that the reduction is correct. These new systems are naturally motivated in two ways:\n\n1. 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 subclass corresponding to $T$ [Bus86, KP90, BK94, KST07, BB09].\n\n2. They form a white-box analogue of the recent characterizations of proof systems using decision tree reductions to black-box TFNP problems [GHJ+22b, BIK+94, DR23, LPR24, FGJ+26, FIM25].\n\n    We consider the proof system $\\langle EF, Iter \\rangle$, where $Iter$ is the complete problem for the classical TFNP subclass PLS. We prove that $\\langle EF, Iter \\rangle$ is polynomially equivalent to the quantified boolean sequent calculus $G_1$, and also to the implicit Resolution proof system $[EF, Resolution]$ introduced by Krajícek [Kra04]. Hence $G_1$ and $[EF, Resolution]$ are polynomially equivalent, which is the first natural characterization of an implicit proof system by a classical propositional proof system beyond the work of Wang [Wan13]. We further observe our characterization can be extended to capture $G_i$ via the game induction principles of [ST07].\n\n    We also calibrate the strength of $\\langle EF, R \\rangle$ for general TFNP relations $R$. We observe that if Extended Frege can prove that a search problem $R$ is in FP, then $\\langle EF, R \\rangle$ 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.\n\n    Finally, and somewhat paradoxically, 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 $\\langle EF, R_P \\rangle$ is polynomially equivalent to $P$. Letting $P = [EF, Resolution]$ and combining our two results shows that $\\langle EF, Iter \\rangle$ is polynomially equivalent to $\\langle EF, R_{[EF, Resolution]} \\rangle$. Hence, despite the widely-believed conjecture that $Iter \\not \\in $ FP, the problems which $EF$-provably reduce to $Iter$ are exactly the problems which $EF$-provably reduce to a fixed polynomial-time computable set.",
  "title": "TR26-109 |  Provable Reductions in TFNP | \n\n\tNoah Fleming, \n\n\tRobert Robere, \n\n\tStefan Grosser, \n\n\tToniann Pitassi"
}