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 calculus; normalization; natural deduction; cut-elimination; Curry-Howard isomorphism; proof terms

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03F07: Structure of proofs

03F03: Proof theory in general (including proof-theoretic semantics)

Related Items

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

Uses Software

• Pesca

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item