Cut elimination inside a deep inference system for classical predicate logic
Studia Logica 82 (1):51 - 71 (2006)
| Abstract | 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 | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,672 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesSara Negri (2002). Varieties of Linear Calculi. Journal of Philosophical Logic 31 (6):569-590.
Jonathan P. Seldin (2000). On the Role of Implication in Formal Logic. Journal of Symbolic Logic 65 (3):1076-1114.
Branislav R. Boričić (1986). A Cut-Free Gentzen-Type System for the Logic of the Weak Law of Excluded Middle. Studia Logica 45 (1):39 - 53.
Georg Moser & Richard Zach (2006). The Epsilon Calculus and Herbrand Complexity. Studia Logica 82 (1):133 - 155.
Sara Negri & Jan Von Plato (1998). Cut Elimination in the Presence of Axioms. Bulletin of Symbolic Logic 4 (4):418-435.
Phiniki Stouppa (2007). A Deep Inference System for the Modal Logic S. Studia Logica 85 (2):199 - 214.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads3 ( #201,837 of 549,067 )Recent downloads (6 months)1 ( #63,185 of 549,067 )How can I increase my downloads? |
My notes
Discussion
