A natural deduction and its corresponding sequent calculus for positive contraction - less relevant logic
cytuj
pobierz pliki
RIS BIB ENDNOTEChoose format
RIS BIB ENDNOTEA natural deduction and its corresponding sequent calculus for positive contraction - less relevant logic
Publication date: 30.08.2017
Reports on Mathematical Logic, 2017, Number 52, pp. 93 - 124
https://doi.org/10.4467/20842589RM.17.006.7144Authors
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 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.
[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 
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.
Information: Reports on Mathematical Logic, 2017, Number 52, pp. 93 - 124
Article type: Original article
Titles:
A natural deduction and its corresponding sequent calculus for positive contraction - less relevant logic
A natural deduction and its corresponding sequent calculus for positive contraction - less relevant logic
University of Belgrade
Published at: 30.08.2017
Article status: Open
Licence: CC BY-NC-ND
Percentage share of authors:
Article corrections:
-Publication languages:
EnglishView count: 1845
Number of downloads: 1081