Cut elimination for a calculus with context-dependent rules

Archive for Mathematical Logic 40 (3):167-188 (2001)
  Copy   BIBTEX

Abstract

Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers.

Categories

Keywords

Reprint years

DOI

10.1007/s001530000058

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

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

Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
Implications-as-Rules vs. Implications-as-Links: An Alternative Implication-Left Schema for the Sequent Calculus. [REVIEW]Peter Schroeder-Heister - 2011 - Journal of Philosophical Logic 40 (1):95 - 101.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
A cut-free Gentzen formulation of basic propositional calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions.Heine Sørensen Morten & Urzyczyn Paweł - 2008 - Journal of Symbolic Logic 73 (3):919-932.
Strong Cut-Elimination in Sequent Calculus Using Klop's l-Translation and Perpetual Reductions.Sørensen Morten Heine & Urzyczyn Paweł - 2008 - Journal of Symbolic Logic 73 (3):919 - 932.
A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.
On the role of implication in formal logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Effective Cut-elimination for a Fragment of Modal mu-calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
Temporal non-commutative logic: Expressing time, resource, order and hierarchy.Norihiro Kamide - 2009 - Logic and Logical Philosophy 18 (2):97-126.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.

Analytics

Added to PP
2013-11-23

Downloads
52 (#299,806)

6 months
7 (#411,886)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Quantales and (noncommutative) linear logic.David N. Yetter - 1990 - Journal of Symbolic Logic 55 (1):41-64.

Add more references