On the non-confluence of cut-elimination

Journal of Symbolic Logic 76 (1):313 - 340 (2011)
  Copy   BIBTEX

Abstract

We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

Links

PhilArchive



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

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.
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.
On the complexity of proof deskolemization.Matthias Baaz, Stefan Hetzl & Daniel Weller - 2012 - Journal of Symbolic Logic 77 (2):669-686.
On the role of implication in formal logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.

Analytics

Added to PP
2013-09-30

Downloads
16 (#911,480)

6 months
4 (#798,384)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Herbrand's theorem as higher order recursion.Bahareh Afshari, Stefan Hetzl & Graham E. Leigh - 2020 - Annals of Pure and Applied Logic 171 (6):102792.
On the form of witness terms.Stefan Hetzl - 2010 - Archive for Mathematical Logic 49 (5):529-554.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.

Add more citations

References found in this work

Proof Theory and Logical Complexity.Helmut Pfeifer & Jean-Yves Girard - 1989 - Journal of Symbolic Logic 54 (4):1493.
Grundlagen der Mathematik II.D. Hilbert & P. Bernays - 1974 - Journal of Symbolic Logic 39 (2):357-357.

Add more references