A natural deduction and its corresponding sequent calculus for positive contraction{less relevant logic



We give a normalizing system of natural deduction for positive contraction{less relevant logic RW+. The speci fic characteristic of our calculus is that it has a simple translational relationship to a particular sequent calculus for RW+, such that normal natural deduction derivations correspond to cut-free sequent calculus derivations and vice versa. By translations from natural deduction to sequent calculus derivations, and back, together with cut{elimination, we obtain an indirect proof of the normalization.


[1] A. Anderson and N. Belnap Jr., Entailment: the logic of relevance and necessity,
vol. 1, Princeton University Press, Princeton, New Jersey, 1975.
[2] K. Bimbo, LEt
! , LR
^, LK and cutfree proofs, Journal of Philosophical Logic 36
(2007), 557{570.
[3] R. T. Brady, Normalized natural deduction system for some relevant logics I: The
logic DW, Journal of Symbolic Logic 7:1 (2006), 35{66.
[4] A. Church, The weak theory of implication, Kontrolliertes Denken (Festgabe zum
60. Geburtstag von Prof. W. Britzelmayr), Munich 1951.
[5] J. M. Dunn, A 'Gentzen system' for positive relevant implication, The Journal of
Symbolic Logic 38 (1973), 356{357.
[6] J. M. Dunn, Relevance logic and entailment, Handbook of Philosophical Logic, vol.
3, D. Gabbay and F. Guenthner (eds.), D. Reidel Publishing Company, pp. 117{224,
[7] J. M. Dunn and G. Restall, Relevance logic, Handbook of Philosophical Logic, vol.
6, , D. Gabbay and F. Guenthner (eds.), Kluwer Academic Publlishers, pp. 1{128,
[8] G. Gentzen, Collected Papers, (ed. M. E. Szabo), North{Holland, Amsterdam, 1969.
[9] S. Giambrone, TW+ and RW+ are decidable, Journal of Philosophical Logic 14
(1985), 235{254.
[10] M. Ilic, An alternative Gentzenization of RW+
, Mathematical Logic Quarterly 62:6
(2016), 465{480.
[11] A. Kron, Decidability and interpolation for a rst {order relevance logic, Substruc-
tural Logics, P. Schroeder-Heister and K. Dosen (eds.), Oxford University Press, pp.
153{177, 1993.
[12] R. K. Meyer and M. A. McRobbie, Multisets and relevant implication I and II,
Australian Journal of Philosophy 60:2 (1982), 107{139 and 3 (1982), 265{281.
[13] G. Minc, Cut elimination theorem for relevant logics, Journal of Soviet Mathema-
tics 6 (1976), 422{428.
[14] S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press,
[15] S. Negri, A normalizing system of natural deduction for intuitionistic linear logic,
Archive for Mathematical Logic 41 (2002), 789{810.
[16] J. von Plato, Natural deduction with general elimination rules, Archive for Mathe-
matical Logic 40 (2001), 541{567.
[17] D. Prawitz, Natural Deduction. A Proof{theoretical Study, Almquist and Wiksell,
Stockholm, 1965.
[18] A. Urquhart, Relevance logic: problems open and closed, Australian Journal of Logic
13:1 (2016), Article no. 2.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.