A semantical proof of the strong normalization theorem for full propositional classical natural deduction

DOI10.1007/S00153-005-0314-YzbMath1090.03027arXiv0905.0358OpenAlexW2002953392MaRDI QIDQ818927

Karim Nour, Khelifa Saber

Publication date: 22 March 2006

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (5)

Unnamed Item ⋮ Some properties of the -calculus ⋮ Strong normalization results by translation ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ A completeness result for the simply typed \(\lambda \mu \)-calculus

Cites Work

• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Non-strictly positive fixed points for classical natural deduction
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• Proofs of strong normalisation for second order classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A semantical proof of the strong normalization theorem for full propositional classical natural deduction