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.

Categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Proofs of strong normalisation for second order classical natural deduction.Michel Parigot - 1997 - Journal of Symbolic Logic 62 (4):1461-1479.
Strong normalization proof with CPS-translation for second order classical natural deduction.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (3):851-859.
Natural deduction for first-order hybrid logic.Torben BraÜner - 2005 - Journal of Logic, Language and Information 14 (2):173-198.
A semantical proof of the strong normalization theorem for full propositional classical natural deduction.Karim Nour & Khelifa Saber - 2006 - Archive for Mathematical Logic 45 (3):357-364.
Strong normalization of classical natural deduction with disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1-3):21-37.
Non-strictly positive fixed points for classical natural deduction.Ralph Matthes - 2005 - Annals of Pure and Applied Logic 133 (1):205-230.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
The Geometry of Non-Distributive Logics.Greg Restall & Francesco Paoli - 2005 - Journal of Symbolic Logic 70 (4):1108 - 1126.
A Binary-conclusion Natural Deduction System.K. Fujita - 1999 - Logic Journal of the IGPL 7 (4):517-545.
Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning.Michael Gabbay & Murdoch J. Gabbay - 2005 - In Gabbay Michael & Gabbay Murdoch J. (eds.), We Will Show Them! Essays in Honour of Dov Gabbay, volume 1. pp. 701-null.
A Short Proof Of The Strong Normalization Of Classical Natural Deduction With Disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
A short proof of the strong normalization of classical natural deduction with disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
Normal Proofs, Cut Free Derivations and Structural Rules.Greg Restall - 2014 - Studia Logica 102 (6):1143-1166.
Normalization and Cut-Elimination in First-Order Logic.Anthony Michael Ungar - 1986 - Dissertation, Stanford University
Natural Deduction for Dual-intuitionistic Logic.Luca Tranchini - 2012 - Studia Logica 100 (3):631-648.

Analytics

Added to PP
2017-02-21

Downloads
2 (#1,784,141)

6 months
1 (#1,510,037)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

$lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
A Realizability Interpretation for Classical Arithmetic.Jeremy Avigad - 2002 - Bulletin of Symbolic Logic 8 (3):439-440.

View all 6 citations / Add more citations

References found in this work

No references found.

Add more references