{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreie7ioyv5vw7yw4cw7kvexw3kp53ihnmde7wi4tw2uhh7seja7icru",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mpfvyfnp3xk2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2606.27931v1",
  "publishedAt": "2026-06-29T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Noah Fleming",
    "Stefan Grosser",
    "Toniann Pitassi",
    "Robert Robere"
  ],
  "textContent": "**Authors:** Noah Fleming, Stefan Grosser, Toniann Pitassi, Robert Robere\n\nWe introduce a new family of propositional proof systems, denoted , for an arbitrary TFNP search problem $R$. Informally, a refutation of a CNF formula $F$ in 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 Σ^b_1$ formulas $φ$ in a theory $T$ imply algorithms solving the search problem for $φ$ 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 , where Iter is a complete problem for PLS. We prove that 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 for general TFNP relations $R$. We observe that if EF can prove that a search problem $R$ is in FP, then 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 is polynomially equivalent to $P$. Letting $P =$ [EF, Resolution] and combining our two results shows that is polynomially equivalent to .",
  "title": "Provable Reductions in TFNP"
}