The NP Search Problems of Frege and Extended Frege Proofs
Arnold Beckmann, Sam Buss · ACM Transactions on Computational Logic · 2017
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 1 2 and V 1 2 , respectively.