Description:
<jats:p>We consider sets <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline1" /><jats:tex-math>${\it\Gamma}(n,s,k)$</jats:tex-math></jats:alternatives></jats:inline-formula> of narrow clauses expressing that no definition of a size <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline2" /><jats:tex-math>$s$</jats:tex-math></jats:alternatives></jats:inline-formula> circuit with <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline3" /><jats:tex-math>$n$</jats:tex-math></jats:alternatives></jats:inline-formula> inputs is refutable in resolution R in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline4" /><jats:tex-math>$k$</jats:tex-math></jats:alternatives></jats:inline-formula> steps. We show that every CNF with a short refutation in extended R, ER, can be easily reduced to an instance of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline5" /><jats:tex-math>${\it\Gamma}(0,s,k)$</jats:tex-math></jats:alternatives></jats:inline-formula> (with <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline6" /><jats:tex-math>$s,k$</jats:tex-math></jats:alternatives></jats:inline-formula> depending on the size of the ER-refutation) and, in particular, that <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline7" /><jats:tex-math>${\it\Gamma}(0,s,k)$</jats:tex-math></jats:alternatives></jats:inline-formula> when interpreted as a relativized NP search problem is complete among all such problems provably total in bounded arithmetic theory <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline8" /><jats:tex-math>$V_{1}^{1}$</jats:tex-math></jats:alternatives></jats:inline-formula>. We use the ideas of implicit proofs from Krajíček [<jats:italic>J. Symbolic Logic</jats:italic>, <jats:bold>69</jats:bold> (2) (2004), 387–397; <jats:italic>J. Symbolic Logic</jats:italic>, <jats:bold>70</jats:bold> (2) (2005), 619–630] to define from <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline9" /><jats:tex-math>${\it\Gamma}(0,s,k)$</jats:tex-math></jats:alternatives></jats:inline-formula> a nonrelativized NP search problem <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline10" /><jats:tex-math>$i{\it\Gamma}$</jats:tex-math></jats:alternatives></jats:inline-formula> and we show that it is complete among all such problems provably total in bounded arithmetic theory <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline11" /><jats:tex-math>$V_{2}^{1}$</jats:tex-math></jats:alternatives></jats:inline-formula>. The reductions are definable in theory <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" xlink:type="simple" xlink:href="S205050941600013X_inline12" /><jats:tex-math>$S_{2}^{1}$</jats:tex-math></jats:alternatives></jats:inline-formula>. We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them.</jats:p>