Gentzenizing Schroeder-Heister's natural extension of natural deduction

DOI10.1305/NDJFL/1093635337zbMATH Open0712.03046OpenAlexW2029272128MaRDI QIDQ923083FDOQ923083

Authors: Arnon Avron 

Publication date: 1990

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1093635337

Recommendations

• Extended Natural Deduction Images of Conversions from the System of Sequents
• A sequent calculus isomorphic to Gentzen's natural deduction
• scientific article; zbMATH DE number 3275554
• scientific article; zbMATH DE number 1406467
• A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic

zbMATH Keywords

normalizationcut-eliminationGentzen-type sequential calculushigher-order rulesintuitionistic implicationnatural deduction system of Schroeder- Heister

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Cut-elimination and normal-form theorems (03F05)

Cited In (7)

• Functional completeness for subsystems of intuitionistic propositional logic
• Eight rules for implication elimination
• Proof-theoretic semantics: an autobiographical survey
• Simple consequence relations
• A note on the proof theory of the \(\lambda \Pi\)-calculus
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus
• Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus

This page was built for publication: Gentzenizing Schroeder-Heister's natural extension of natural deduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q923083)