- 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".

Ralph Matthes Last modified: Mon Aug 30 17:07:37 CEST 2004