Contenuto in:
Capitolo

Sequent calculus and complexity theory

  • Duccio Pianigiani

We come to a formalism introduced by Gentzen, namely the sequents calculus. We introduce here the basic concepts and prove the most important result about it, namely cut-elimination. Actually we will not illustrate here the cut elimination for pure logic, but rather a proof of the free-cut elimination theorem, according to which some cuts can be Eliminated, in fact the only results available for theories (i.e. logic plus proper axioms and induction rule), since we will see that for them the full cut-elimination is not valid. We show how this result has been applied for the characterization of functions computable in polynomial time.

  • Keywords:
  • Sequent calculus,
  • cut-elimination,
  • free-cut elimination,
  • provably total functions,
+ Mostra di più

Duccio Pianigiani

University of Siena, Italy - ORCID: 0000-0001-9441-7226

  1. Ajtai, Miklós. 1994. “The complexity of the pigeonhole principle”. Combinatorica 14: 417-433. DOI: 10.1007/BF01302964
  2. Beame, Paul and Impagliazzo, Russell and and Pitassi, Toniann. 1993. “Exponential lower bounds for the pigeonhole principle” . Computational Complexity 3: 97-140. DOI: 10.1007/BF01200117
  3. Beckmann, Arnold and Buss, Samuel R.2011. “Corrected upper bounds for free-cut elimina- tion”. Theoretical Computer Science 412 (39): 5433-5445 DOI: 10.1016/j.tcs.2011.05.053
  4. Beckmann, Arnold and Pollett, Chris and Buss, Samuel R. 2003. “Ordinal notations and well- orderings in bounded arithmetic”. Annals of Pure and Applied Logic 120, (1–3): 197-223, DOI: 10.1016/s0168-0072(02)00066-0
  5. Buss, Samuel R. 1986. Bounded Arithmetic. Napoli: Bibliopolis.
  6. Buss, Samuel. 1985. “The polynomial hierarchy and intuitionistic Bounded Arithmetic” . Structure in Complexity Theory: 77-103. DOI: 10.1145/22145.22177
  7. Buss, Samuel R. 1998. “An introduction to proof theory”. In Handbook of proof theory, 1-78. Amsterdam: Elsevier. DOI: 10.2307/420968
  8. Buss, Samuel R. 1999. “Bounded arithmetic, proof complexity and two papers of Parikh” . Annals of Pure and Applied Logic 96 (1-3): 43-55. DOI: 10.1016/S0168-0072(98)00030-X
  9. Buss, Samuel R. and Krajícek, Jan. 1994. “An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic” . Proceedings of The London Mathematical Society: 1-21. DOI: 10.1112/plms/s3-69.1.1
  10. Buss, Samuel R. and Krajíček, Jan and Takeuti, Gaisi. 1993. “Provably total functions in the bounded arithmetic theories R 3 i , U 2 i , and V 2 i ” . In Proof Theory, Arithmetic, and Complexity, edited by P. Clote and J. Krajíček, 116-161. Oxford: Oxford University Press. DOI: 10.1093/oso/9780198536901.003.0006
  11. Cantini, Andrea. 1996. “Asymmetric Interpretations for Bounded Theories” . Mathematical Logic Quarterly 42: 270-288. DOI: 10.1002/malq.19960420123
  12. Cook, Stephen and Nguyen, Phuong. 2010. Logical Foundations of Proof Complexity . Cam- bridge: Cambridge University Press. DOI: 10.2178/bsl/1309952322
  13. Cook, Stephen and Urquhart, Alisdair. 1993. “Functional interpretations of feasibly constructive arithmetic” . Annals of Pure and Applied Logic 63 (2): 103-200. DOI: 10.1016/0168-0072(93)90044-E
  14. Ferreira, Fernando and Ferreira, Gilda. 2013. “Interpretability in Robinson’s Q”. The Bulletin of Symbolic Logic 19: 289-317. DOI: 10.1017/S1079898600010660
  15. Girard, Jean Yves. 1987. Proof-theory and logical complexity I. Napoli: Bibliopolis.
  16. Girard, Jean-Yves and Lafont, Yves and Taylor, Paul. 1989. Proofs and types. Cambridge: Cambridge University Press. DOI: 10.2307/2274726
  17. Gentzen, Gerhard. 1935. “Untersuchungen über das logische Schließen” . Mathematische Zeitschrift 39: 176-210 and 405-431. DOI: 10.1007/BF01201353
  18. Harnik, Victor. 1992. “Provably Total Functions of Intuitionistic Bounded Arithmetic”. The Journal of Symbolic Logic 57 (2): 466-477. DOI: 10.2307/2275282
  19. Hájek, Peter and Pudlák, Pavel. 1993. Metamathematics of first order arithmetic. Berlin: Springer. DOI: 10.1017/9781316717271
  20. Herbrand, Jacques. 1930. “Recherches sur la théorie de la démonstration”. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques 33: 1-131. DOI: 10.3917/puf.herbr.1968.01.0035
  21. Ketonen, Jussi and Solovay, Robert. 1981. “Rapidly Growing Ramsey Functions”. Annals of Mathematics 113 (2): 267-314. DOI: 10.1007/978-3-319-01315-2_8
  22. Krajíček, Jan. 1995. Bounded arithmetic, propositional logic, and complexity theory. Cam- bridge: Cambridge University Press. DOI: 10.1017/CBO9780511529948
  23. Parikh, Rohit. 1971. “Existence and Feasibility.” The Journal of Symbolic Logic 36 (3): 494-508. DOI: 10.2307/2269958
  24. Paris, Jeff and Dimitracopoulos, Costas. 1983, “A Note on the Undefinability of Cuts”. The Journal of Symbolic Logic 48: 564-569. DOI: 10.2307/2273447
  25. Razborov, Alexander A. 1993. “An equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic.” In P. Clote and J. Krajicek (editors) Arith- metic, Proof Theory and Computational Complexity 247-277. Oxford: Oxford University Press. DOI: 10.1093/oso/9780198536901.003.0012
  26. Tait, William W. 1968. “Normal derivability in classical logic”. In The Syntax and Semantics of Infinitatry Languages. Lecture Notes in Mathematics 72, edited by J. Barwise, 204-236. Berlin: Springer. DOI: 10.1007/BFb0079691
  27. Takeuti, Gaisi. 1987. Proof Theory. Amsterdam: North Holland (Reprint Courier Corporation, 2013).
  28. Takeuti, Gaisi. 1993. “RSUV isomorphism.” In Arithmetic, Proof Theory and Computational Complexity, edited by P. Clote and J. Krajicek, 364-386. Oxford: Oxford University.
  29. Troelstra, Anne S. and Schwichtenberg, Helmut. 2000. Basic proof theory. Cambridge: Cam- bridge University Press. DOI: 10.1017/cbo9781139168717
  30. Verbrugge, Rineke. 1993. Efficient Metamathematics. Dissertation, Universiteit Van Amsterdam
  31. Urban, Christian and Bierman, Gavin M. 2001. “Strong Normalisation of Cut-Elimination in Classical Logic.”Fundamenta Informaticae 45 (1-2): 123-155. DOI: 10.1007/3-540-45413-6_32
  32. Wilkie, Alex J. and Paris, Jeff B. “On the scheme of induction for bounded arithmetic formulas”. Annals of Pure and Applied Logic 35 : 261-302. DOI: 10.1016/0168-0072(87)90066-2
  33. Zambella, Domenico. 1996. “Notes on Polynomially Bounded Arithmetic”. The Journal of Symbolic Logic 61 (3): 942-966. DOI: 10.2307/2275794
PDF
  • Anno di pubblicazione: 2025
  • Pagine: 173-204

XML
  • Anno di pubblicazione: 2025

Informazioni sul capitolo

Titolo del capitolo

Sequent calculus and complexity theory

Autori

Duccio Pianigiani

Lingua

Inglese

DOI

10.36253/979-12-215-0778-2.12

Opera sottoposta a peer review

Anno di pubblicazione

2025

Copyright

© 2025 Author(s)

Licenza d'uso

CC BY-SA 4.0

Licenza dei metadati

CC0 1.0

Informazioni bibliografiche

Titolo del libro

Lectures in Proof Theory and Complexity

Autori

Duccio Pianigiani

Opera sottoposta a peer review

Anno di pubblicazione

2025

Copyright

© 2025 Author(s)

Licenza d'uso

CC BY-SA 4.0

Licenza dei metadati

CC0 1.0

Editore

Firenze University Press, USiena Press

DOI

10.36253/979-12-215-0778-2

eISBN (pdf)

979-12-215-0778-2

eISBN (xml)

979-12-215-0779-9

Collana

UNIverSI. Ricerca e Didattica all’Università di Siena

ISSN della collana

3035-5915

e-ISSN della collana

3035-5931

137

Download dei libri

147

Visualizzazioni

Salva la citazione

1.481

Libri in accesso aperto

in catalogo

3.227

Capitoli di Libri

5.569.557

Download dei libri

5.515

Autori

da 1181 Istituzioni e centri di ricerca

di 66 Nazioni

77

scientific boards

da 413 Istituzioni e centri di ricerca

di 46 Nazioni

1.316

I referee

da 405 Istituzioni e centri di ricerca

di 39 Nazioni