Proofs of strong normalisation for second order classical natural deduction

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

Abstract

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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,347

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
67 (#244,600)

6 months
15 (#172,692)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Structural Rules in Natural Deduction with Alternatives.Greg Restall - 2023 - Bulletin of the Section of Logic 52 (2):109-143.
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.

View all 14 citations / Add more citations

References found in this work

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

Add more references