Describing proofs by short tautologies

Annals of Pure and Applied Logic 159 (1-2):129-145 (2009)
  Copy   BIBTEX


Herbrand’s theorem is one of the most fundamental results about first-order logic. In the context of proof analysis, Herbrand-disjunctions are used for describing the constructive content of cut-free proofs. However, given a proof with cuts, the computation of a Herbrand-disjunction is of significant computational complexity, as the cuts in the proof have to be eliminated first.In this paper we prove a generalization of Herbrand’s theorem: From a proof with cuts, one can read off a small tautology composed of instances of the end-sequent and the cut formulas. This tautology describes the proof in the following way: Each cut induces a formula stating that a disjunction of instances of the cut formula implies a conjunction of instances of the cut formula. All these cut-implications together then imply the already existing instances of the end-sequent. The proof that this formula is a tautology is carried out by transforming the instances in the proof to normal forms and using characteristic clause sets to relate them. These clause sets have first been studied in the context of cut-elimination.This extended Herbrand theorem is then applied to cut-elimination sequences in order to show that, for the computation of an Herbrand-disjunction, the knowledge of only the term substitutions performed during cut-elimination is already sufficient.



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

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

Matrix identities and the pigeonhole principle.Michael Soltys & Alasdair Urquhart - 2004 - Archive for Mathematical Logic 43 (3):351-357.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Uniform Short Proofs for Classical Theorems.Kees Doets - 2001 - Notre Dame Journal of Formal Logic 42 (2):121-127.
Reasoning processes in propositional logic.Claes Strannegård, Simon Ulfsbäcker, David Hedqvist & Tommy Gärling - 2010 - Journal of Logic, Language and Information 19 (3):283-314.
On the form of witness terms.Stefan Hetzl - 2010 - Archive for Mathematical Logic 49 (5):529-554.
Probabilistic proofs and transferability.Kenny Easwaran - 2009 - Philosophia Mathematica 17 (3):341-362.
Are All Tautologies True?Philip Hugly & Charles Sayward - 1989 - Logique Et Analyse 125 (125-126):3-14.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.
Deep tautologies.Johannes Bulhof & Steven Gimbel - 2001 - Pragmatics and Cognition 9 (2):279-292.
Bounded arithmetic, propositional logic, and complexity theory.Jan Krajíček - 1995 - New York, NY, USA: Cambridge University Press.


Added to PP

16 (#911,480)

6 months
4 (#798,384)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Fragments of bounded arithmetic and the lengths of proofs.Pavel Pudl'ak - 2008 - Journal of Symbolic Logic 73 (4):1389-1406.
On the form of witness terms.Stefan Hetzl - 2010 - Archive for Mathematical Logic 49 (5):529-554.

Add more citations

References found in this work

Cut normal forms and proof complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.

Add more references