A short proof of the strong normalization of classical natural deduction with disjunction
René David, Karim Nour · Journal of Symbolic Logic · 2003
Abstract 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.