The class TFNP, of NP search problems where all instances have solutions, appears not to have complete problems. However, TFNP contains various syntactic subclasses and important problems. We introduce a syntactic class of problems that contains these known subclasses, for the purpose of understanding and classifying TFNP problems. This class is defined in terms of the search for an error in a concisely-represented formal proof. Finally, the known complexity subclasses are based on existence theorems that hold for finite structures; from Herbrand's Theorem, we note that such theorems must apply specifically to finite structures, and not infinite ones.

Mainly, we add more detail on the related literature on Bounded Arithmetic, which obtains similar results to this paper.

The complexity class TFNP is the set of {\em total function} problems that belong to NP: every input has at least one output and outputs are easy to check for validity, but it may be hard to find an output. TFNP is not believed to have complete problems, but it encompasses several subclasses (PPAD, PPADS, PPA, PLS, PPP) that do, plus several other problems, such as {\sc Factoring}, which appear harder to classify. In this paper we introduce a new class, which we call PTFNP (for ``provable'' TFNP) which contains the five subclasses, has complete problems, and generally feels like a well-behaved close approximation of TFNP. PTFNP is based on a kind of consistency search problem that we call WRONG PROOF: Suppose that we have a consistent deductive system, and a concisely-represented proof having exponentially many steps, that leads to a contradiction. There must be an error somewhere in the proof, and the challenge is to find it. We show that this problem generalises various well-known TFNP problems, including the five classes mentioned above, making it a candidate for an overarching complexity characterisation of NP total functions. Finally, we note that all five complexity subclasses of TFNP mentioned above capture existence theorems (such as ``every dag has a sink'') that are true for finite structures but false for infinite ones. We point out that an application of Jacques Herbrand's 1930 theorem shows that this is no coincidence.