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.

Categories

Keywords

Reprint years

DOI

10.1007/s00153-010-0186-7

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 94,070

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

Cut-elimination in second order logic.O. Serebriannikov - 1988 - Bulletin of the Section of Logic 17 (3-4):159-160.
Epsilon substitution for transfinite induction.Henry Towsner - 2005 - Archive for Mathematical Logic 44 (4):397-412.
Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing.Steffen van Bakel - 2004 - Notre Dame Journal of Formal Logic 45 (1):35-63.
Describing proofs by short tautologies.Stefan Hetzl - 2009 - Annals of Pure and Applied Logic 159 (1-2):129-145.
A note on cut-elimination for classical propositional logic.Gabriele Pulcini - 2022 - Archive for Mathematical Logic 61 (3):555-565.
Duplication of directed graphs and exponential blow up of proofs.A. Carbone - 1999 - Annals of Pure and Applied Logic 100 (1-3):1-67.
Epsilon substitution for $$\textit{ID}_1$$ ID 1 via cut-elimination.Henry Towsner - 2018 - Archive for Mathematical Logic 57 (5-6):497-531.
Interpolants, cut elimination and flow graphs for the propositional calculus.Alessandra Carbone - 1997 - Annals of Pure and Applied Logic 83 (3):249-299.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.

Analytics

Added to PP
2013-11-23

Downloads
63 (#250,675)

6 months
8 (#505,344)

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