Proof theory of paraconsistent quantum logic (Q1749807)

Minimal quantum logic or orthologic was introduced in [\textit{G. Birkhoff} and \textit{J. von Neumann}, Ann. Math. (2) 37, 823--843 (1936; JFM 62.1061.04); \textit{G. Birkhoff} and \textit{J. von Neumann}, Ann. Math. (2) 37, 823--843 (1936; Zbl 0015.14603)], and its Kripke-style semantics was provided in [\textit{R. I. Goldblatt}, J. Philos. Log. 3, 19--35 (1974; Zbl 0278.02023)]. Its Gentzen-type sequent calculi have been studied in [\textit{N. J. Cutland} and \textit{P. F. Gibbins}, Log. Anal., Nouv. Sér. 25, 221--248 (1982; Zbl 0518.03029); \textit{C. Faggian} and \textit{G. Sambin}, Int. J. Theor. Phys. 37, No. 1, 31--37 (1998; Zbl 0904.03031); the reviewer, in: Handbook of quantum logic and quantum structures. Quantum logic. With a foreword by Anatolij Dvurečenskij. Amsterdam: Elsevier/North-Holland. 227--260 (2009; Zbl 1273.03089); the reviewer, Int. J. Theor. Phys. 33, No. 7, 1427--1443 (1994; Zbl 0809.03045); the reviewer, Int. J. Theor. Phys. 33, No. 1, 103--113 (1994; Zbl 0798.03062); the reviewer, J. Symb. Log. 45, 339--352 (1980; Zbl 0437.03034); \textit{S. Tamura}, Kobe J. Math. 5, No. 1, 133--150 (1988; Zbl 0663.03050); \textit{M. Takano}, Int. J. Theor. Phys. 34, No. 4, 649--654 (1995; Zbl 0824.03032)]. Belnap and Dunn's paraconsistent four-valued logic [\textit{J. M. Dunn}, Philos. Stud. 29, No. 3, 149--168 (1976; Zbl 1435.03043); \textit{N. D. Belnap jun.}, in: Mod. uses of multiple-valued logic, 5th int. Symp., Bloomington 1975, 5--37 (1977; Zbl 0417.03009); \textit{N. D. Belnap jun.}, in: Mod. Uses of multiple-valued Logic, 5th int. Symp., Bloomington 1975, 5--37 (1977; Zbl 0424.03012)], a.k.a. \textit{A. R. Anderson} and \textit{N. D. Belnap jun.}'s first-degree entailment [Entailment. The logic of relevance and necessity. Vol. I. Princeton, N. J.: Princeton University Press (1975; Zbl 0323.02030); \textit{A. R. Anderson} et al., Entailment. The logic of relevance and necessity. Vol. II. Princeton, NJ: Princeton University Press (1992; Zbl 0921.03025)], is known to be equivalent to the $\{\wedge,\vee,\sim\}$-fragment of Nelson's paraconsistent four-valued logic [\textit{D. Nelson}, J. Symb. Log. 14, 16--26 (1949; Zbl 0033.24304); \textit{A. Almukdad} and \textit{D. Nelson}, J. Symb. Log. 49, 231--233 (1984; Zbl 0575.03016)]. Its Gentzen-type sequent calculi have been investigated in [\textit{J. M. Font}, Log. J. IGPL 5, No. 3, 413--440 (1997; Zbl 0871.03012); \textit{J. M. Font}, Log. J. IGPL 7, No. 5, 671--672 (1999; Zbl 0937.03028); \textit{N. Kamide} and \textit{H. Wansing}, Proof theory of N4-paraconsistent logics. London: College Publications (2015; Zbl 1436.03003); \textit{A. P. Pynko}, Math. Log. Q. 41, No. 4, 442--454 (1995; Zbl 0837.03019); Zbl 0323.02030]. Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, was introduced in [\textit{M. L. Dalla Chiara} and \textit{R. Giuntini}, Synthese 125, No. 1--2, 55--68 (2000; Zbl 0969.03070)]. A cut-free Gentzen-type sequent calculus for it was investigated in [Zbl 0904.03031] by extending the $\{\wedge,\vee\}$-fragment of basic logic in [\textit{G. Sambin} et al., J. Symb. Log. 65, No. 3, 979--1013 (2000; Zbl 0969.03017)]. This paper introduces four cut-free Gentzen-type sequent calculi for paraconsistent quantum logic. The first is obtained by Takano [loc. cit.] by deleting some initial sequents and negated logical inference rules. The second comes from a Gentzen-type sequent calculus for the $\{\wedge,\vee\}$-fragment of basic logic by adding some negated logical inference rules. The third derives from a Gentzen-type sequent calculus for the $\{\wedge,\vee\}$-fragment of \textit{H. Aoyama}'s weak sequent calculus LB [``On a weak system of sequent calculus'', J. Log. Philos. 3, 29--37 (2003)] by adding some negated logical inference rules. The fourth, PQL, is obtained from the third by restricting the sequent definition, being obtainable from a Gentzen-type sequent calculus for \textit{lattice logic} [\textit{G. Restall} and \textit{F. Paoli}, J. Symb. Log. 70, No. 4, 1108--1126 (2005; Zbl 1100.03049); \textit{J. Schulte Moenting}, Algebra Univers. 12, 290--321 (1981; Zbl 0528.03029)] or from \textit{finite sum-product logic} [\textit{J. R. B. Cockett} and \textit{R. A. G. Seely}, Theory Appl. Categ. 8, 63--99 (2001; Zbl 0969.03071)] by adding some negated logical inference rules. These four calculi are logically equivalent. A first-order predicate extension FPQL of PQL is shown to be decidable after the decidability of first-order \textit{substructural logics} without contraction rules.