The Origins and Development of Sequent Calculi

Abstract

In 1934 Gentzen developed sequent calculus as a technical device for the study of natural deduction. Soon it turned out to be one of the most important tools of modern proof theory. In this survey paper we characterize the general idea of sequent calculi and some of their important features, in particular cut elimination and its consequences. We also briefly characterize some recent results, such as the generalized sequent calculi and the development of substructural logics.