Strong Normalization of Classical Natural Deduction

Yuuki Andou

We show a proof of strong normalization theorem (SN) for a system of natural deduction for first order classical logic. Our system has full logical connectives primitively including those for disjunction and for existential quantifier. In [1] we have proved Church-Rosser property directly for our system and also made a comment about SN of it. Our proof of SN is obtained by using a method of de Groote. In [2] he proved SN of intuitionistic natural deduction system which includes disjunction, and in his proof essential reductions and structural reductions are treated separately. Applying his method to our system on the base of Parigot’s proof in [3] of SN for classical natural deduction, we obtain our proof which has the same separation on the treatment of two sorts of reductions.

[1] Andou, Y.; Church-Rosser property of a simple reduction for full first order classical natural deduction; Submitted.

[2] de Groote, P.; On the strong normalization of natural deduction with premutation-conversions; in: Rewriting Techniques and Applications (Springer, Berlin, 1999), LNCS 1631, 45-59.

[3] Parigot, M.; Proofs of strong normalization for second order classical natural deduction; Journal of Symbolic Logic 62 (1997) 1461-1479.

Address: Faculty of Liberal Arts(I), Hosei University, Tokyo 102-8160, JAPAN

E-mail: norakuro@i.hosei.ac.jp