Gentzenizing Schroeder-Heister's natural extension of natural deduction
The author provides an example of how the use of the Gentzen-type sequential calculus simplifies a complex natural deduction formalism by giving the Gentzen-type version to the natural deduction system of Schroeder-Heister. The notions of the natural deduction system that are difficult to handle become redundant, so that the complex normalization proof can be replaced by a standard cut-elimination proof. The resulting Gentzen system is essentially the same as the intuitionistic one, which therefore sheds new light on the connection between Schroeder-Heister's higher-order rules and intuitionistic implication.
- 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
- Functional completeness for subsystems of intuitionistic propositional logic
- A note on the proof theory of the -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
- Proof-theoretic semantics: an autobiographical survey
- Eight rules for implication elimination
- Simple consequence relations
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)
