GENTZEN’S OVERVIEW OF CALCULI AND REDUCTIONS IN CONSISTENCY PROOFS

Abstract Gentzen’s sequent calculi were a part of his consistency program, the ultimate aim of which was a proof of the consistency of analysis. Among Gentzen’s series of shorthand notes there was one titled WKR in which various sequent calculi and cut elimination procedures are examined. Nothing of this series has survived, but there is instead a late summary Gentzen wrote of it in 1944. In this article, these calculi and reductions are described in the context of Gentzen’s consistency program, followed by an English translation of his manuscript that is written in what is known as the unified German shorthand (einheitliche Kurzschrift).