Abstract
Many logics in the relevant family can be given a proof theory in the style of Belnap's display logic (Belnap, 1982). However, as originally given, the proof theory is essentially more expressive than the logics they seek to model. In this paper, we consider a modified proof theory which more closely models relevant logics. In addition, we use this proof theory to show decidability for a large range of substructural logics.
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, Volume 1, Princeton University Press, Princeton, 1975.
Anderson, A. R., Belnap, N. D. and Dunn, J. M.: Entailment: The Logic of Relevance and Necessity, Volume 2, Princeton University Press, Princeton, 1992.
Belnap, N. D.: Display Logic. Journal of Philosophical Logic 11(1982) 357–417.
Belnap, N. D.: Linear Logic Displayed. Notre Dame Journal of Formal Logic 31(1990) 15–25.
Belnap, N. D.: Life in the Undistributed Middle, in: P. Schroeder-Heister and K. Došen (eds), Substructural Logics, Oxford University Press, 1993, 31–41.
Brady, R. T.: Gentzenization and Decidability of some Contraction-Less Relevant Logics. Journal of Philosophical Logic 20 (1991) 97–117.
Dunn, J. M.: A 'Gentzen' System for Positive Relevant Inplication. Journal of Symbolic Logic 38 (1974) 356–357.
Dunn, J. M.: Relevance Logic and Entailment, in: D. Gabbay and D. Guenther (eds), Handbook of Philosophical Logic, 117–229. D. Reidel, 1986.
Giambone, S.: TW + and RW + are Decidable. Journal of Philosophical Logic 14 (1985) 235–254.
Girard, J.-Y.: Linear Logic. Theoretical Computer Science 50(1987) 1–101.
Kracht, M.: Power and Weakness of the Modal Display Calculus. Unpublished manuscript, II. Mathematiches Institut, Freue Universität Berline, 1994.
Mares, E.: CE and E. A message posted to the relevant — logic mailing list. September 1994.
Meyer, R. K.: Intuitionism, Entailment, Negation, in: H. Leblanc (ed.), Truth, Syntax and Modality, 168–198. North-Holland, 1973.
Minc, G.: Cut-Elimination Theorem in Relevant Logics (Russian), in: J. V. Matijasevic and O. A. Silenko (eds), Isslédovania po konstructivnoj mathematiké i matematičeskoj logike V, 90–97. Izdatél'stvo “Nauka”. English translation in The Journal of Soviet Mathematics 6 (1976), 422-428.
Restall, G.: Negation in Relevant Logics: How I stopped worrying and learned to love the Routley star, to appear in What is Negation?, eds Dov Gabbay and Heinrich Wansing. Oxford University Press.
Restall, G.: Simplified Semantics for Relevant Logics (and some of their rivals. Journal of Philosophical Logic) 22(1993) 481–511.
Routley, G.: A Useful Substructural Logic. Bulletin of the Interest Group in Pure and Applied Logic 2(2) (1994) 135–146.
Routley, R. and Meyer, R. K.: Semantics of Entailment 1, in: H. Leblanc (ed.), Truth, Syntax and Modality, 199–243. North-Holland, Amsterdam, 1973. Proceedings of the Temple University Conference on Alternative Semantics.
Sprenger, M. and Wymann-Böni, M.: How to decide the lark. Theoretical Computer Science 110 (1993) 419–432.
Statman, R.: The word problem for Smullyan's lark combinator is decidable. Journal of Symbolic Computation 7 (1989) 103–112.
Urquhart, A.: The Undecidability of Entailment and Relevant Implication. The Journal of Symbolic Logic 49 (1984) 1059–1073.
van Benthem, J.: Correspondence Theory, in: D. M. Gabbay and F. Guenthner (eds), Handbook of Philosophical Logic, 167–247. Reidel, 1984.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Restall, G. Displaying and Deciding Substructural Logics 1: Logics with Contraposition. Journal of Philosophical Logic 27, 179–216 (1998). https://doi.org/10.1023/A:1017998605966
Issue Date:
DOI: https://doi.org/10.1023/A:1017998605966