A Cut-Elimination Proof in Positive Relevant Logic with Necessity
- PDF / 465,111 Bytes
- 32 Pages / 453.543 x 680.315 pts Page_size
- 53 Downloads / 160 Views
´ Mirjana Ilic
Abstract. This paper presents a sequent calculus for the positive relevant logic with necessity and a proof that it admits the elimination of cut. Keywords: Relevant logics, Sequent calculi, Admissibility of cut.
1.
Introduction
In this paper we consider negation-less relevant logic R [1], p. 341, with ◦ , and we set up its corco-tenability ◦ and S4-type modality , called R+ ◦ responding sequent calculus GR+ . ◦ , with the truth constant t, namely the The enrichment of the logic R+ ◦t logic R+ , is gentzenised by Belnap, Gupta and Dunn, [3], [2] §61. The use of t has become standard in formulating sequent calculi for relevant logics, after Dunn in [13] and Minc in [21] independently discovered that t, or its functional analogue, can be used in the rule of cut to prevent the inference of the modal fallacy α → (β → β). Really, with Dunn’s cut: Πϕ
Γ[ϕ] γ
Γ[Π] γ
(cut)
where Γ[Π] is the result of replacing arbitrary many occurrences of ϕ in Γ[ϕ] by Π, if Π is non-empty, and otherwise by t, the modal fallacy cannot be derived (for a more detailed explanation see [14], [15] or [1], pp. 381– 391). But, the presence of both, t or its functional analogue, in the lower sequent of cut, mismatches Gentzen’s idea of cut, where all formulae from the premises, except the cut formula, appear in the conclusion of cut. Another solution, which coincides with the Gentzen’s idea, is presented by Belnap, Gupta and Dunn in [3], where sequents are not allowed to have empty lefthand sides, they have t there instead. But, t is not the part of the standard
Presented by Heinrich Wansing; Received April 7, 2019
Studia Logica https://doi.org/10.1007/s11225-020-09920-3
c Springer Nature B.V. 2020
M. Ili´c
vocabulary {→, ∧, ∨, ∼} for R. Truly, t can be conservatively added, and after the elimination of cut, removed from the calculus, and this is exactly the procedure mostly employed, after Dunn published his Gentzen system [13], see e.g. [9,17] (of course, t is important in R: it is its strongest theorem and it plays the significant role in the algebraization of R [12]1 ). However, the inference of the modal fallacy can be prevented by another, t-free form of cut. This cut is introduced in [18], where the positive contraction-less relevant logic RW+◦ is considered, but it can also be employed in formulating sequent calculi for some other positive relevant logics. Noting that t remains important in relevant logics without permutation; it is shown in [5] how cumbersome the system may become without t (a thorough study of sequent calculi, including calculi which formalize non-classical logics, is given in [6]1 ). ◦ ◦ with our t-free form of cut. We show that GR+ is We formulate GR+ ◦ really a sequent calculus for R+ and we give a cut-elimination procedure ◦ . Instead of sequences, we use multisets (lists without order), to for GR+ build up sequents. The idea of using multisets as a data type might have originated from Curry [10]1 , but in relevant logics, multisets were first considered as a data type in [20
Data Loading...
