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.
University of Siena, Italy - ORCID: 0000-0001-9441-7226
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
Licenza dei metadati
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
Licenza dei metadati
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