Gentzen's Proof Systems: Byproducts in a Work of Genius

DOI10.2178/bsl/1344861886zbMath1258.03002OpenAlexW2019486724MaRDI QIDQ2915886

Jan von Plato

Publication date: 19 September 2012

Published in: The Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.bsl/1344861886

zbMATH Keywords

natural deductionsequent systemGentzen

Mathematics Subject Classification ID

History of mathematics in the 20th century (01A60) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) History of mathematical logic and foundations (03-03) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION ⋮ EARLY STRUCTURAL REASONING. GENTZEN 1932 ⋮ The explosion calculus ⋮ Inference in Nineteenth-Century British Logic ⋮ The placeholder view of assumptions and the Curry-Howard correspondence ⋮ The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract) ⋮ From axiomatic logic to natural deduction ⋮ GENERALITY AND EXISTENCE: QUANTIFICATIONAL LOGIC IN HISTORICAL PERSPECTIVE ⋮ The Role of Structural Reasoning in the Genesis of Graph Theory ⋮ Prawitz, Proofs, and Meaning ⋮ Meaning in Use ⋮ Relevant Connexive Logic ⋮ Nineteenth Century British Logic on Hypotheticals, Conditionals, and Implication ⋮ Eight inference rules for implication

Cites Work

• Natural deduction with general elimination rules
• Die Grundlegung der elementaren Zahlenlehre
• A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION
• Consistency of Heyting arithmetic in natural deduction
• Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• A natural extension of natural deduction
• Normalization theorems for full first order classical natural deduction
• Completeness Before Post: Bernays, Hilbert, and the Development of Propositional Logic
• In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs
• The consistency of arithmetics
• A proof of Gentzen's \textit{Hauptsatz} without multicut
• Unnamed Item
• Unnamed Item