Journal of Philosophical Logic 36 (5):557-570 (2007)

Katalin Bimbo
University of Alberta
Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ LK $$\end{document} without any use of mix.
Keywords Philosophy
Categories (categorize this paper)
DOI 10.1007/s10992-007-9048-0
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 55,899
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

No references found.

Add more references

Citations of this work BETA

Trees for E.Shawn Standefer - 2018 - Logic Journal of the IGPL 26 (3):300-315.
A Cut-Free Sequent Calculus for Relevant Logic RW.M. Ili & B. Bori I. - 2014 - Logic Journal of the IGPL 22 (4):673-695.

Add more citations

Similar books and articles

On the Relationships Between ATR0 and $\Widehat{ID}_{.Jeremy Avigad - 1996 - Journal of Symbolic Logic 61 (3):768 - 779.
Fixed Point Theories and Dependent Choice.Gerhard Jäger & Thomas Strahm - 2000 - Archive for Mathematical Logic 39 (7):493-508.
Lemmon-Style Bases for the Systems $S1^Circ - S4^Circ$.J. Jay Zeman - 1968 - Journal of Symbolic Logic 33 (3):458-461.
LEt ® , LR °[^( ~ )], LK and Cutfree Proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.
Probabilistic Proofs and Transferability.Kenny Easwaran - 2009 - Philosophia Mathematica 17 (3):341-362.
Marginalia on Sequent Calculi.A. S. Troelstra - 1999 - Studia Logica 62 (2):291-303.
The Parallel Versus Branching Recurrences in Computability Logic.Wenyan Xu & Sanyang Liu - 2013 - Notre Dame Journal of Formal Logic 54 (1):61-78.


Added to PP index

Total views
5 ( #1,130,248 of 2,402,067 )

Recent downloads (6 months)
5 ( #156,686 of 2,402,067 )

How can I increase my downloads?


Sorry, there are not enough data points to plot this chart.

My notes