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 Σ^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 <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]}$>.

翻译：暂无翻译