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