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:
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 subclass corresponding to $T$ [Bus86, KP90, BK94, KST07, BB09].
2. 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].
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].
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.
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.
