Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi

In this paper we give an arithmetical proof of the strong normalization oflambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as aformulae-as-types translation of classical propositional logic in naturaldeduction style. Then we give a translation between thelambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which isthe implicational part of the lambda-bar-mu-mu-tilde-calculus invented byCurien and Herbelin [3] extended with negation. In this paper we adapt themethod of David and Nour [4] for proving strong normalization. The novelty inour proof is the notion of zoom-in sequences of redexes, which leads usdirectly to the proof of the main theorem