A short proof of the strong normalization of classical natural deduction with disjunction

DOI10.2178/jsl/1067620187zbMath1066.03056arXiv0905.0760OpenAlexW2077107862MaRDI QIDQ4650284

René David, Karim Nour

Publication date: 9 February 2005

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

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

zbMATH Keywords

classical propositional logicstrong normalization\(\lambda\mu\)-calculus

Mathematics Subject Classification ID

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

Related Items (12)

A semantical proof of the strong normalization theorem for full propositional classical natural deduction ⋮ Strong normalization proofs by CPS-translations ⋮ Unnamed Item ⋮ Some properties of the -calculus ⋮ Strong normalization results by translation ⋮ A short proof of the strong normalization of classical natural deduction with disjunction ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ Contraction-free Proofs and Finitary Games for Linear Logic ⋮ Unnamed Item ⋮ Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion ⋮ A simple proof of second-order strong normalization with permutative conversions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Classical logic, storage operators and second-order lambda-calculus
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• On the intuitionistic force of classical search
• Normalization without reducibility
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• On the proof theory of the intermediate logic MH
• Normalization theorems for full first order classical natural deduction
• A new constructive logic: classic logic
• A short proof of the strong normalization of classical natural deduction with disjunction
• On the semantics of classical disjunction

This page was built for publication: A short proof of the strong normalization of classical natural deduction with disjunction