Strong normalization of classical natural deduction with disjunctions

DOI10.1016/J.APAL.2008.01.003zbMATH Open1141.03027OpenAlexW2043498337MaRDI QIDQ2482841FDOQ2482841

Authors: Koji Nakazawa, Makoto Tatsuta 

Publication date: 24 April 2008

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2008.01.003

Recommendations

• A note on strong normalization in classical natural deduction
• Strong normalization results by translation
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• A simple proof of second-order strong normalization with permutative conversions

zbMATH Keywords

strong normalizationpermutative conversion\(\lambda\mu\)-calculusCPS-translationgeneral elimination

Mathematics Subject Classification ID

Classical propositional logic (03B05) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Natural deduction with general elimination rules
• On the strong normalisation of intuitionistic natural deduction with permutation-conversions
• The duality of computation
• Domain-free \(\lambda\mu\)-calculus
• Proofs of strong normalisation for second order classical natural deduction
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• Parallel reductions in \(\lambda\)-calculus
• Non-strictly positive fixed points for classical natural deduction
• A simple proof of second-order strong normalization with permutative conversions
• A short proof of the strong normalization of classical natural deduction with disjunction
• Call-by-value is dual to call-by-name
• Stabilization -- an alternative to double-negation translation for classical natural deduction
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• A semantics of realisability for the classical propositional natural deduction
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• Strong normalization proof with CPS-translation for second order classical natural deduction
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (16)

• Proofs of strong normalisation for second order classical natural deduction
• Title not available (Why is that?)
• Proof Terms for Generalized Natural Deduction
• A simple proof of second-order strong normalization with permutative conversions
• Strong normalization proofs by CPS-translations
• Peirce's rule in a full natural deduction system
• Peirce's rule in natural deduction.
• Strong normalization for truth table natural deduction
• A note on strong normalization in classical natural deduction
• Classical Logic with Mendler Induction
• A short proof of the strong normalization of classical natural deduction with disjunction
• Strong normalization results by translation
• Title not available (Why is that?)
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• A strong normalization result for classical logic
• Strong normalization proof with CPS-translation for second order classical natural deduction

This page was built for publication: Strong normalization of classical natural deduction with disjunctions

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