Abstract
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 \( LK \) without any use of mix.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Anderson, A. R. and Belnap, N. D.: Entailment. The Logic of Relevance and Necessity, Vol. I., Princeton University Press, Princeton, NJ, 1975.
Anderson, A. R., Belnap, N. D., and Dunn, J. M.: Entailment. The Logic of Relevance and Necessity, Vol. II, Princeton University Press, Princeton, NJ, 1992.
Belnap, N. D. and Wallace, J. R.: A decision procedure for the system \( E_{{\overline{I} }} \), of entailment with negation. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 11 (1965), 277–289.
Bimbó, K.: Admissibility of cut in LC with fixed point combinator. Studia Logica 81 (2005), 399–423.
Bimbó, K.: Relevance logics, in D. Jacquette (ed.), Philosophy of logic, vol. 5 of Handbook of the philosophy of science. D. Gabbay, P. Thagard and J. Woods (eds.), Elsevier (North-Holland), Amsterdam, 2007, pp. 723–789.
Bimbó, K. and Dunn, J. M.: Two extensions of the structurally free logic \( LC \), Logic Journal of IGPL 6 (1998), 403–424.
Dunn, J. M.: Relevance logic and entailment, in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Vol. 3, 1st edn., Reidel, Dordrecht, 1986, pp. 117–229.
Dunn, J. M. and Meyer, R. K.: Combinators and structurally free logic, Logic Journal of IGPL 5 (1997), 505–537.
Gentzen, G.: Untersuchungen über das logische Schließen, I, Mathematische Zeitschrift 39 (1935a), 176–210.
Gentzen, G.: Untersuchungen über das logische Schließen, II, Mathematische Zeitschrift 39 (1935b), 405–431.
Negri, S. and von Plato, J.: Structural Proof Theory, Cambridge University Press, Cambridge, UK, 2001.
Thistlewaite, P. B., McRobbie, M. A., and Meyer, R. K.: Automated Theorem Proving in Non-classical Logics, Pitman, London, UK, 1988.
Troelstra, A. S. and Schwichtenberg, H.: Basic proof theory, in Cambridge Tracts in Theoretical Computer Science, Vol. 43, 2nd edn. Cambridge University Press, Cambridge, UK, 2000.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Bimbó, K. \( LE^{t}_{ \to } \), \(LR^{ \circ }_{{\widehat{ \sim }}}\), LK and Cutfree Proofs. J Philos Logic 36, 557–570 (2007). https://doi.org/10.1007/s10992-007-9048-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-007-9048-0