A semantical proof of the strong normalization theorem for full propositional classical natural deduction
From MaRDI portal
Publication:818927
DOI10.1007/s00153-005-0314-yzbMath1090.03027arXiv0905.0358MaRDI QIDQ818927
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
03F05: Cut-elimination and normal-form theorems
Related Items
Some properties of the -calculus, Unnamed Item, Strong normalization results by translation, A completeness result for the simply typed \(\lambda \mu \)-calculus, Non-strictly positive fixed points for classical natural deduction
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