We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.

The $\lambda\mu$-calculus is an extension of the $\lambda$-calculus that has been introduced by M Parigot to give an algorithmic content to classical proofs. We show that Bohm's theorem fails in this calculus.

Summary. A constructive realizablity interpretation for classical arithmetic is presented, enabling one to extract witnessing terms from proofs of 1 sentences. The interpretation is shown to coincide with modified realizability, under a novel translation of classical logic to intuitionistic logic, followed by the Friedman-Dragalin translation. On the other hand, a natural set of reductions for classical arithmetic is shown to be compatible with the normalization of the realizing term, implying that certain strategies for eliminating cuts and extracting a witness from (...) the proof of a 1 sentence are insensitive to the order in which reductions are applied. (shrink)

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.

We prove the strong normalization of full classical natural deduction by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.