Geodesic
$S_{k,\exp}$ does not prove $\mathrm{NP}=\mathrm{co}-\mathrm{NP}$ uniformly
Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VIII, Tome 304 (2003), pp. 99-120 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

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. 
@article{ZNSL_2003_304_a5,
     author = {Ch. Pollett},
     title = {$S_{k,\exp}$ does not prove $\mathrm{NP}=\mathrm{co}-\mathrm{NP}$ uniformly},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {99--120},
     year = {2003},
     volume = {304},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a5/}
}
TY  - JOUR
AU  - Ch. Pollett
TI  - $S_{k,\exp}$ does not prove $\mathrm{NP}=\mathrm{co}-\mathrm{NP}$ uniformly
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2003
SP  - 99
EP  - 120
VL  - 304
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a5/
LA  - en
ID  - ZNSL_2003_304_a5
ER  - 
%0 Journal Article
%A Ch. Pollett
%T $S_{k,\exp}$ does not prove $\mathrm{NP}=\mathrm{co}-\mathrm{NP}$ uniformly
%J Zapiski Nauchnykh Seminarov POMI
%D 2003
%P 99-120
%V 304
%U http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a5/
%G en
%F ZNSL_2003_304_a5
Ch. Pollett. $S_{k,\exp}$ does not prove $\mathrm{NP}=\mathrm{co}-\mathrm{NP}$ uniformly. Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VIII, Tome 304 (2003), pp. 99-120. http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a5/

[1] L. M. Adleman, K. Manders, “The computational complexity of decision procedures for polynomials”, Proceedings of the Sixteenth Annual Symposium on the Foundations of Computer Science, 1975, 169–177 | MR

[2] L. M. Adleman, K. Manders, “Diophantine Complexity”, Proceedings of the Seventeenth Annual Symposium on the Foundations of Computer Science, 1976, 81–88 | MR

[3] S. R. Buss, Bounded Arithmetic, Bibliopolis, Napoli, 1986 | MR | Zbl

[4] P. Clote, G. Takeuti, “First order bounded arithmetic and small boolean circuit complexity classes”, Feasible Mathematics, II, eds. P. Clote, J. Remmel, Birkhäuser, Boston, 1995, 154–218 | MR | Zbl

[5] H. Gaifman and C. Dimitracopoulos, “Fragments of Peano's arithmetic and the MRDP theorem”, Logic and algorithmic, Monograph. Enseign. Math., 30, Univ. Genève, Geneva, 1982, 187–206 | MR

[6] A. Grzegorczyck, “Some classes of recursive functions”, Rozpr. Mat., 4 (1953), 1–45 | MR

[7] J. Hastad, “Almost optimal lower bounds for small depth circuits”, Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing, 1987, 6–20 | MR

[8] P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetics, Springer-Verlag, 1993 | MR

[9] J. P. Jones, Yu. Matiyasevich, “Register machine proof of the theorem on exponential diophantine representation”, J. Symbolic Logic, 49 (1984), 818–829 | DOI | MR | Zbl

[10] C. F. Kent, B. R. Hodgson, “An arithmetical characterization of NP”, Theor. Computer Sci., 21 (1982), 255–267 | DOI | MR | Zbl

[11] J. Krajicek, Bounded Arithmetic, Propositional Logic and Complexity Theory, Cambridge University Press, 1995 | MR | Zbl

[12] Yu. V. Matiyasevich, “Diofantovost perechislimykh mnozhestv”, Doklady AN SSSR, 191 (1970), 279–282 | MR | Zbl

[13] Yu. V. Matiyasevich, Desyataya problema Gilberta, Fizmatlit, M., 1993 | MR

[14] P. G. Odifreddi, Classical recursion Theory, Vol. II, Elsevier, 1999 | MR

[15] R. Parikh, “Existence and feasibility in arithmetic”, J. Symbolic Logic, 36 (1971), 494–508 | DOI | MR | Zbl

[16] C. Pollett, “Structure and definability in general bounded arithmetic theories”, Annals Pure Appl. Logic, 100 (1999), 189–245 | DOI | MR | Zbl

[17] C. Pollett, “Multifunction algebras and the provability of $PH\downarrow$”, Annals Pure Appl. Logic, 104 (2000), 279–303 | DOI | MR | Zbl

[18] C. Pollett, “On the Bounded Version of Hilbert's Tenth Problem”, Arch. Math. Logic, 42:3 (2003), 469–488 | DOI | MR | Zbl

[19] A. A. Razborov, “Bounded arithmetic and lower bounds in Boolean complexity”, Feasible Mathematics, II, eds. P. Clote, J. Remmel, Birkhäuser, 1995, 344–386 | MR | Zbl

[20] A. A. Razborov, “Lower bounds for propositional proofs and independence results in bounded arithmetic”, Proceedings of $20$th International Symposium on the Mathematical Foundations of Computer Science, Springer-Verlag, 1995, 105 | MR

[21] G. Takeuti, “RSUV isomorphisms”, Arithmetic, Proof Theory, and Computational Complexity, Oxford Logic Guides, 23, eds. P. Clote, J. Krajíček, Clarendon Press, Oxford, 1993, 364–386 | MR | Zbl