Cut elimination inside a deep inference system for classical predicate logic

Studia Logica 82 (1):51 - 71 (2006)
Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations.
Keywords cut elimination  deep inference  first-order predicate logic
Categories (categorize this paper)
DOI 10.2307/20016767
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
Download options
PhilPapers Archive

Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 15,904
External links
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA
Nuel D. Belnap (1982). Display Logic. Journal of Philosophical Logic 11 (4):375-417.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

20 ( #139,757 of 1,725,443 )

Recent downloads (6 months)

9 ( #72,316 of 1,725,443 )

How can I increase my downloads?

My notes
Sign in to use this feature

Start a new thread
There  are no threads in this forum
Nothing in this forum yet.