×

Paraconsistent double negation as a modal operator. (English) Zbl 1375.03029

The author constructs a sequent calculus PM for a “paraconsistent modal-like logic” dealing with a negation operator that can simulate the necessity-operator of the S4-type. Namely, the negation connective in PM is governed by the following rules: \[ {{\alpha, \Gamma \Rightarrow \Delta}\over{{\sim\sim}\alpha, \Gamma \Rightarrow \Delta}} ({\sim\sim}\text{left}) \quad\quad {{{\sim\sim}\Gamma \Rightarrow \alpha}\over{{\sim\sim}\Gamma \Rightarrow {\sim\sim}\alpha}} ({\sim\sim}\text{right}). \]
These rules directly correspond to the following rules for the modal operator \(\square\) in S4: \[ {{\alpha, \Gamma \Rightarrow \Delta}\over{\square\alpha, \Gamma \Rightarrow \Delta}} (\square\text{left}) \quad\quad {{\square\Gamma \Rightarrow \alpha}\over{\square\Gamma \Rightarrow \square\alpha}} (\square\text{right}). \]
This observation suggests rather straight mutual translations between the PM- and S4-expressions, which in turn allows mutual embeddings of the corresponding systems. PM is shown to be decidable, cut-free and complete.

MSC:

03B53 Paraconsistent logics
03B45 Modal logic (including the logic of norms)
03F05 Cut-elimination and normal-form theorems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Almukdad, Constructible falsity and inexact predicates, J. Symb. Log. 49 (1) pp 231– (1984) · Zbl 0575.03016 · doi:10.2307/2274105
[2] Arieli, The value of the four values, Artif. Intell. 102 (1) pp 97– (1998) · Zbl 0928.03025 · doi:10.1016/S0004-3702(98)00032-0
[3] Arieli, Reasoning with logical bilattices, J. Log. Lang. Inform. 5 (1) pp 25– (1996) · Zbl 0851.03017
[4] Belnap, Modern uses of multiple-valued logic. Invited papers from the Fifth International Symposium on Multiple-Valued Logic, held at Indiana University, Bloomington, Ind., May 13-16, 1975 2 pp 5– (1977)
[5] Béziau, Paraconsistent logic from a modal viewpoint, J. Appl. Log. 3 pp 7– (2005) · Zbl 1063.03011 · doi:10.1016/j.jal.2004.07.009
[6] Došen, Negative modal operators in intuitionistic logic, Publ. Inst. Math. Beogr. 35 (49) pp 3– (1984) · Zbl 0555.03011
[7] Dunn, Intuitive semantics for first-degree entailment and ’coupled trees’, Philos. Stud. 29 (3) pp 149– (1976) · Zbl 1435.03043 · doi:10.1007/BF00373152
[8] Dunn, Philosophical Perspectives 7 pp 331– (1953)
[9] Gurevich, Intuitionistic logic with strong negation, Stud. Log. 36 pp 49– (1977) · Zbl 0366.02015 · doi:10.1007/BF02121114
[10] Horn, Negation. In: Stanford Encyclopedia of Philosophy (2016)
[11] Kamide, Proof theory of Nelson’s paraconsistent logic: a uniform perspective, Theoret. Comput. Sci. 415 pp 1– (2012) · Zbl 1382.03048 · doi:10.1016/j.tcs.2011.11.001
[12] Kamide, Studies in Logic 54 (2015)
[13] Nelson, Constructible falsity, J. Symb. Log. 14 pp 16– (1949) · Zbl 0033.24304 · doi:10.2307/2268973
[14] Rautenberg, Logik und Grundlagen der Mathematik 22 (1979)
[15] Troelstra, Cambridge Tracts in Theoretical Computer Science 43 (2000)
[16] Vorob’ev, Конструктивное исчисление высказываний с сильным отрицанием, Dokl. Akad. Nauk SSSR 85 pp 465– (1952) · Zbl 0791.14019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.