Towards a unified complexity theory of total functions (Q1745728)

TFNP (Total Function Nondeterministic Polynomial) is the complexity class of functions \(f\) of the following form. There is a PTIME query \(R\) and a polynomial \(p\) such that for any input \(I\), there is at least one witness \(f(I)\) such that \(|f(I)| \leq p(|I|)\) and \(R(I, f(I))\). TFNP and some subclasses are described in [\textit{N. Megiddo} and the second author, Theor. Comput. Sci. 81, No. 2, 317--324 (1991; Zbl 0731.68036)]. This article presents a ``WrongProof'' problem that is hard for some of these subclasses, and defines a class PTFNP as the class of problems reducible to WrongProof. In WrongProof, one is given a readily confirmed contradiction together with a proof, and the output is the location of an error in the proof. Exponentially large proofs are represented by polynomial-sized Boolean circuits enumerating the lines of the proof as in [\textit{J. Krajíček}, J. Symb. Log. 69, No. 2, 387--397 (2004; Zbl 1069.03053)]. Some problems known to be complete for some subclasses of TFNP are reduced to WrongProof.