Changes from LC03 submission to final version

• Acknowledgements: I am thankful for fruitful discussions with Andreas Abel and Klaus Aehlig. I also thank the anonymous referee for inducing a further thought process.
• Added to remark1 on page 9: Non-canonical stability witnesses that occur as second step terms of It# would not enjoy a similar operational rule, hence a coherence problem arises in form of non-confluence.
• At the very end of Section 4.1 (page 11), a paragraph added in form of a remark:

  There is a less radical approach for the circumvention of
  administrative reductions than the introduction of another set of
  variables, due to Andou [1,2]. The need above,
  namely that $\mu$-bound variables $x$ only occur free in subterms of
  the form $xt$, is turned into the definition of a \emph{regular} term,
  and only regular terms are studied. (Clearly, if one knows that $x$ is
  bound by some $\mu x^{\neg A}$, one might replace free occurrences of
  $x$ by $\lambda y^A. xy$ and arrive at a regular term.)  Then, one may
  define reduction as in $\lambda\mu$-calculus, and regularity is not
  lost during reduction. However, we would still only obtain a common
  reduct for the translated terms on both sides of the new
  $\mu$-reduction rule. For a proper simulation of $\mu$-reduction, it
  will be essential to translate the type $\neg A$ of such a variable
  $x$ into $\neg A'$ and not into $(\neg A)'$. Therefore,
  compositionality considerations require to open up a new namespace of
  ``$\mu$-variables'' for the variables that receive this special
  treatment of their types during translation.
  
  [1] Yuuki Andou. A normalization-procedure for the
    first order classical natural deduction with full logical symbols,
    Tsukuba Journal of Mathematics, vol. 19(1995), no.1, pp.153--162.
  [2] Yuuki Andou. Church-Rosser property of a simple reduction for
    full first-order classical natural deduction, Annals of
    Pure and Applied Logic, vol.119(2003), pp.225--237.
  

• The last phrase has slightly changed to: Published proofs of strong normalization of classical second-order logic by double-negation translations seem to have failed altogether, but there is the recent work by Nakazawa and Tatsuta which does perhaps not fully qualify as an "embedding".