On Gentzen’s Structural Completeness Proof

Abstract

In his very first publication, Gentzen introduced the structural rules of thinning and cut on sequents. He did not consider rules for logical operators. Gentzen provided a most interesting ‘structural completeness proof’, which it is the concern of this study to explain and clarify. We provide an improved (because more detailed) proof of Gentzen’s completeness result. Then we reflect on the self-imposed limitations of this, Gentzen’s earliest sequent-setting, and explore how his approach might have been generalized, even in the absence of logical operators, so as to cover cases involving sequents with empty antecedent or succedent, and logical consequences of infinite sets of sequents.