### arnold beckmann's pages

## The NP Search Problems of Frege and Extended Frege Proofs

**File:** PDF-File

**Author:** Arnold Beckmann and Sam Buss

**Title:** The NP Search Problems of Frege and Extended Frege Proofs

**Journal:** ACM TOCL 2017, **18**(2): 11:1-11:19

**Year:** 2017

**Pages:** 19

**DOI:** 10.1145/3060145

**Abstract:**
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.