Translations and Normalization Procedures

Maria da Paz N. Medeiros & Luiz Carlos Pereira

The aim of the present paper is to explore some interesting connections between translations among logics and different normalization procedures. It can be easily verified that the family of negative translations (Kolmogorov, Gentzen, Gödel) can be proof-theoretically justified by the normalization procedure for classical logic used by Prawitz (see Prawitz [1]). Prawitz shows, as a preliminary result to normalization, that every application of the classical absurd rule in the fragment {∧, →, ⊥, ∀} of the natural deduction system can be reduced to an atomic application. The moral is: in the given fragment, classical reasoning can be restricted to atomic formulas. In 1989, J. Seldin presented a new normalization strategy where he showed that every derivation in the fragment {∧, ∨, →, ⊥, ∃} could be transformed into a derivation with at most one application of the classical absurd rule. Moreover, if this application occurred, it would be the last rule in the resulting derivation. The moral now is: in this new fragment, classical reasoning, if used at all, is used as the last step of an argument. This normalization procedure gives rise (1) to a new translation from classical logic into intuitionistic logic, and (2) to an extension of Glivenko’s theorem to first order logic. In the final part of the paper, we extend this analysis to the translation proposed by P. Krauss and to translations from intuitionistic logic into classical linear logic.

[1] Prawitz, D. Natural Deduction, Almqvist and Wiksell, Stockholm, 1965.

[2] Seldin, J. Normalization and Excluded Middle I, Studia Logica 48, pp. 193-217, 1989.

[3] Seldin, J. On the proof-theory of the intermediate logic MH, JSL 51, pp. 626-647, 1986.

Addresses Maria da Paz N. Medeiros: Department of Philosophy, UFRJ, Rio de Janeiro, Brazil

E-mail: mpaz@fil.puc-rio.br

Luiz Carlos Pereira: Department of Philosophy - PUC-Rio/UFRJ, Rio de Janeiro, Brazil

E-mail: luiz@inf.puc-rio.br