Sequent calculus and complexity theory Duccio Pianigiani University of Siena, Italy This is a section of Lectures in Proof Theory and Complexity(DOI: 10.36253/979-12-215-0778-2) by Duccio Pianigiani Firenze University Press, USiena Press Florence 2025 https://doi.org/10.36253/979-12-215-0778-2.12

Available for academic research purposes

Open Access

Copyright Author(s)

Content licence CC BY-SA 4.0

Metadata licence CC0 1.0

This is original content, published for academic research purposes

 Digital edition XML powered by Booksflow

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.

 Sequent calculus cut-elimination free-cut elimination provably total functions

It is available online at https://doi.org/10.36253/979-12-215-0778-2.12

References Ajtai, Miklós. 1994. “The complexity of the pigeonhole principle”. Combinatorica 14: 417-433. 10.1007/BF01302964 Beame, Paul and Impagliazzo, Russell and and Pitassi, Toniann. 1993. “Exponential lower bounds for the pigeonhole principle” . Computational Complexity 3: 97-140. 10.1007/BF01200117 Beckmann, Arnold and Buss, Samuel R.2011. “Corrected upper bounds for free-cut elimina- tion”. Theoretical Computer Science 412 (39): 5433-5445 10.1016/j.tcs.2011.05.053 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, 10.1016/s0168-0072(02)00066-0 Buss, Samuel R. 1986. Bounded Arithmetic. Napoli: Bibliopolis. Buss, Samuel. 1985. “The polynomial hierarchy and intuitionistic Bounded Arithmetic” . Structure in Complexity Theory: 77-103. 10.1145/22145.22177 Buss, Samuel R. 1998. “An introduction to proof theory”. In Handbook of proof theory, 1-78. Amsterdam: Elsevier. 10.2307/420968 Buss, Samuel R. 1999. “Bounded arithmetic, proof complexity and two papers of Parikh” . Annals of Pure and Applied Logic 96 (1-3): 43-55. 10.1016/S0168-0072(98)00030-X 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. 10.1112/plms/s3-69.1.1 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. 10.1093/oso/9780198536901.003.0006 Cantini, Andrea. 1996. “Asymmetric Interpretations for Bounded Theories” . Mathematical Logic Quarterly 42: 270-288. 10.1002/malq.19960420123 Cook, Stephen and Nguyen, Phuong. 2010. Logical Foundations of Proof Complexity . Cam- bridge: Cambridge University Press. 10.2178/bsl/1309952322 Cook, Stephen and Urquhart, Alisdair. 1993. “Functional interpretations of feasibly constructive arithmetic” . Annals of Pure and Applied Logic 63 (2): 103-200. 10.1016/0168-0072(93)90044-E Ferreira, Fernando and Ferreira, Gilda. 2013. “Interpretability in Robinson’s Q”. The Bulletin of Symbolic Logic 19: 289-317. 10.1017/S1079898600010660 Girard, Jean Yves. 1987. Proof-theory and logical complexity I. Napoli: Bibliopolis. Girard, Jean-Yves and Lafont, Yves and Taylor, Paul. 1989. Proofs and types. Cambridge: Cambridge University Press. 10.2307/2274726 Gentzen, Gerhard. 1935. “Untersuchungen über das logische Schließen” . Mathematische Zeitschrift 39: 176-210 and 405-431. 10.1007/BF01201353 Harnik, Victor. 1992. “Provably Total Functions of Intuitionistic Bounded Arithmetic”. The Journal of Symbolic Logic 57 (2): 466-477. 10.2307/2275282 Hájek, Peter and Pudlák, Pavel. 1993. Metamathematics of first order arithmetic. Berlin: Springer. 10.1007/978-3-662-22156-3 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. 10.3917/puf.herbr.1968.01.0035 Ketonen, Jussi and Solovay, Robert. 1981. “Rapidly Growing Ramsey Functions”. Annals of Mathematics 113 (2): 267-314. 10.1007/978-3-319-01315-2_8 Krajíček, Jan. 1995. Bounded arithmetic, propositional logic, and complexity theory. Cam- bridge: Cambridge University Press. 10.1017/CBO9780511529948 Parikh, Rohit. 1971. “Existence and Feasibility.” The Journal of Symbolic Logic 36 (3): 494-508. 10.2307/2269958 -- Paris, Jeff and Dimitracopoulos, Costas. 1983, “A Note on the Undefinability of Cuts”. The Journal of Symbolic Logic 48: 564-569. 10.2307/2273447 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. 10.1093/oso/9780198536901.003.0012 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. 10.1007/BFb0079691 Takeuti, Gaisi. 1987. Proof Theory. Amsterdam: North Holland (Reprint Courier Corporation, 2013). Takeuti, Gaisi. 1993. “RSUV isomorphism.” In Arithmetic, Proof Theory and Computational Complexity, edited by P. Clote and J. Krajicek, 364-386. Oxford: Oxford University. Troelstra, Anne S. and Schwichtenberg, Helmut. 2000. Basic proof theory. Cambridge: Cam- bridge University Press. 10.1017/cbo9781139168717 Verbrugge, Rineke. 1993. Efficient Metamathematics. Dissertation, Universiteit Van Amsterdam Urban, Christian and Bierman, Gavin M. 2001. “Strong Normalisation of Cut-Elimination in Classical Logic.”Fundamenta Informaticae 45 (1-2): 123-155. 10.1007/3-540-45413-6_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. 10.1016/0168-0072(87)90066-2 Zambella, Domenico. 1996. “Notes on Polynomially Bounded Arithmetic”. The Journal of Symbolic Logic 61 (3): 942-966. 10.2307/2275794