On the form of witness terms

Archive for Mathematical Logic 49 (5):529-554 (2010)
  Copy   BIBTEX

Abstract

We investigate the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential formulas. The form of witness terms in cut-free proofs is characterized in terms of structured combinations of basic substitutions. Based on this result, a regular tree grammar computing witness terms is given and a class of proofs is shown to have only elementary cut-elimination.

Links

PhilArchive



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

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

Herbrand consistency of some arithmetical theories.Saeed Salehi - 2012 - Journal of Symbolic Logic 77 (3):807-827.
On the no-counterexample interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.
Quantum Mathematics.J. Michael Dunn - 1980 - PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1980:512 - 531.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.
A compact representation of proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
On Herbrand consistency in weak arithmetic.Zofia Adamowicz & Paweł Zbierski - 2001 - Archive for Mathematical Logic 40 (6):399-413.
A model of peano arithmetic with no elementary end extension.George Mills - 1978 - Journal of Symbolic Logic 43 (3):563-567.
On the non-confluence of cut-elimination.Matthias Baaz & Stefan Hetzl - 2011 - Journal of Symbolic Logic 76 (1):313 - 340.
Interpretability over peano arithmetic.Claes Strannegård - 1999 - Journal of Symbolic Logic 64 (4):1407-1425.
⊃E is Admissible in “true” relevant arithmetic.Robert K. Meyer - 1998 - Journal of Philosophical Logic 27 (4):327-351.
⊃E is Admissible in “true” relevant arithmetic.Robert K. Meyer - 1998 - Journal of Philosophical Logic 27 (4):327 - 351.
Complete infinitary type logics.J. W. Degen - 1999 - Studia Logica 63 (1):85-119.

Analytics

Added to PP
2013-11-23

Downloads
63 (#257,831)

6 months
8 (#370,225)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
Die Widerspruchsfreiheit der reinen Zahlentheorie.Gerhard Gentzen - 1936 - Journal of Symbolic Logic 1 (2):75-75.
Grundlagen der Mathematik II.D. Hilbert & P. Bernays - 1974 - Journal of Symbolic Logic 39 (2):357-357.
The correspondence between cut-elimination and normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.

View all 13 references / Add more references