arXiv Analytics

Sign in

arXiv:0905.0760 [math.LO]AbstractReferencesReviewsResources

A short proof of the Strong Normalization of Classical Natural Deduction with Disjunction

René David, Karim Nour

Published 2009-05-06Version 1

We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e. in presence of all the usual connectives) classical natural deduction.

Journal: The Journal of Symbolic Logic 68, 4 (2003) 1277-1288
Categories: math.LO
Related articles: Most relevant | Search more
arXiv:0905.1557 [math.LO] (Published 2009-05-11)
A short proof of the strong normalization of the simply typed $λμ$-calculus
arXiv:1805.09890 [math.LO] (Published 2018-05-24)
Truth, Disjunction, and Induction
arXiv:0905.1032 [math.LO] (Published 2009-05-07)
An arithmetical proof of the strong normalization for the $λ$-calculus with recursive equations on types

Links

Toolbox