A simple proof of second-order strong normalization with permutative conversions

&
Annals of Pure and Applied Logic 136 (1-2):134-155 (2005)
  Copy   BIBTEX

Abstract

A simple and complete proof of strong normalization for first- and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions is given. The paper follows the Tait–Girard approach via computability predicates and saturated sets. Strong normalization is first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction are resolved using a new logic where disjunction is restricted to atomic formulas

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2005.05.009

Links

PhilArchive



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

External links

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

Short proofs of normalization for the simply- typed λ-calculus, permutative conversions and Gödel's T.Felix Joachimski & Ralph Matthes - 2003 - Archive for Mathematical Logic 42 (1):59-87.
Atomic polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
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 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.
Some general results about proof normalization.Marc Aiguier & Delphine Longuet - 2010 - Logica Universalis 4 (1):1-29.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Strong normalization of classical natural deduction with disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1-3):21-37.

Analytics

Added to PP
2014-01-16

Downloads
16 (#909,949)

6 months
6 (#528,006)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.
The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
Non-strictly positive fixed points for classical natural deduction.Ralph Matthes - 2005 - Annals of Pure and Applied Logic 133 (1):205-230.

View all 7 references / Add more references