Gentzenizing Schroeder-Heister's natural extension of natural deduction

DOI10.1305/NDJFL/1093635337MaRDI QIDQ923083zbMATHOpenAlexFDO

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

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)

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

Cited in

(7)

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