Proofs of strong normalisation for second order classical natural deduction

Abstract

We give two proofs of strong normalisation for second order classical natural deduction . The first one is an adaptation of the method of reducibility candidates introduced in [9] for second order intuitionistic natural deduction; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a Kolmogorov translation.