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

Other Versions

No versions found

Links

PhilArchive

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.

Analytics

Added to PP
2014-01-16

Downloads
68 (#876,150)

6 months
22 (#485,058)

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, 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