Chapter Sequent calculus and complexity theory

Overview & Synopsis

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.