$S_{k,\exp}$ does not prove $\mathrm{NP}=\mathrm{co}-\mathrm{NP}$ uniformly

Ch. Pollett

Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VIII, Tome 304 (2003), pp. 99-120

Résumé

A notion of a uniform sequent calculus proof is given. It is then shown that a strengthening, $S_{k,\exp}$, of the well-studied bounded arithmetic system $S_k$ of Buss does not prove $\mathrm{NP}=\mathrm{co}-\mathrm{NP}$ with a uniform proof. A slightly stronger result that $S_{k,\exp}$ cannot prove $\widehat\Sigma_{1,k'}^b=\widehat\Pi_{1,k'}^b$ uniformly for $2\leq k'\leq k$ is also established. A variation on the technique used is then applied to show that $S_{k,\exp}$ is unable to prove Davis–Putnam–Robinson–Matiyasevich theorem. This result is also without any uniformity conditions. Generalization of both these results to higher levels of the Grzegorczyck Hierarchy are then presented.