Proofs of strong normalisation for second order classical natural deduction. (English) Zbl 0941.03063

Summary: We give two proofs of strong normalisation for second-order classical natural deduction. The first one is an adaptation of the method of reducibility candidates introduced by J. Y. Girard [Interprétation fonctionnelle et élémination des coupures de l’arithmétique d’ordre supérieure, Ph. D. thesis, Univ. Paris VII (1972)] for second-order intuitionistic natural deduction; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a Kolmogorov translation.


03F05 Cut-elimination and normal-form theorems
03B15 Higher-order logic; type theory (MSC2010)
Full Text: DOI


[1] A semantics of evidence for classical arithmetic 60 pp 325– (1995)
[2] A new deconstructive logic: linear logic · Zbl 0895.03023
[3] DOI: 10.1016/0304-3975(75)90017-1 · Zbl 0325.68006
[4] Proceedings of the international conference on logic programming and automated reasoning pp 190– (1992)
[5] Proceedings of the Russian conference on logic programming pp 361– (1991)
[6] Proceedings of MFCS pp 439– (1990)
[7] Lambda-calcul, types et modèles (1990) · Zbl 0697.03004
[8] Proceedings of POPL pp 47– (1990)
[9] Proofs and types (1989) · Zbl 0671.68002
[10] DOI: 10.1017/S0960129500001328 · Zbl 0752.03027
[11] Logic and computer science pp 123– (1990)
[12] Theoretical Computer Science 50 (1987) · Zbl 0734.68002
[13] DOI: 10.1145/322358.322370 · Zbl 0519.68046
[14] Proceedings of CAAP ’94 pp 85– (1994)
[15] The lambda-calculus (1981)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.