CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI

DOI10.1017/S1755020320000015zbMath1485.03233arXiv2001.00662MaRDI QIDQ5024505

Richard Zach

Publication date: 26 January 2022

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

Full work available at URL: https://arxiv.org/abs/2001.00662

zbMATH Keywords

sequent calculusnormalizationnatural deductioncut-eliminationCurry-Howard isomorphismproof terms

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (1)

A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems

Uses Software

• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective)
• On sequence-conclusion natural deduction systems
• Existential instantiation and normalization in sequent natural deduction
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Untersuchungen über das logische Schliessen. II
• Definitional reflection and basic logic
• A natural extension of natural deduction
• Normalization theorems for full first order classical natural deduction
• Basic logic: reflection, symmetry, visibility
• Inversion Principles and Introduction Rules
• Deriving Natural Deduction Rules from Truth Tables
• Cut-elimination and redundancy-elimination by resolution

This page was built for publication: CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI