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

Mirjana Ilić


We give a normalizing system of natural deduction for positive contraction - less relevant logic RW+. The specific 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.

Słowa kluczowe: relevant logic, natural deduction

[1] A. Anderson and N. Belnap Jr., Entailment: the logic of relevance and necessity, vol. 1, Princeton University Press, Princeton, New Jersey, 1975.

[2] Bimbó, Katalin. 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, 1986.

[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, 2002.

[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. Ilić, An alternative Gentzenization of   urn:x-wiley:09425616:media:malq201400084:malq201400084-math-0004  Mathematical Logic Quarterly 62:6 (2016), 465–480.

[11] A. Kron, Decidability and interpolation for a first–order relevance logic, Substructural Logics, P. Schroeder-Heister and K. Došen  (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 Mathematics 6 (1976), 422–428.

[14] S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press, 2001.

[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.