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.
No takes yet. Share an insight, caveat, or question.
Beckmann et al. (2017) studied this question.
Synapse has enriched 3 closely related papers on similar clinical questions. Consider them for comparative context: