Normalization and Cut-Elimination in First-Order Logic

Dissertation, Stanford University (1986)
  Copy   BIBTEX

Abstract

Gentzen has proved cut-elimination and normalization theorems for sequent and natural deduction calculi. These theorems, it is sometimes said, convey information about the proofs represented by the derivations of these calculi. This dissertation is concerned with investigating this claim. ;The partial correspondence between the two theorems is described and the reasons why it is only partial are explained in terms of certain deficiencies of natural deduction systems. It is then argued that any system which purports to represent proofs will suffer from these or related deficiencies, and that this poses problems for the interpretation of Gentzen's theorems in terms of proofs. A multiple-conclusion version of natural deduction is then presented, and Gentzen's theorems are extended to it and compared with one another. Finally, it is argued that the obstacles in the way of establishing a full correspondence between the theorems and of interpreting them as conveying information about proofs indicate that traditional ideas about proofs are too narrow

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

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

Similar books and articles

Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Gentzen's proof systems: byproducts in a work of genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Symmetric and dual paraconsistent logics.Norihiro Kamide & Heinrich Wansing - 2010 - Logic and Logical Philosophy 19 (1-2):7-30.
Natural deduction with general elimination rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
Natural deduction systems for some non-commutative logics.Norihiro Kamide & Motohiko Mouri - 2007 - Logic and Logical Philosophy 16 (2-3):105-146.
A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.

Analytics

Added to PP
2015-02-06

Downloads
1 (#1,770,361)

6 months
1 (#1,042,085)

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Author's Profile

Anthony Ungar
State University of New York (SUNY)

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references