Proof Theory of Paraconsistent Quantum Logic

Abstract

Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, is introduced as Gentzen-type sequent calculi, and the cut-elimination theorems for these calculi are proved. This logic is shown to be decidable through the use of these calculi. A first-order extension of this logic is also shown to be decidable. The relationship between minimal quantum logic and paraconsistent four-valued logic is clarified, and a survey of existing Gentzen-type sequent calculi for these logics and their close relatives is addressed.

1 Introduction

In this paper, we develop some cut-free Gentzen-type sequent calculi for paraconsistent quantum logic [9], a hybrid of minimal quantum logic (also traditionally called orthologic ¹) [6, 14] and Belnap-Dunn’s paraconsistent four-valued logic [5, 10]. To obtain such a cut-free calculus, we clarify the relationship among minimal quantum logic, paraconsistent four-valued logic, and their close relatives. A survey of existing Gentzen-type sequent calculi for minimal quantum logic and paraconsistent four-valued logic is also conducted with this aim. We then integrate and expand the realm of proof theories of minimal quantum logic, paraconsistent four-valued logic, and paraconsistent quantum logic.

Gentzen-type sequent calculi for minimal quantum logic [8, 12, 19–21, 25, 26] and for paraconsistent four-valued logic have both been studied [2, 13, 15, 22]. Paraconsistent four-valued logic is also known as Anderson-Belnap’s first-degree entailment [2]. Because the {∧, ∨, ~}-fragment of Nelson’s paraconsistent four-valued logic N4 [1, 18] is known to be equivalent to Belnap-Dunn’s paraconsistent four-valued logic, the existing Gentzen-type sequent calculi for N4 are also regarded as those for paraconsistent four-valued logic. Gentzen-type sequent calculi for minimal quantum logic and paraconsistent four-valued logic have been studied independently to date.

Paraconsistent quantum logic was introduced by Dalla Chiara and Giuntini [9] as weak forms of quantum logic [6, 14], for which the noncontradiction and excluded-middle laws do not hold. They introduced an axiomatization, a Kripke-style semantics, and an algebraic semantics for two forms of paraconsistent quantum logic. A cut-free Gentzen-type sequent calculus for paraconsistent quantum logic was introduced by Faggian and Sambin [12], extending the {∧, ∨}-fragment of basic logic by Sambin et al. [24]. They also called paraconsistent quantum logic basic orthologic in [12].

In this paper, four new cut-free Gentzen-type sequent calculi for paraconsistent quantum logic are introduced. The first is obtained from Takano’s Gentzen-type sequent calculus for minimal quantum logic by deleting some initial sequents and negated logical inference rules. The second is obtained from a Gentzen-type sequent calculus for the {∧, ∨}-fragment of basic logic by adding some negated logical inference rules. The third is obtained from a Gentzen-type sequent calculus for the {∧, ∨}-fragment of Aoyama’s weak sequent calculus LB [3] by adding some negated logical inference rules. The fourth, PQL, is obtained from the third by restricting the sequent definition. PQL is also obtained from a Gentzen-type sequent calculus for lattice logic by Restall and Paoli [23] and by Mönting [17] or equivalently finite sum-product logic by Cockett and Seely [7] by adding some negated logical inference rules. These four calculi are shown to be logically equivalent.

The sequents Γ ⇒ Δ of PQL have the restriction that Γ and Δ are a single formula rather than a set of formulas, i.e., Γ ⇒ Δ is of the form γ ⇒ δ, where γ and δ are formulas. This restriction is regarded as the intersection of the sequent restrictions on intuitionistic logic and dual-intuitionistic logic. This sequent restriction considerably simplifies the proofs of the cut-elimination and decidability theorems of PQL and its first-order extension in comparison with those of other proposals. No double induction on the grade and rank in the cut-elimination proofs is needed. A first-order predicate extension FPQL of PQL is simply shown to be decidable as well. This situation regarding the decidability of FPQL is similar to that of first-order substructural logics without contraction rules. Indeed, the sequent restriction prohibits the application of the contraction rules.

The remainder of this paper is structured as follows.

In Section 2, the existing Gentzen-type sequent calculi for minimal quantum logic are surveyed and a relationship among these calculi is clarified.

In Section 3, the existing Gentzen-type sequent calculi for paraconsistent four-valued logic are surveyed and a relationship among the logics discussed herein is clarified.

In Section 4, four new cut-free Gentzen-type sequent calculi, including the simplest calculus PQL, are introduced for paraconsistent quantum logic and the cut-elimination theorems for these calculi are shown. Through the use of such a calculus, paraconsistent quantum logic is shown to be decidable.

In Section 5, FPQL is introduced by extending PQL, the cut-elimination theorem for FPQL is presented, and FPQL is shown to be decidable.

2 Sequent Calculi for Minimal Quantum Logic

Prior to a detailed discussion, the language used herein is introduced below. Formulas are constructed from countably many propositional variables, ∧ (conjunction), ∨ (disjunction) and ∼ (negation). Small letters p, q,... are used to denote propositional variables, Greek small letters α, β,... are used to denote formulas, and Greek capital letters Γ, Δ,... are used to represent finite (possibly empty) sets of formulas. An expression ∼Γ is used to denote the set {∼γ | γ ∈ Γ} of formulas. The symbol ≡ is used to denote the equality of symbols. A sequent is an expression of the form Γ ⇒ Δ. An expression α ⇔ β is used to represent the abbreviation of the sequents α ⇒ β and β ⇒ α. An expression L⊢S means that a sequent S is provable in a sequent calculus L. We say that two sequent calculi L ₁ and L ₂ are theorem-equivalent if {S | L ₁⊢S} = {S | L ₂⊢S}. A rule R of inference is said to be admissible in a sequent calculus L if the following condition is satisfied: For any instance

$$\frac{S_{1} {\cdots} S_{n}}{S} $$

of R, if L⊢S _i for all i, then L⊢S. Moreover, R is said to be derivable in L if there is a derivation from S ₁,⋯ ,S _n to S in L. Note that a rule R of inference is admissible in a sequent calculus L if and only if two sequent calculi L and L + R are theorem-equivalent.

A Gentzen-type sequent calculus QL₁ for the minimal quantum logic is introduced below.

Definition 1

(QL ₁ ) The initial sequents of QL₁ are of the form:

$$\alpha \Rightarrow \alpha \sim \alpha, \alpha \Rightarrow \qquad \Rightarrow \sim \!\alpha,\alpha. $$

The structural inference rules of QL₁ are of the form:

$$\frac{\Gamma \Rightarrow \Delta}{\Sigma, \Gamma \Rightarrow \Delta, \Lambda}\mathrm{(ext)} $$

$$\frac{\Gamma \Rightarrow \alpha \quad \alpha, \Sigma \Rightarrow \Delta}{\Gamma,\Sigma \Rightarrow \Delta}(\mathrm{cut1}) \qquad \frac{\Gamma \Rightarrow \Delta, \alpha \quad \alpha \Rightarrow {\Pi}}{\Gamma \Rightarrow \Delta,{\Pi}} \ (\mathrm{cut2}). $$

The logical inference rules of QL₁ are of the form:

$$\frac{\alpha, \Gamma \Rightarrow \Delta}{\alpha \wedge \beta, \Gamma \Rightarrow \Delta} (\wedge \mathrm{left1}) \qquad \frac{\beta, \Gamma \Rightarrow \Delta}{\alpha \wedge \beta, \Gamma \Rightarrow \Delta} (\wedge \mathrm{left2})\\ $$

$$\frac{\Gamma \Rightarrow \alpha \quad \Gamma \Rightarrow \beta} {\Gamma \Rightarrow \alpha \wedge \beta} (\wedge \text{right}) \qquad \frac{\alpha \Rightarrow \Delta \quad \beta \Rightarrow \Delta}{\alpha \vee \beta \Rightarrow \Delta} (\vee \text{left})\\ $$

$$\frac{\Gamma \Rightarrow \Delta, \alpha} {\Gamma \Rightarrow \Delta, \alpha \vee \beta} (\vee \mathrm{right1}) \qquad \frac{\Gamma \Rightarrow \Delta, \beta}{\Gamma \Rightarrow \Delta, \alpha \vee \beta} (\vee \mathrm{right2})\\ $$

$$\frac{\alpha, \Gamma \Rightarrow \Delta} {\sim\sim\alpha, \Gamma \Rightarrow \Delta} (\sim\sim \text{left}) \qquad \frac{\Gamma \Rightarrow \Delta, \alpha}{\Gamma \Rightarrow \Delta, \sim\sim\alpha} (\sim\sim \text{right})\\ $$

$$\frac{\Delta \Rightarrow \Gamma} {\sim \Gamma \Rightarrow \sim\Delta}(\sim\text{twist}). $$

Proposition 2

The following rules are derivable in QL ₁ :

$$\frac{\Gamma \Rightarrow \alpha} {\sim \alpha, \Gamma \Rightarrow} (\sim \text{left}) \qquad \frac{\alpha \Rightarrow \Delta}{\Rightarrow \Delta, \sim \alpha} (\sim \text{right}) $$

$$\frac{\Gamma \Rightarrow \sim \alpha} {\alpha, \Gamma \Rightarrow} (\sim \text{left}^{-1}) \qquad \frac{\sim\alpha \Rightarrow \Delta}{\Rightarrow \Delta, \alpha} (\sim \text{right}^{-1}) $$

$$\frac{\sim\sim \alpha,\Gamma \Rightarrow \Delta} {\alpha, \Gamma \Rightarrow \Delta} (\sim\sim \text{left}^{-1}) \qquad \frac{\Gamma \Rightarrow \Delta, \sim\sim \alpha}{\Gamma \Rightarrow \Delta, \alpha} (\sim\sim \text{right}^{-1}). $$

Proof

The cases for (∼left), (∼right), (∼left⁻¹) and (∼right⁻¹) are proved by using the initial sequents of the form: ∼α, α ⇒ and ⇒∼α,α, and the rules (cut1) and (cut2). The cases for (∼∼left⁻¹) and (∼∼right⁻¹) are proved by using (∼∼left), (∼∼right), (cut1) and (cut2). □

Note that the initial sequents ∼α,α ⇒ and ⇒ ∼α,α just correspond to (∼left) and (∼right), respectively. Thus, we have the following definition and theorem.

Definition 3

(QL ₂ ) QL₂ is obtained from QL₁ by replacing the initial sequents of the form: ∼α,α ⇒ and ⇒∼α,α with the logical inference rules (∼left) and (∼right).

Theorem 4

(Equivalence between QL ₁ and QL ₂ ) QL ₁ and QL ₂ are theorem-equivalent.

A Gentzen-type sequent calculus CGL by Cutland and Gibbins [8] for the minimal quantum logic can be defined below.

Definition 5

(CG [8]) CGL is obtained from QL₂ by deleting (∼right).

Theorem 6

(Equivalence between CGL and QL ₁ ) CGL and QL ₁ are theorem-equivalent.

Proof

By Propositions 2 and 4, it is sufficient to show that the initial sequents of the form ⇒ α,∼α, which just correspond to (∼right), is derivable in QL₂ − (∼right), i.e. CGL. This is proved by:

where (∼∼right⁻¹) is derivable in CGL. □

Proposition 7

The following negated logical inference rules are derivable in QL ₁:

$$\frac{\sim\alpha \Rightarrow \Delta \quad \sim\beta \Rightarrow \Delta} {\sim(\alpha \wedge \beta) \Rightarrow \Delta} (\sim\wedge \text{left})\\ $$

$$\frac{\Gamma \Rightarrow \Delta,\sim \alpha} {\Gamma \Rightarrow \Delta, \sim (\alpha \wedge \beta)} (\sim \wedge \mathrm{right1}) \qquad \frac{\Gamma \Rightarrow \Delta, \sim \beta}{\Gamma \Rightarrow \Delta, \sim (\alpha \wedge \beta)} (\sim \wedge \mathrm{right2})\\ $$

$$\frac{\sim \alpha, \Gamma \Rightarrow \Delta} {\sim (\alpha \vee \beta), \Gamma \Rightarrow \Delta} (\sim \wedge \mathrm{left1}) \qquad \frac{\sim \beta, \Gamma \Rightarrow \Delta}{\sim (\alpha \vee \beta), \Gamma \Rightarrow \Delta} (\sim \wedge \mathrm{left2})\\ $$

$$\frac{\Gamma \Rightarrow \sim \alpha \quad \Gamma \Rightarrow \sim \beta} {\Gamma \Rightarrow \sim (\alpha \vee \beta)} (\sim \vee \text{right})\\ $$

$$\frac{\sim \alpha \Rightarrow \Delta \sim \beta \Rightarrow \Delta} {\Rightarrow \Delta, \alpha \wedge \beta} (\wedge\text{right}\natural) \qquad \frac{\Gamma \Rightarrow \sim \alpha \quad \Gamma \Rightarrow \sim \beta}{\alpha \vee \beta, \Gamma \Rightarrow} (\wedge\text{left}\natural)\\ $$

$$\frac{\Gamma \Rightarrow \alpha \quad \Gamma \Rightarrow \beta} {\sim (\alpha \wedge \beta), \Gamma\Rightarrow} (\wedge\text{left}\sharp) \qquad \frac{\alpha \Rightarrow \Delta \quad \beta \Rightarrow \Delta}{\Rightarrow \Delta, \sim (\alpha \vee \beta)} (\vee\text{right}\sharp) $$

Proof

We show only some cases. We use Proposition 2.

• 1. Case (∼∧left):

  

• 2. Case (∧right♮):

  

  where (∼∧left) is derivable in QL₁ as shown above.

• 3. Case (∧left♯):

  

□

A Gentzen-type sequent calculus TL by Takano [25] for the minimal quantum logic is defined below. TL is called GMQL^♯ in [25], and precisely speaking, GMQL^♯ was introduced as a cut-free system.

Definition 8

(TL [25]) TL is obtained from QL₁ by replacing (∼twist) with the negated logical inference rules in Proposition 7.

Theorem 9

(Equivalence between TL and QL ₁ ) TL and QL ₁ are theorem-equivalent.

Proof

By Proposition 7, the negated logical inference rules are derivable in QL₁. Thus, it is sufficient to show that (∼twist) is admissible in cut-free TL. This was proved by Takano in [25]. □

A Gentzen-type sequent calculus NL by Nishimura [20,21] for the minimal quantum logic is defined below. NL is called GMQL in [20].

Definition 10

(NL [20,21]) NL is obtained from TL by deleting the initial sequents of the form: ∼α,α ⇒ and ⇒ ∼α,α and the negated logical inference rules (∧left♯) and (∨right♯), and adding (∼twist) and the negation inference rules of the form:

$$\frac{\Gamma \Rightarrow \Delta}{\sim \Delta, \Gamma \Rightarrow}\,(\sim \text{left}\ddag) \qquad \frac{\Gamma \Rightarrow \Delta}{\Rightarrow \Delta, \sim \Gamma} (\sim \text{right}\ddag). $$

The following theorems are known [20,21,25].

Theorem 11

(Equivalence between NL and TL [25]) NL and TL are theorem-equivalent.

Theorem 12

Cut-elimination for NL and TL [20, 25]) Let L be NL or TL. The rules (cut1) and (cut2) are admissible in cut-free L.

Some remarks on other Gentzen-type sequent calculi for the minimal quantum logic are addressed as follows.

• 1. A cut-free Gentzen-type sequent calculus GOL^∗was introduced by Tamura [26]. GOL^∗ can be obtained from TL by deleting (∧left♯) and (∨right♯), and adding (∼left), (∼right) and the negation inference rule of the form:

  $$\frac{\alpha \Rightarrow \beta}{\sim \beta \Rightarrow \sim\alpha.} $$

• 2. A Gentzen-type sequent calculus GO was introduced by Nishimura [19]. GO uses the non-context-restriction cut rule (i.e., the cut rule of Gentzen’s LK) and the negation inference rules of the form:

  $$\frac{\Gamma \Rightarrow \Delta, \alpha}{\sim\alpha, \Gamma \Rightarrow \Delta} \quad\quad \frac{\alpha \Rightarrow \Delta}{\mathrm \sim \Delta \Rightarrow \sim\alpha.} $$

• 3. A cut-free Gentzen-type sequent calculus^⊥O was introduced by Faggian and Sambin [12] as an extension of (a fragment of) basic logic [24]. In^⊥O, negation is not regarded as an explicit connective, but is defined by ∼∼p := p, ∼(α∧β) := ∼α∨∼β and ∼(α∨β) := ∼α∧ ∼β where p is a propositional variable. Moreover, some more context restrictions on logical inference rules are imposed, and the negation inference rules (∼left‡) and (∼right‡) displayed in Definition 10 are adopted. For the basic logic, see the next section.

• 4. A reformulation LO for Nishimura’s GO was introduced by Aoyama [4] for investigating a relationship between the minimal quantum logic and dual-intuitionistic logic. LO has the initial sequents ∼∼α ⇒ α and α ⇒∼∼α instead of the logical inference rules (∼∼left) and (∼∼right).

• 5. A cut-free Gentzen-type sequent calculus OCL+ for the logic of orthocomplemented lattices (not for orthologic but close to it) was introduced by Mönting [17].² The calculus OCL+ adopts the restricted sequents Γ ⇒ Δ (called C-admissible sequents) where Γ and Δ are multisets of formulas such that Γ ∪ Δ where ∪ represents the multiset union contains at most two formulas. The initial sequents and logical and structural inference rules of OCL+, in which all the sequents are C-admissible, are as follows:

  $${\alpha \Rightarrow \alpha} \quad\quad \frac{\Gamma \Rightarrow \Delta,\alpha\quad \alpha, \Sigma \Rightarrow {\Pi}}{\Gamma, \Sigma \Rightarrow \Delta, {\Pi}} \quad\quad \frac{\Gamma \Rightarrow \Delta}{\alpha, \Gamma \Rightarrow \Delta} \quad\quad \frac{\Gamma \Rightarrow \Delta}{\Gamma \Rightarrow \Delta,\alpha} $$
  $$\frac{\alpha, \Gamma \Rightarrow \Delta}{\alpha\wedge\beta,\Gamma \Rightarrow \Delta} \quad\quad \frac{\beta, \Gamma \Rightarrow \Delta}{\alpha\wedge\beta,\Gamma \Rightarrow \Delta} \quad \frac{\Gamma \Rightarrow \Delta,\alpha \quad \Gamma \Rightarrow \Delta,\beta}{\Gamma \Rightarrow \Delta,\alpha\wedge\beta} $$
  $$\frac{\alpha, \Gamma \Rightarrow \Delta \quad \beta,\Gamma \Rightarrow \Delta}{\alpha \vee \beta, \Gamma \Rightarrow \Delta} \quad\quad \frac{\Gamma \Rightarrow \Delta,\alpha}{\Gamma \Rightarrow \Delta,\alpha\vee\beta} \quad\quad \frac{\Gamma \Rightarrow \Delta, \beta}{\Gamma \Rightarrow \Delta,\alpha\vee\beta} $$
  $$\frac{\Gamma \Rightarrow \Delta,\alpha}{\sim\alpha, \Gamma \Rightarrow \Delta} \quad\quad \frac{\alpha, \Gamma \Rightarrow \Delta}{\Gamma \Rightarrow \Delta, \sim\alpha.} $$

OCL+ is not a Gentzen-type sequent calculus for the minimal quantum logic, since ∼ (p ∧ q) ⇒∼p∨ ∼ q where p and q are distinct propositional variables is not provable in cut-free OCL+, but provable in cut-free NL and TL.

3 Sequent Calculi for Paraconsistent Four-Valued Logic and its Subsystems and Extensions

A Gentzen-type sequent calculus PL₁ for Belnap-Dunn’s paraconsistent four-valued logic [5, 10] is defined below.

Definition 13

(PL ₁ ) PL₁ is obtained from QL₁ by deleting the initial sequents of the form: ∼α, α ⇒ and ⇒∼α, α, replacing the structural and logical inference rules (cut1), (cut2), (∧right) and (∨left) with the structural and logical inference rules of the form:

$$\frac{\Gamma \Rightarrow {\Pi}, \alpha \quad \alpha,\Sigma \Rightarrow \Delta}{\Gamma, \Sigma \Rightarrow {\Pi}, \Delta}\,(\text{cut}) $$

$$\frac{\Gamma \Rightarrow \Delta, \alpha \quad \Gamma \Rightarrow \Delta, \beta}{\Gamma \Rightarrow \Delta, \alpha \wedge\beta}\, (\wedge{\text{right}}^{p}) \quad\quad \frac{\alpha, \Gamma \Rightarrow \Delta \quad \beta, \Gamma \Rightarrow \Delta}{\alpha\vee\beta, \Gamma \Rightarrow \Delta}\,(\vee \text{left}^{p}). $$

A Gentzen-type sequent calculus PL₂ for the paraconsistent four-valued logic is defined below.

Definition 14

(PL ₂ ) PL₂ is obtained from PL₁ by deleting (∼twist) and adding (∼∧right1), (∼∧right2), (∼∨left1), (∼∨left2) displayed in Proposition 7 and the negated logical inference rules of the form:

$$\frac{\sim\!\alpha,\Gamma \Rightarrow \Delta \quad \!\!\!\!\sim \!\beta, \!\Gamma\! \Rightarrow \!\Delta} {\sim\!(\alpha \wedge \beta), \!\Gamma\! \Rightarrow \!\Delta} \, (\sim \wedge \text{left}^{p}) \quad \frac{\Gamma \!\!\Rightarrow \!\Delta, \sim \!\alpha \quad \Gamma\!\Rightarrow \!\Delta, \sim \beta}{\Gamma\! \Rightarrow \!\Delta, \sim (\alpha \vee \beta)} \, (\sim\!\vee \text{right}^{p}). $$

The following theorem can be proved in a similar way as that for Theorem 25, which will be proved, and hence the proof is omitted here.

Theorem 15

(Equivalence between PL ₁ and PL ₂ ) PL ₁ and PL ₂ are theorem-equivalent.

We can obtain the following cut-elimination theorem for PQL₂. The following theorem can be proved in a similar way as that for Theorem 26, which will be proved, and hence the proof is omitted here.

Theorem 16

(Cut-elimination for PL ₂ ) The rule (cut) is admissible in cut-free PL ₂.

Some remarks on other Gentzen-type sequent calculi for the paraconsistent four-valued logic are addressed as follows.

• 1. A cut-free Gentzen-type sequent calculus $\mathcal {G}_{B}$ was introduced by Pynko [22]. $\mathcal {G}_{B}$ has the sequents of the form: Γ ⇒ Δ with the non-empty restriction such that both the sequences Γ and Δ of formulas are non-empty. $\mathcal {G}_{B}$ adopts some full context logical inference rules such as:

  $$\frac{\Gamma, \alpha,\beta,\Delta \Rightarrow {\Pi}}{\Gamma, \alpha\wedge\beta,\Delta \Rightarrow {\Pi}} \quad\quad \frac{\Gamma \Rightarrow \Delta,\alpha,\Sigma \quad\Gamma \Rightarrow \Delta,\beta,\Sigma} {\Gamma \Rightarrow \Delta,\alpha\wedge\beta,\Sigma} $$
  $$\frac{\Gamma, \sim\alpha, \Delta \Rightarrow {\Pi} \quad\Gamma, \sim \beta, \Delta \Rightarrow {\Pi}} {\Gamma, \sim(\alpha\wedge\beta),\Delta \Rightarrow {\Pi}} \quad\quad \frac{\Gamma \Rightarrow \Delta,\sim \alpha,\sim\beta, \Sigma}{\Gamma \Rightarrow \Delta, \sim(\alpha\wedge\beta),\Sigma.} $$

  It was shown in [22] that the structural rules including the cut rule are admissible in $\mathcal {G}_{B}$.

• 2. A Gentzen-type sequent calculus LE _{f d e2} for Anderson-Belnap’s first-degree entailment E _{f d e} or equivalently R _{f d e} [2] pp. 179-180 is obtained from Pynko’s $\mathcal {G}_{B}$ by deleting the non-empty sequent restriction and adding the inference rule (for an implication connective) of the form:

  $$\frac{\alpha \Rightarrow \beta}{\Rightarrow \alpha \to\beta} (\to \text{r}). $$

• 3. A Gentzen-type sequent calculus LE _{f d e1} for E _{f d e} [2] pp. 177-178 adopts the negation inference rules of the form:

  $$\frac{\Gamma \Rightarrow \Delta}{\Delta^{\star} \Rightarrow \Gamma^{\star}} \quad\quad \frac{\Gamma,\alpha \Rightarrow \Delta}{\Delta^{\star} \Rightarrow \Gamma^{\star},\sim \alpha} \quad\quad \frac{\Gamma \Rightarrow \Delta,\alpha}{\Delta^{\star},\sim\alpha \Rightarrow \Gamma^{\star}.} $$

  where an expression Γ^⋆ is the sequence obtained from Γ by replacing each member α of Γ by α ^⋆. An expression α ^⋆ is the result of adding a sign of negation to α if the number of outer negation signs on α is even (or zero), or the result of removing a sign of negation from α if the number is odd. We remark that α ^⋆⋆ is the same formula as α.

• 4. A Gentzen-type sequent calculus $\mathcal {G}_{FV}$ was introduced by Font and Verdú [13]. $\mathcal {G}_{FV}$ has the sequents of the form: Γ ⇒ γ with the non-empty restriction such that Γ is a non-empty sequence of formulas. $\mathcal {G}_{FV}$ has the initial sequent of the form: α ⇒ α and the structural and logical inference rules of the form:

  $$\frac{\Gamma \Rightarrow \alpha \ \ \ \alpha, \Gamma\Rightarrow \gamma} {\Gamma \Rightarrow \gamma} \quad\quad \frac{\Gamma, \beta, \alpha, \Delta \Rightarrow \gamma}{\Gamma, \alpha, \beta, \Delta \Rightarrow \gamma} \quad\quad \frac{\alpha, \alpha, \Gamma \Rightarrow \gamma}{\alpha, \Gamma \Rightarrow \gamma} \quad\quad \frac{\Gamma \Rightarrow \gamma}{\alpha, \Gamma \Rightarrow \gamma} $$
  $$\frac{\alpha, \beta,\Gamma \Rightarrow \gamma}{\alpha\wedge\beta, \Gamma \Rightarrow \gamma} \quad\quad \frac{\Gamma \Rightarrow \alpha\ \ \ \Gamma \Rightarrow \beta}{\Gamma \Rightarrow \alpha\wedge\beta} $$
  $$\frac{\alpha,\Gamma \Rightarrow \gamma \ \ \ \beta, \Gamma \Rightarrow \gamma}{\alpha\vee\beta, \Gamma \Rightarrow \gamma} \quad\quad \frac{\Gamma \Rightarrow \alpha}{\Gamma \Rightarrow \alpha\vee\beta} \quad\quad \frac{\Gamma \Rightarrow \beta}{\Gamma \Rightarrow \alpha\vee\beta} $$
  $$\frac{\alpha, \Gamma \Rightarrow \gamma}{\sim \sim\alpha, \Gamma \Rightarrow \gamma} \quad\quad \frac{\Gamma \Rightarrow \alpha}{\Gamma \Rightarrow \sim \sim\alpha} \quad\quad \frac{\alpha \Rightarrow \beta} {\sim\beta \Rightarrow \sim\alpha.} $$

• 5. Belnap-Dunn’s paraconsistent four-valued logic is also known to be equivalent to the {∧, ∨, ∼}-fragment of Nelson’s paraconsistent four-valued logic N4 [1, 18]. Various cut-fee Gentzen-type sequent calculi for N4 have been introduced and studied. The {∧, ∨, ∼}-fragments of these calculi are thus also regarded as Gentzen-type sequent calculi for Belnap-Dunn’s paraconsistent four-valued logic (see e.g., [15]). Such a cut-free Gentzen-type sequent calculus is obtained from $\mathcal {G}_{FV}$ by deleting the non-empty restriction of sequents and the context-free version of the (∼twist), and adding the negated logical inference rules of the form:

  $$\frac{\sim\alpha, \Gamma \Rightarrow \gamma \ \ \ \sim\beta, \Gamma \Rightarrow \gamma} {\sim(\alpha\wedge\beta), \Gamma \Rightarrow \gamma} \quad\quad \frac{\Gamma \Rightarrow \sim\alpha}{\Gamma \Rightarrow \sim(\alpha\wedge\beta)} \quad\quad \frac{\Gamma \Rightarrow \sim\beta}{\Gamma \Rightarrow \sim(\alpha\wedge\beta)} $$
  $$\frac{\sim\alpha, \sim\beta,\Gamma \Rightarrow \gamma}{\sim(\alpha\vee\beta), \Gamma \Rightarrow \gamma} \quad\quad \frac{\Gamma \Rightarrow \sim\alpha \ \ \ \Gamma \Rightarrow \sim\beta}{\Gamma \Rightarrow \sim(\alpha\vee\beta).} $$

Next, we consider some extensions and subsystems of PL₁.

A Gentzen-type sequent calculus CL for classical logic can be defined below.

Definition 17

(CL) CL is obtained from PL₁ by adding the initial sequents of the form: ∼α,α ⇒ and ⇒∼α,α.

The following proposition shows that CL is indeed a Gentzen-type sequent calculus for classical logic.

Proposition 18

The following negation inference rules for Gentzen’s LK for classical logic are derivable in CL:

$$\frac{\Gamma \Rightarrow \Delta, \alpha}{\sim\alpha, \Gamma \Rightarrow \Delta} (\sim \text{left}^{c}) \quad\quad \frac{\alpha, \Gamma \Rightarrow \Delta} {\Gamma \Rightarrow \Delta, \sim\alpha}(\sim \text{right}^{c}). $$

Proof

By using the initial sequents of the form ∼α,α ⇒ and ⇒∼α,α and the structural rule (cut). □

We can obtain the following extensions by adding some axiom schemes (initial sequents) to PL₁ (see [11]).

• 1. The first-degree entailment of Kleene is obtained from PL₁ by adding initial sequents of the form: ∼α,α ⇒ β.

• 2. The first-degree entailment of Priest is obtained from PL₁ by adding initial sequents of the form: β ⇒∼α,α.

• 3. The first-degree entailment of Dunn and McCall, also called the first-degree entailment of RM (R-mingle), is obtained from PL₁ by adding initial sequents of the form: ∼α,α ⇒∼β,β.

A Gentzen-type sequent calculus PQL₁ for the paraconsistent quantum logic, which is a common denominator of the minimal quantum logic and the paraconsistent four-valued logic, is defined below. Some alternative cut-free Gentzen-type sequent calculi for the paraconsistent quantum logic will be introduced in the next section.

Definition 19

(PQL ₁ ) PQL₁ is obtained from QL₁ by deleting the initial sequents of the form: ∼α,α ⇒ and ⇒∼α,α.

A Gentzen-type sequent calculus BL for the {∧, ∨}-fragment of basic logic by Sambin et al. [24] can be defined below. We will mention that the {∧, ∨}-fragments of the following logics are the same logic: lattice logic by Restall and Paoli [23] and by Mönting [17], finite sum-product logic by Cockett and Seely [7], the logic of weak sequent calculus by Aoyama and basic logic by Sambin et al.

Definition 20

(BL [24]) BL is obtained from the ∼-free part of PQL₁ by replacing (∧left1), (∧left2), (∨left1) and (∨left2) with the logical inference rules of the form:

$$\frac{\alpha \Rightarrow \Delta}{\alpha\wedge\beta \Rightarrow \Delta} (\wedge \text{left1}^{b}) \quad\quad \frac{\beta \Rightarrow \Delta}{\alpha\wedge\beta \Rightarrow \Delta} [(\wedge \text{left2}^{b})] $$

$$\frac{\Gamma \Rightarrow \alpha}{\Gamma \Rightarrow \alpha\vee\beta} (\vee \text{right1}^{b}) \quad\quad \frac{\Gamma \Rightarrow \beta}{\Gamma \Rightarrow \alpha\vee\beta} (\vee \text{right2}^{b}). $$

The following cut-elimination theorem for BL is known [24].

Theorem 21

(Cut-elimination for BL [24]) The rules (cut1) and (cut2) are admissible in cut-free BL.

It is remarked that the original “full” basic logic has other logical connectives such as implication, co-implication, negation and co-negation. For example, the negation inference rules of the full basic logic are of the form:

$$\frac{\alpha \Rightarrow}{\Rightarrow \neg\alpha} \quad\quad \frac{\Rightarrow \alpha}{\neg \alpha \Rightarrow} \quad\quad \frac{\alpha \Rightarrow \beta}{\neg \beta \Rightarrow \neg \alpha.} $$

We can obtain Fig. 1 as a perspective on the relationship among the logics discussed. In Fig. 1, QL means QL₁ for the minimal quantum logic, PL means PL₁ for the paraconsistent four-valued logic, and PQL means PQL₁ for the paraconsistent quantum logic. The arrow denoted as L ₁ → L ₂ in Fig. 1 means that L ₂ is an extension of L ₁. The “context” displayed in Fig. 1 means that the context restriction on some inference rules are canceled. For example, (∧right^p) in PL₁ is obtained from (∧right) in PQL₁ by canceling the context restriction, i.e., (∧right) is obtained from (∧right^p) by deleting the context Δ.

Fig. 1

Relationship among logics

4 Sequent Calculi for Paraconsistent Quantum Logic

A Gentzen-type sequent calculus PQL₂ for the paraconsistent quantum logic is introduced as follows: It is obtained from TL by deleting the initial sequents of the form: ∼α,α ⇒ and ⇒∼α,α, and the negated logical inference rules (∧right♮), (∨left♮), (∧left♯) and (∨right♯). For the sake of readability, PQL₂ is re-displayed below.

Definition 22

(PQL ₂ ) The initial sequents of PQL₂ are of the form:

$$\alpha \Rightarrow \alpha. $$

The structural inference rules of PQL₂ are of the form:

$$\frac{\Gamma\Rightarrow \Delta}{\Sigma, \Gamma \Rightarrow \Delta, \Lambda}\ (\text{ext}) $$

$$\frac{\Gamma \Rightarrow \alpha \ \ \ \alpha,\Sigma \Rightarrow \Delta} {\Gamma,\Sigma \Rightarrow \Delta}(\text{cut1}) \quad\quad \frac{\Gamma \Rightarrow \Delta,\alpha \ \ \ \alpha \Rightarrow {\Pi}} {\Gamma \Rightarrow \Delta,{\Pi}}(\text{cut2}). $$

The logical inference rules of PQL₂ are of the form:

$$\frac{\alpha,\Gamma \Rightarrow \Delta}{\alpha\wedge\beta, \Gamma \Rightarrow \Delta}(\wedge \text{left1}) \quad\quad \frac{\beta, \Gamma \Rightarrow \Delta}{\alpha\wedge\beta, \Gamma \Rightarrow \Delta} \ (\wedge \text{left2}) $$

$$\frac{\Gamma \Rightarrow \alpha \ \ \ \Gamma \Rightarrow \beta} {\Gamma \Rightarrow \alpha\wedge \ \beta} \ (\wedge \text{right}) \quad\quad \frac{\alpha \Rightarrow \Delta \ \ \ \beta \Rightarrow \Delta} {\alpha\vee\beta \Rightarrow \Delta}(\vee \text{left}) $$

$$\frac{\Gamma \Rightarrow \Delta, \alpha}{\Gamma \Rightarrow \Delta, \alpha\vee\beta} \ (\vee \text{right1}) \quad\quad \frac{\Gamma \Rightarrow \Delta, \beta}{\Gamma \Rightarrow \Delta, \alpha\vee\beta} \ (\vee \text{right2}) $$

$$\frac{\alpha, \Gamma \Rightarrow \Delta}{\sim \sim\alpha, \Gamma \Rightarrow \Delta} \ (\sim \sim \text{left}) \quad\quad \frac{\Gamma \Rightarrow \Delta,\alpha}{\Gamma \Rightarrow \Delta, \sim \sim\alpha} \ (\sim \sim \text{right}) $$

$$\frac{\sim\alpha \Rightarrow \Delta \ \ \ \sim \beta \Rightarrow \Delta} {\sim(\alpha\wedge\beta) \Rightarrow \Delta} \ (\sim\wedge \text{left}) $$

$$\frac{\Gamma \Rightarrow \Delta, \sim\alpha}{\Gamma \Rightarrow \Delta, \sim(\alpha\wedge\beta)} \ (\sim\wedge \text{right1}) \quad\quad \frac{\Gamma \Rightarrow \Delta, \sim\beta}{\Gamma \Rightarrow \Delta, \sim(\alpha\wedge\beta)} \ (\sim\wedge \text{right2}) $$

$$\frac{\sim\alpha, \Gamma \Rightarrow \Delta}{\sim(\alpha\vee\beta), \Gamma \Rightarrow \Delta} \ (\sim\vee \text{left1}) \quad\quad \frac{\sim\beta, \Gamma \Rightarrow \Delta}{\sim(\alpha\vee\beta), \Gamma \Rightarrow \Delta} \ (\sim\vee \text{left2}) $$

$$\frac{\Gamma \Rightarrow \sim\alpha \ \ \ \Gamma \Rightarrow \sim\beta}{\Gamma \Rightarrow \sim(\alpha\vee\beta)} \ (\sim\vee \text{right}). $$

Lemma 23

The rules (∼∼left ⁻¹) and (∼∼right ⁻¹) in Proposition 2 are admissible in cut-free PQL ₂.

Proof

We consider only the case for (∼∼left⁻¹) since the case for (∼∼right⁻¹) can be obtained similarly. The proof can be obtained by induction on the proofs P of the upper sequent ∼∼α, Γ ⇒ Δ of (∼∼left⁻¹) in cut-free PQL₂. □

Lemma 24

The rule (∼twist) is admissible in cut-free PQL ₂.

Proof

By induction on the proofs P of the upper sequent Δ ⇒ Γ of (∼twist) in cut-free PQL₂. We distinguish the cases according to the last inference of P. We show only some cases. We use Lemma 23.

• 1. Case (∧right): The last inference of P is of the form:

  $$\frac{\Delta \Rightarrow \alpha \ \ \ \Delta \Rightarrow \beta} {\Delta \Rightarrow \alpha \wedge \beta} \ (\wedge \text{right}). $$

  In this case, we have PQL₂ ⊢ ∼α ⇒∼Δ and PQL₂⊢∼β ⇒∼Δ by induction hypothesis. Then, we obtain the required fact:

  $$\frac{\sim \alpha \overset{\vdots}{\Rightarrow} \sim \Delta \sim \beta \overset{\vdots}{\Rightarrow} \sim \Delta} {\sim (\alpha \wedge \beta) \Rightarrow \sim \Delta } \ (\sim \wedge \text{left}). $$

• 2. Case (∼∼left): The last inference of P is of the form:

  $$\frac{\alpha, \Delta^{\prime} \Rightarrow \Gamma}{\sim \sim \alpha, \Delta^{\prime} \Rightarrow \Gamma} \ (\sim \sim \text{left}). $$

  In this case, we have PQL₂ ⊢ ∼Γ ⇒ ∼Δ^′, ∼α by induction hypothesis. Then, we obtain the required fact:

  $$\frac{\sim \Gamma \Rightarrow \overset{\vdots}{\sim} \Delta^{\prime}, \sim \alpha}{\sim \Gamma \Rightarrow \sim \Delta^{\prime}, \sim \sim \sim \alpha}(\sim \sim \text{right}). $$

• 3. Case (∼∧left): The last inference of P is of the form:

  $$\frac{\sim \alpha \Rightarrow \Gamma \ \ \ \sim \beta \Rightarrow \Gamma} {\sim (\alpha \wedge \beta) \Rightarrow \Gamma} \ (\sim \wedge \text{left}). $$

  In this case, we have PQL₂ ⊢ ∼Γ ⇒ ∼∼α and PQL₂ ⊢ ∼Γ ⇒ ∼∼β by induction hypothesis. Then, we obtain the required fact:

  

  where (∼∼right⁻¹) is admissible in cut-free PQL₂ by Lemma 23.

□

Theorem 25

(Equivalence between PQL ₁ and PQL ₂ ) PQL ₁ and PQL ₂ are theorem-equivalent.

Proof

As shown in Proposition 2, the negated logical inference rules of PQL₂ are derivable in PQL₁, By Lemma 24, (∼twist) of PQL₁ is admissible in cut-free PQL₂. Therefore, PQL₂ and PQL₁ are theorem-equivalent. □

The following cut-elimination theorem can be obtained by the standard proof method by Gentzen. However, we here obtain an alternative proof of the theorem.

Theorem 26

(Cut-elimination for PQL ₂ ) The rules (cut1) and (cut2) are admissible in cut-free PQL ₂.

Proof

We assume the cut-elimination theorem for the ∼-free fragment PQL⁺ of PQL₂ since the cut-elimination theorem for PQL⁺ can be obtained by the fact that TL is conservative over PQL⁺. This conservative extension result is obtained from Theorem 12. We also assume the systems which have the initial sequents of the form: p ⇒ p and ∼p ⇒∼p for any propositional variable p, i.e., the system obtained from PQL₂ by replacing α ⇒ α with p ⇒ p and ∼p ⇒∼p, and the system obtained from PQL⁺ by replacing α ⇒ α with p ⇒ p. The initial sequents of the form: α ⇒ α for any formula α are provable in these modified systems without the cut rules. This fact can be shown by induction on α. Thus, we use the same names PQL₂ and PQL⁺ for these modified systems, and identify these original and modified systems. In the following, we give an embedding-based proof of the cut-elimination theorem for (modified) PQL₂.

Firstly, we introduce a translation of PQL₂ into PQL⁺. We fix a set Φ of propositional variables and define the set Φ^′ := {p ^′ | p ∈ Φ} of propositional variables. The language $\mathcal {L}_{\text {PQL}_{2}}$ of PQL₂ is defined using Φ, ∧, ∨ and ∼. The language $\mathcal {L}_{\text {PQL}^{+}}$ of PQL⁺ is defined using Φ, Φ^′, ∧ and ∨. A mapping f from $\mathcal {L}_{\text {PQL}_{2}}$ to $\mathcal {L}_{\text {PQL}^{+}}$ is defined inductively by:

• 1. for any p ∈ Φ, f(p): = p and f(∼p) := p ^′ ∈ Φ^′,

• 2. f(α ♯ β):= f(α) ♯ f(β) with ♯∈{∧, ∨},

• 3. f(∼∼α):= f(α),

• 4. f(∼(α ∧ β)) := f(∼α) ∨ f(∼β),

• 5. f(∼(α ∨ β)) := f(∼α) ∧ f(∼β).

An expression f(Γ) denotes the result of replacing every occurrence of a formula α in Γ by an occurrence of f(α).

Next, we show a proposition for embedding PQL₂ into PQL⁺. Let Γ, Δ be finite sets of formulas in $\mathcal {L}_{\text {PQL}_{2}}$, and f be the mapping defined above. Then, we obtain the following proposition.

• 1. If PQL₂⊢ Γ ⇒ Δ, then PQL⁺ ⊢ f(Γ) ⇒ f(Δ).

• 2. If PQL⁺−{(cut1),(cut2)} ⊢f(Γ) ⇒ f(Δ), then PQL₂ − {(cut1),(cut2)}⊢Γ ⇒ Δ.

Firstly, we show (1) by induction on the proofs P of Γ ⇒ Δ in PQL₂. We distinguish the cases according to the last inference of P, and show some cases.

• 1. Case (∼ p ⇒∼ p): The last inference of P is of the form: ∼p ⇒∼p for any p∈ Φ. In this case, we obtain PQL⁺ ⊢ f(∼p) ⇒ f(∼p), i.e., PQL⁺⊢ p ^′ ⇒ p ^′ (p ^′ ∈ Φ^′), by the definition of f.

• 2. Case (∼∼left): The last inference of P is of the form:

  $$\frac{\alpha, \Gamma \Rightarrow \Delta}{\sim \sim \alpha, \Gamma \Rightarrow \Delta}\ (\sim \sim \text{left}). $$

  By induction hypothesis, we have the required fact PQL⁺⊢f(α), f(Γ) ⇒ f(Δ) where f(α) coincides with f(∼∼α) by the definition of f.

• 3. Case (∼∧left): The last inference of P is of the form:

  $$\frac{\sim \alpha \Rightarrow \Delta \ \ \ \sim \beta \Rightarrow \Delta}{\sim (\alpha \wedge \beta) \Rightarrow \Delta} \ (\sim\!\wedge \text{left}). $$

  By induction hypothesis, we have the facts PQL⁺⊢f(∼α) ⇒ f(Δ) and PQL⁺⊢f(∼β) ⇒ f(Δ). We then obtain the required fact

  $$\frac{f(\sim \alpha) \overset{\vdots}{\Rightarrow} f(\Delta) \ \ \ f(\sim \beta) \overset{\vdots}{\Rightarrow} f(\Delta)}{f(\sim \alpha) \vee f(\sim \beta) \Rightarrow f(\Delta)} \ (\vee \text{left}). $$

  where f(∼α) ∨f(∼β) coincides with f(∼(α∧β)) by the definition of f.

Next, we show (2) by induction on the proofs Q of f(Γ) ⇒ f(Δ) in cut-free PQL⁺. We distinguish the cases according to the last inference of P, and show only the following case.

Case (∨left): The last inference of Q is (∨left).

• 1. Subcase (1): The last inference of Q is of the form:

  $$\frac{f(\alpha) \Rightarrow f(\Delta) \quad f(\beta) \Rightarrow f(\Delta)} {f(\alpha \vee \beta) \Rightarrow f(\Delta)}(\vee \text{left}) $$

  where f(α∨β) coincides with f(α) ∨f(β) by the definition of f. In this case, we have PQL₂ − {(cut1),(cut2)} ⊢ α ⇒ Δ and PQL₂ − {(cut1),(cut2)} ⊢ β ⇒ Δ by induction hypothesis. We then obtain the required fact:

  $$\frac{\alpha \overset{\vdots} {\Rightarrow} \Delta\quad \beta \overset{\vdots}{\Rightarrow} \Delta} {\alpha \vee\beta \Rightarrow \Delta}(\vee \text{left}). $$

• 2. Subcase (2): The last inference of Q is of the form:

  $$\frac{f(\sim \alpha) \Rightarrow f(\Delta)\quad f(\sim \beta) \Rightarrow f(\Delta)} {f(\sim (\alpha \wedge \beta)) \Rightarrow f(\Delta)}(\vee \text{left}) $$

  where f(∼(α ∧ β)) coincides with f(∼α) ∨f(∼β) by the definition of f. In this case, we have PQL₂ − {(cut1),(cut2)} ⊢∼α ⇒ Δ and PQL₂ − {(cut1),(cut2)} ⊢∼β ⇒ Δ by induction hypothesis. We then obtain the required fact:

  $$\frac{\sim \alpha \overset{\vdots}{\Rightarrow} \Delta \ \ \sim \beta \overset{\vdots}{\Rightarrow} \Delta} {\sim (\alpha \wedge \beta) \Rightarrow \Delta}(\sim \wedge \text{left}). $$

Finally, we show the cut-elimination theorem for PQL₂ as follows. Suppose PQL₂ ⊢ Γ ⇒ Δ. Then, we have PQL⁺⊢f(Γ) ⇒ f(Δ) by the proposition (1) just shown above. Thus, by the cut-elimination theorem for PQL⁺, we obtain PQL⁺ − {(cut1), (cut2)} ⊢f(Γ) ⇒ f(Δ). By the above proposition (2), we then obtain the required fact PQL₂ − {(cut1), (cut2)} ⊢ Γ ⇒ Δ. □

We can obtain the following theorem.

Theorem 27

(Decidability for PQL ₂ ) PQL ₂ , i.e., the paraconsistent quantum logic, is decidable.

Proof

We assume the decidability of the positive fragment PQL⁺ of PQL₂ since this fact is obtained from the decidability of the minimal quantum logic. Let f be the mapping used in the proof of Theorem 26. By decidability of PQL⁺, for each α, it is possible to decide if ⇒ f(α) is provable in PQL⁺. Then, by the proposition shown in the proof of Theorem 26, PQL₂ is also decidable. □

A Gentzen-type sequent calculus PQL₃ for the paraconsistent quantum logic is obtained from BL by adding some negated logical inference rules with some context restrictions. PQL₃ is precisely defined below.

Definition 28

(PQL ₃ ) The initial sequents and structural inference rules of PQL₃ are the same as those of PQL₂.

The logical inference rules of PQL₃ are of the form:

$$\frac{\alpha \Rightarrow \Delta}{\alpha\wedge\beta \Rightarrow \Delta} \ (\wedge \text{left1}^{b}) \quad\quad \frac{\beta \Rightarrow \Delta}{\alpha\wedge\beta \Rightarrow \Delta}(\wedge \text{left2}^{b}) $$

$$\frac{\Gamma \Rightarrow \alpha \quad \Gamma \Rightarrow \beta}{\Gamma \Rightarrow \alpha\wedge\beta} \ (\wedge \text{right}) \quad\quad \frac{\alpha \Rightarrow \Delta \quad \beta \Rightarrow \Delta}{\alpha\vee\beta \Rightarrow \Delta} (\vee \text{left}) $$

$$\frac{\Gamma \Rightarrow \alpha}{\Gamma \Rightarrow \alpha\vee\beta} \ (\vee \text{right1}^{b}) \quad\quad \frac{\Gamma \Rightarrow \beta}{\Gamma \Rightarrow \alpha\vee\beta} (\vee \text{right2}^{b}) $$

$$\frac{\alpha \Rightarrow \Delta}{\sim \sim\alpha \Rightarrow \Delta } \ (\sim \sim \text{left}^{b}) \quad\quad \frac{\Gamma \Rightarrow \alpha}{\Gamma \Rightarrow \sim \sim\alpha} \ (\sim \sim \text{right}^{b}) $$

$$\frac{\sim\alpha \Rightarrow \Delta \quad \sim\beta \Rightarrow \Delta}{\sim(\alpha\wedge\beta) \Rightarrow \Delta} \ (\sim\wedge \text{left}) $$

$$\frac{\Gamma \Rightarrow \sim \alpha}{\Gamma \Rightarrow \sim (\alpha\wedge\beta)} \ (\sim\wedge \text{right1}^{b}) \quad\quad \frac{\Gamma \Rightarrow \sim\beta}{\Gamma \Rightarrow \sim(\alpha\wedge\beta)} \ (\sim\wedge \text{right2}^{b}) $$

$$\frac{\sim\alpha \Rightarrow \Delta}{\sim(\alpha\vee\beta) \Rightarrow \Delta} (\sim\vee \text{left1}^{b}) \quad\quad \frac{\sim\beta \Rightarrow \Delta}{\sim(\alpha\vee\beta) \Rightarrow \Delta} \ (\sim\vee \text{left2}^{b}) $$

$$\frac{\Gamma \Rightarrow \sim\alpha \quad \Gamma \Rightarrow \sim\beta}{\Gamma \Rightarrow \sim (\alpha\vee\beta)} \ (\sim\vee \text{right}). $$

If Γ is a non-empty set {γ ₁, γ ₂, ...,γ _n} of formulas, where the sequence 〈γ ₁, γ ₂, ...γ _n〉 of the formulas in Γ is assumed to be uniquely determined, then Γ ^∧ and Γ^∨ represent γ ₁ ∧ γ ₂ ∧ ⋯ ∧ γ _n and γ ₁ ∨ γ ₂ ∨ ⋯ ∨ γ _n, respectively. If Γ is empty, then Γ ^∧ and Γ^∨ represent the empty set.

Theorem 29

(Equivalence between PQL ₂ and PQL ₃ ) For any sequent Γ ⇒ Δ, PQL ₂ ⊢ Γ ⇒ Δ iff PQL ₃ ⊢ Γ^∧ ⇒ Δ^∨.

Proof

(⇒): By induction on the proofs P of Γ ⇒ Δ in PQL₂. We distinguish the cases according to the last inference of P. We show only the following case.

Case (∧left1): The last inference of P is of the form:

$$\frac{\alpha, \Gamma, \Rightarrow \Delta}{\alpha\wedge\beta, \Gamma \Rightarrow \Delta} \ (\wedge \text{left1}). $$

In the following, we consider only the case for Γ ≠ ∅. By induction hypothesis, we have PQL₃ ⊢ α ∧ Γ^∧ ⇒ Δ^∨. Then, we obtain the required fact:

where P ₁ is of the form:

(⇐): By induction on the proofs Q of Γ^∧ ⇒ Δ^∨ in PQL₃. We distinguish the cases according to the last inference of Q. We show only the following case.

Case (∼∨right): The last inference of Q is of the form:

$$\frac{\Gamma^{\wedge} \Rightarrow \sim\alpha \quad \Gamma^{\wedge} \Rightarrow \sim\beta}{\Gamma^{\wedge} \Rightarrow \sim(\alpha\vee\beta)}(\sim\vee \text{right}). $$

By induction hypothesis, we have PQL₂ ⊢ Γ ⇒∼α and PQL₂ ⊢ Γ ⇒∼β. Then we obtain the required fact:

$$\frac{\Gamma \overset{\vdots}{\Rightarrow} \sim\alpha \quad \Gamma \overset{\vdots}{\Rightarrow} \sim\beta}{\Gamma \Rightarrow \sim(\alpha\vee\beta)} (\sim\vee \text{right}). $$

□

Theorem 30

(Cut-elimination for PQL ₃ ) The rules (cut1) and (cut2) are admissible in cut-free PQL ₃.

Proof

Similar to the proof of Theorem 26. By using the cut-elimination theorem for BL and a proposition for embedding PQL₃ into BL. □

A Gentzen-type sequent calculus PQL₄ for the paraconsistent quantum logic is obtained from PQL₃ by restricting the sequents in which both the antecedents and the succedents are singular. This restriction of sequents was proposed by Aoyama in [3]. PQL₄ is precisely defined below.

Definition 31

(PQL ₄ ) The sequents Γ ⇒ Δ of PQL₄ have the restriction that Γ and Δ consist of at most one formula. In the following definition, Γ and Δ represent a formula or the empty set.

The initial sequents of PQL₄ are the same as those of PQL₃.

The structural inference rule of PQL₄ is of the form:

$$\frac{\Gamma \Rightarrow \alpha \quad \alpha \Rightarrow \Delta}{\Gamma \Rightarrow \Delta} \ (\text{cut}^{a}). $$

The logical inference rules of PQL₄ are of the form:

$$\frac{\alpha \Rightarrow \Delta}{\alpha\wedge\beta \Rightarrow \Delta} \ (\wedge \text{left1}^{a}) \quad\quad \frac{\beta \Rightarrow \Delta}{\alpha\wedge\beta \Rightarrow \Delta} \ (\wedge \text{left2}^{a}) $$

$$\frac{\Gamma \Rightarrow \alpha \quad \Gamma \Rightarrow \beta}{\Gamma \Rightarrow \alpha\wedge\beta} \ (\wedge \text{right}^{a}) \quad\quad \frac{\alpha \Rightarrow \Delta \quad \beta \Rightarrow \Delta}{\alpha\vee\beta \Rightarrow \Delta} \ (\vee \text{left}^{a}) $$

$$\frac{\Gamma \Rightarrow \alpha}{\Gamma \Rightarrow \alpha\vee\beta} \ (\vee \text{right1}^{a}) \quad\quad \frac{\Gamma \Rightarrow \beta}{\Gamma \Rightarrow \alpha\vee\beta} \ (\vee \text{right2}^{a}) $$

$$\frac{\alpha \Rightarrow \Delta}{\sim \sim\alpha \Rightarrow \Delta} \ (\sim \sim \text{left}^{a}) \quad\quad \frac{\Gamma \Rightarrow \alpha}{\Gamma \Rightarrow \sim \sim\alpha} \ (\sim \sim \text{right}^{a}) $$

$$\frac{\sim\alpha \Rightarrow \Delta \quad \sim\beta \Rightarrow \Delta}{\sim(\alpha\wedge\beta) \Rightarrow \Delta}(\sim\wedge \text{left}^{a}) $$

$$\frac{\Gamma \Rightarrow \sim\alpha}{\Gamma \Rightarrow \sim(\alpha\wedge\beta)} \ (\sim\wedge \text{right1}^{a}) \quad\quad \frac{\Gamma \Rightarrow \sim\beta}{\Gamma \Rightarrow \sim(\alpha\wedge\beta)} \ (\sim\wedge \text{right2}^{a}) $$

$$\frac{\sim\alpha \Rightarrow \Delta}{\sim(\alpha\vee\beta) \Rightarrow \Delta} \ (\sim\vee \text{left1}^{a}) \quad\quad \frac{\sim\beta \Rightarrow \Delta}{\sim(\alpha\vee\beta) \Rightarrow \Delta} \ (\sim\vee \text{left2}^{a}) $$

$$\frac{\Gamma \Rightarrow \sim\alpha \quad \Gamma \Rightarrow \sim\beta}{\Gamma \Rightarrow \sim(\alpha\vee\beta)} \ (\sim\vee \text{right}^{a}). $$

PQL₄ is an extension of the {∧, ∨}-fragment of a weak sequent calculus LB by Aoyama [3]. A Gentzen-type sequent calculus called here AL for the {∧, ∨}-fragment of LB can be defined as follows.

Definition 32

(AL [3]) AL is the ∼-free part of PQL₄.

The following theorem is known [3].

Theorem 33

(Cut-elimination for AL [3]) The rule (cut ^a) is admissible in cut-free AL.

The original LB has the implication and negation connectives as well as the universal and existential quantifiers. Moreover, LB has the structural rues of the form:

$$\frac{\Rightarrow \Delta}{\alpha \Rightarrow \Delta} \quad\quad \frac{\Gamma \Rightarrow}{\Gamma \Rightarrow \alpha} $$

since LB has the negation and implication inference rules of the form:

$$\frac{\Rightarrow \alpha}{\neg\alpha \Rightarrow} \quad\quad \frac{\alpha \Rightarrow}{\Rightarrow \neg\alpha} \quad\quad \frac{\Rightarrow \alpha \quad \beta \Rightarrow \Delta}{\alpha \to \beta \Rightarrow \Delta} \quad\quad \frac{\alpha \Rightarrow \beta}{\Rightarrow \alpha \to \beta.} $$

The cut-elimination theorem for LB was addressed in [3].

Then, we can obtain the following theorems in a similar way as for PQL₃.

Theorem 34

(Equivalence between PQL ₂ and PQL ₄ ) For any sets Γ and Δ of formulas, PQL ₂ ⊢ Γ ⇒ Δ iff PQL ₄ ⊢ Γ^∧ ⇒ Δ^∨.

Theorem 35

(Cut-elimination for PQL ₄ ) The rule (cut ^a ) is admissible in cut-free PQL ₄.

Note that AL and BL are also logically equivalent in the sense of Theorem 34, and AL is regarded as an alternative Gentzen-type sequent calculus for the {∧, ∨}-fragment of the basic logic. Note also that the sequents of the form Γ ⇒ and ⇒ Δ are not provable in cut-free PQL₄.

A Gentzen-type sequent calculus PQL for the paraconsistent quantum logic is obtained from PQL₄ by further restricting the sequent definition.

Definition 36

(PQL) The sequents of PQL are of the form γ ⇒ δ for any formulas γ and δ, i.e., γ ⇒ and ⇒ δ cannot be a sequent.

The initial sequents of PQL are the same as those of PQL₄.

The structural inference rule of PQL is of the form:

$$\frac{\gamma \Rightarrow \alpha \quad \alpha \Rightarrow \delta}{\gamma \Rightarrow \delta} \ (\text{cut}^{k}). $$

The logical inference rules of PQL are of the form:

$$\frac{\alpha \Rightarrow \delta}{\alpha\wedge\beta \Rightarrow \delta} \ (\wedge \text{left1}^{k}) \quad\quad \frac{\beta \Rightarrow \delta}{\alpha\wedge\beta \Rightarrow \delta} \ (\wedge \text{left2}^{k}) $$

$$\frac{\gamma \Rightarrow \alpha \quad \gamma \Rightarrow \beta}{\gamma \Rightarrow \alpha\wedge\beta} \ (\wedge \text{right}^{k}) \quad\quad \frac{\alpha \Rightarrow \delta \quad \beta \Rightarrow \delta}{\alpha\vee\beta \Rightarrow \delta} \ (\vee \text{left}^{k}) $$

$$\frac{\gamma \Rightarrow \alpha}{\gamma \Rightarrow \alpha\vee\beta} \ (\vee \text{right1}^{k}) \quad\quad \frac{\gamma \Rightarrow \beta}{\gamma \Rightarrow \alpha\vee\beta} \ (\vee \text{right2}^{k}) $$

$$\frac{\alpha \Rightarrow \delta}{\sim \sim\alpha \Rightarrow \delta} \ (\sim \sim \text{left}^{k}) \quad\quad \frac{\gamma \Rightarrow \alpha}{\gamma \Rightarrow \sim \sim\alpha} \ (\sim \sim \text{right}^{k}) $$

$$\frac{\sim\alpha \Rightarrow \delta \quad \sim\beta \Rightarrow \delta}{\sim(\alpha\wedge\beta) \Rightarrow \delta} \ (\sim\wedge \text{left}^{k}) $$

$$\frac{\gamma \Rightarrow \sim\alpha}{\gamma \Rightarrow \sim(\alpha\wedge\beta)} \ (\sim\wedge \text{right1}^{k}) \quad\quad \frac{\gamma \Rightarrow \sim\beta}{\gamma \Rightarrow \sim(\alpha\wedge\beta)} \ (\sim\wedge \text{right2}^{k}) $$

$$\frac{\sim\alpha \Rightarrow \delta}{\sim(\alpha\vee\beta) \Rightarrow \delta} \ (\sim\vee \text{left1}^{k}) \quad\quad \frac{\sim\beta \Rightarrow \delta}{\sim(\alpha\vee\beta) \Rightarrow \delta} \ (\sim\vee \text{left2}^{k}) $$

$$\frac{\gamma \Rightarrow \sim\alpha \quad \gamma \Rightarrow \sim\beta}{\gamma \Rightarrow \sim(\alpha\vee\beta)} \ (\sim\vee \text{right}^{k}). $$

PQL is an extension of a Gentzen-type sequent calculus GLL for lattice logic by Restall and Paoli [23].³ A system GO+, which is the same system as GLL, was introduced by Mönting [17], but it was not called a sequent calculus. A general version of lattice logic, which was called finite sum-product logic, was introduced by Cockett and Seely [7]. Indeed, the {∧, ∨}-fragments of the following logics are the same logic: Lattice logic by Restall and Paoli and by Mönting, finite sum-product logic by Cockett and Seely, the logic of weak sequent calculus by Aoyama and basic logic by Sambin et al.

It is remarked that a Gentzen-type sequent calculus Σπ for the finite sum-product logic by Cockett and Seely [7] is obtained from GLL (or GO+) by replacing the logical inference rules for ∨ and ∧ with the following logical inference rules for $\sum$ and $\prod$: for a non-empty index set I with k∈I,

$$\frac{\{\alpha_{i} \Rightarrow \beta\}_{i \in I}}{{\sum}_{i\in I} \alpha_{i} \Rightarrow \beta} \quad\quad \frac{\alpha \Rightarrow \beta_{k}}{\alpha \Rightarrow {\sum}_{i \in I} \beta_{i}} \quad\quad \frac{\alpha_{k} \Rightarrow \beta}{{\prod}_{i\in I} \alpha_{i} \Rightarrow \beta} \quad\quad \frac{\{\alpha \Rightarrow \beta_{i}\}_{i \in I}}{\alpha \Rightarrow {\prod}_{i \in I} \beta_{i}} $$

where $\sum$ and $\prod$ are regarded as generalizations of ∨ and ∧, respectively.

A Gentzen-type sequent calculus called here LL for lattice logic (or finite sum-product logic) can be defined as follows.

Definition 37

(LL [17, 23]) LL is the ∼-free part of PQL.

The following theorem is known [23].

Theorem 38

(Cut-elimination for LL [23]) The rule (cut ^k ) is admissible in cut-free LL.

Prior to proceed discussion on PQL, we remark that some Gentzen-type sequent calculi for some extensions of LL by adding the following negation inference rules were studied in [23]:

$$\frac{\Gamma \Rightarrow \Delta, \alpha}{\sim\alpha, \Gamma \Rightarrow \Delta} \quad\quad \frac{\alpha, \Gamma \Rightarrow \Delta}{\Gamma \Rightarrow \Delta, \sim\alpha} $$

with one of the following sequent restrictions. Let Γ ⇒ Δ be a sequent. Then, the sequent restrictions are presented as follows:

• 1. Γ ∪ Δ contains exactly two formulas and Δ contains at most one formula,

• 2. Γ ∪ Δ contains exactly two formulas,

• 3. Γ ∪ Δ contains at most two formulas and Δ contains at most one formula,

• 4. Γ ∪ Δ contains at most two formulas.

These restrictions respectively imply distributionless minimal logic, the logic of involutive lattices, distributionless intuitionistic logic, and the logic of orthocomplemented lattices [17]. We also remark that these logics are different from the paraconsistent quantum logic, since ∼(p ∧ q) ⇒∼ p∨ ∼q where p and q are distinct propositional variables is not provable in such a cut-free system, but provable in cut-free PQL.

We can obtain the following theorem.

Theorem 39

(Equivalence between PQL ₄ and PQL) For any sets Γ and Δ of formulas, PQL ₄ ⊢ Γ ⇒ Δ iff PQL ⊢ Γ^∧ ⇒ Δ^∨.

Note that the ∼-free fragment of PQL is also logically equivalent to BL and AL.

We can show the following cut-elimination theorem by simple induction on proofs, i.e., we do not need to use the standard double induction on grade and rank.

Theorem 40

(Cut-elimination for PQL) The rule (cut ^k ) is admissible in cut-free PQL.

Proof

Consider the following proof P such that there is no occurrence of (cut^k) in the subproofs P ₁ and P ₂ of P:

$$\frac{\gamma \overset{\vdots}{\Rightarrow} \overset{P_{1}}{\alpha} \quad \alpha \overset{\vdots}{\Rightarrow} \overset{P_{2}}{\delta}} {\gamma \Rightarrow \delta} (\text{cut}^{k}). $$

Then, it is sufficient to show that (cut^k) in P can be eliminated. This can straightforwardly be proved by induction on the height of P. We distinguish the cases according to the last inferences of P ₁ and P ₂. We show only the following case.

The last inferences of P ₁ and P ₂ are (∼∨right^k) and (∼∨left1^k), respectively.

In this case, we obtain the following proof:

$$\frac{\gamma \overset{\vdots}{\Rightarrow \sim} \alpha \quad \sim \overset{\vdots}{\alpha \Rightarrow} \delta}{\gamma \Rightarrow \delta}(\text{cut}^{k})\ $$

where (cut^k) in this proof can be eliminated by induction hypothesis. □

By using Theorem 40, we can obtain a simple alternative proof of the decidability of the paraconsistent quantum logic.

Theorem 41

(Decidability for PQL) PQL, i.e., the paraconsistent quantum logic, is decidable.

Proof

Suppose that a sequent S is given. Then, we can consider a cut-free bottom-up proof search tree P of S in PQL by Theorem 40. Since PQL has the subformula-like property which is obtained from Theorem 40, P is constructed only from some subformulas or negated-subformulas of some formulas in S. Moreover, there is no occurrence of the contraction rule (in the sense of Gentzen’s LK) in P because PQL has no such rule. Thus, P has no infinite branch or infinite path, and hence P is regarded as a finite tree by Köng’s lemma. Thus, we can decide if P is a proof of S in PQL or not. Of course, the number of the cut-free bottom-up proof search trees for S is finite. Therefore PQL is decidable. □

5 Sequent Calculi for First-Order Paraconsistent Quantum Logic

Gentzen-type sequent calculi for first-order paraconsistent quantum logic can be considered by straightforwardly extending PQL₁, PQL₂, PQL₃, PQL₄ and PQL. In what follows, we only consider a first-order extension FPQL of the simplest system PQL.

Formulas of the first-order paraconsistent quantum logic are obtained from free variables, bound variables, functions, predicates, ∧, ∨, ∼, ∀ (any) and ∃ (exists). The numbers of free and bound variables are assumed to be countable, and the numbers of functions and predicates are also assumed to be countable. It is also assumed that there is at least one predicate. A 0-ary function is an individual constant, and a 0-ary predicate is a propositional variable. Small letters p, q, r,... are used to denote atomic formulas, and Greek lower-case letters α, β,... are used to denote formulas. A sequent of the first-order paraconsistent quantum logic is the same expression as that of PQL.

A Gentzen-type sequent calculus FPQL for the first-order paraconsistent quantum logic is defined below.

Definition 42

(FPQL) FPQL is obtained from PQL by replacing a propositional variable in the initial sequents with an atomic formula, and adding the logical inference rules of the form:

$$\frac{\alpha(t) \Rightarrow \delta}{\forall x \alpha(x) \Rightarrow \delta} \ (\forall \text{left}) \quad\quad \frac{\gamma \Rightarrow \alpha(a)}{\gamma \Rightarrow \forall x \alpha(x)} \ (\forall \text{right}) $$

$$\frac{\alpha(a) \Rightarrow \delta}{\exists x \alpha(x) \Rightarrow \delta} \ (\exists \text{left}) \quad\quad \frac{\gamma \Rightarrow \alpha(t)}{\gamma \Rightarrow \exists x \alpha(x)}\ (\exists \text{right}) $$

$$\frac{\sim \alpha(a) \Rightarrow \delta}{\sim \forall x \alpha(x) \Rightarrow \delta} \ (\sim\forall \text{left}) \quad\quad \frac{\gamma \Rightarrow \sim \alpha(t)}{\gamma \Rightarrow \sim\forall x \alpha(x)} \ (\sim\forall \text{right}) $$

$$\frac{\sim \alpha(t) \Rightarrow \delta}{\sim\exists x \alpha(x) \Rightarrow \delta} \ (\sim\exists \text{left}) \quad\quad \frac{\gamma \Rightarrow \sim \alpha(a)}{\gamma \Rightarrow \sim\exists x \alpha(x)} \ (\sim\exists \text{right}) $$

where a is a free variable which must not occur in the lower sequents of (∀right), (∃left), (∼∀left) and (∼∃right), and t is an arbitrary term.

We have the following theorem.

Theorem 43

(Cut-elimination for FPQL) The rule (cut ^k) is admissible in cut-free FPQL.

Proof

Straightforward extension of the proof of Theorem 40. □

We can prove the decidability of FPQL by using the method by Mey [16] for a first-order logic without contraction rules. First-order substructural logics without contraction rules are known to be decidable. FPQL is also regarded as such a logic. We thus give a sketch of the proof.

Theorem 44

(Decidability for FPQL) FPQL is decidable.

Proof

(Sketch). In the following discussion, we assume Theorem 43, i.e., we consider cut-free proofs in FPQL. Before to show the decision procedure, we introduce some notions.

We introduce a finite number of special variables called term variables. The terms appearing in a bottom-up cut-free proof search tree are replaced by these term variables. The tree obtained from the original bottom-up cut-free proof search tree by this replacement is called here cut-free quasi-proof, and the corresponding bottom-up cut-free proof search is called here cut-free quasi-proof search. Such a cut-free quasi-proof does not necessarily correspond to a cut-free proof, but it has the possibility of transforming to a cut-free proof by a terminable unification algorithm.

We can show the following fact. For any given sequent S, the number of cut-free quasi-proofs of S is finite. Indeed, the number of cut-free quasi-proofs is computable by the total number of free variables, individual constants, logical symbols, quantifiers, predicate symbols and function symbols appearing in S.

Thus, we can decide if a given sequent S is provable or not, in the following procedure. (1) in order to obtain a finite set of cut-free quasi-proofs of S, we perform cut-free quasi-proof search. (2) by using a terminable unification algorithm, we find a cut-free proof of S from the obtained finite set of cut-free quasi-proofs of S. (3) if a cut-free proof is found in (2), then S is provable, otherwise it is not provable. □