The NP Search Problems of Frege and Extended Frege Proofs

摘要

We study consistency search problems for Frege and extended Frege proofs-namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle, describing a proof of a contradiction; the output is the location of a syntactic error in the proof. The consistency search problems for Frege and extended Frege systems are shown to be many-one complete for the provably total NP search problems of the second-order bounded arithmetic theories U-2(1) and V-2(1), respectively.