A Connection Between Cut Elimination and Normalization

Archive for Mathematical Logic 45 (2):113-148 (2006)
  Copy   BIBTEX

Abstract

A new set of conversions for derivations in the system of sequents for intuitionistic predicate logic will be defined. These conversions will be some modifications of Zucker's conversions from the system of sequents from [11], which will have the following characteristics: (1) these conversions will be sufficient for transforming a derivation into a cut-free one, and (2) in the natural deduction the image of each of these conversions will be either in the set of conversions for normalization procedure, or an identity of derivations. This will be used to give a new proof of the normalization theorem for natural deduction, as a consequence of the cut-elimination theorem for the system of sequents

Categories

Keywords

Reprint years

DOI

10.1007/s00153-005-0295-x

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 97,042

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

Natural deduction with general elimination rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
Strong normalization of classical natural deduction with disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1-3):21-37.
A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
A simple proof of second-order strong normalization with permutative conversions.Makoto Tatsuta & Grigori Mints - 2005 - Annals of Pure and Applied Logic 136 (1-2):134-155.
Commuting Conversions vs. the Standard Conversions of the “Good” Connectives.Fernando Ferreira & Gilda Ferreira - 2009 - Studia Logica 92 (1):63-84.
η- conversions of IPC implemented in atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.
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.
Normalization proof for Peano Arithmetic.Annika Siders - 2015 - Archive for Mathematical Logic 54 (7-8):921-940.
Normal deduction in the intuitionistic linear logic.G. Mints - 1998 - Archive for Mathematical Logic 37 (5-6):415-425.
Indexed systems of sequents and cut-elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.

Analytics

Added to PP
2013-11-23

Downloads
28 (#644,834)

6 months
8 (#836,215)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Mirjana Borisavljević
University of Belgrade

Citations of this work

An Analysis of the Rules of Gentzen’s _Nj and Lj_.Mirjana Borisavljević - 2018 - Review of Symbolic Logic 11 (2):347-370.
Normal derivations and sequent derivations.Mirjana Borisavljevi - 2008 - Journal of Philosophical Logic 37 (6):521 - 548.

Add more citations

References found in this work

[Omnibus Review].Dag Prawitz - 1991 - Journal of Symbolic Logic 56 (3):1094-1096.
The correspondence between cut-elimination and normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.
Normalization as a homomorphic image of cut-elimination.Garrel Pottinger - 1977 - Annals of Mathematical Logic 12 (3):323.
A proof of Gentzen's Hauptsatz without multicut.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (1):9-18.
A cut-elimination proof in intuitionistic predicate logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.

View all 6 references / Add more references