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

• Autorzy: Ilić M.

Identyfikatory

DOI

10.4467/20842589RM.17.006.7144

• Języki publikacji: EN

Abstrakty

EN

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

EN

relevant logic; natural deduction

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2017
• Tom: Vol. 52
• Strony: 101--132
• Opis fizyczny: Bibliogr. 18 poz., rys.

Twórcy

autor

Ilić M.

• Faculty of Economics University of Belgrade Kamenička 6, 11000 Belgrade, Serbia

Bibliografia

• [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, LE→t , 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 RW+◦, 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 Mathematical 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.

Uwagi

PL

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).