Proofs of strong normalisation for second order classical natural deduction

Journal of Symbolic Logic 62 (4):1461-1479 (1997)

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 in [9] 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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275652
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 46,483
Through your library

References found in this work BETA

The |Lambda-Calculus.H. P. Barendregt - 1988 - Philosophical Review 97 (1):132-137.

Add more references

Citations of this work BETA

Non-Strictly Positive Fixed Points for Classical Natural Deduction.Ralph Matthes - 2005 - Annals of Pure and Applied Logic 133 (1):205-230.
Call-by-Name Reduction and Cut-Elimination in Classical Logic.Kentaro Kikuchi - 2008 - Annals of Pure and Applied Logic 153 (1-3):38-65.
A Completeness Result for the Simply Typed Λμ-Calculus.Karim Nour & Khelifa Saber - 2009 - Annals of Pure and Applied Logic 161 (1):109-118.

View all 12 citations / Add more citations

Similar books and articles


Added to PP index

Total views
50 ( #177,560 of 2,286,547 )

Recent downloads (6 months)
16 ( #52,904 of 2,286,547 )

How can I increase my downloads?


My notes

Sign in to use this feature