zbMATH — the first resource for mathematics

On Gentzen’s structural completeness proof. (English) Zbl 1429.03204
Wansing, Heinrich (ed.), Dag Prawitz on proofs and meaning. Cham: Springer. Outst. Contrib. Log. 7, 385-414 (2015).
Summary: 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.
For the entire collection see [Zbl 1304.03008].
03F07 Structure of proofs
03-03 History of mathematical logic and foundations
01A60 History of mathematics in the 20th century
Full Text: DOI
[1] Franks, C. (2010). Cut as consequence. History and Philosophy of Logic, 31(4), 349-379. · Zbl 1298.03005
[2] Gentzen, G. (1932). Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen. Mathematische Annalen, 107(1), 329-350. · Zbl 0005.33803
[3] Hertz, P. (1928). Reichen die üblichen syllogistischen Regeln für das Schließen in der positiven Logik elementarer Sätze aus? Annalen der Philosophie und Philosophischen Kritik, 7(1), 272-277. · JFM 54.0065.13
[4] Schroeder-Heister, P.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.