A modal view of linear logic

Simone Martini Andrea Masini Dipartimento di Informatica Università di Pisa Corso Italia, 40 I-56125 Pisa Italy

              {martini,masini}@di.unipi.it

Abstract

We present a sequent calculus for the modal logic S4, and, building on some relevant features of this system (the absence of contraction rules and the confinement of weakenings into axioms and modal rules) we show how S4 can be easily translated into full propositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities (exponentials) only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

1 Introduction

From a proof-theoretic point of view, linear logic [4] can be considered as an attempt to control the bookkeeping of formulas in a classical (or intuitionistic) proof. Contractions and weakenings are excluded from the armamentarium of the logic, giving rise to a deeply symmetrical system, where all propositional connectives double in two versions — the “multiplicatives” and the “additives”. The expressive power of this logic, however, was thought to be too limited, and for the purpose of recovering, via a suitable translation of formulas and proofs [4, pag. 78], the full power of intuitionistic logic (and thus of classical logic, via the double negation translation), the modalities (or exponentials) ! and ? were introduced. The rules for modalities exactly mimic the structural rules (weakening and contraction) of classical or intuitionistic logic. These rules, which appear much more extrinsic than those for the other connectives, destroy the symmetry of the calculus.

It is rather well known, however, that there are contraction-free sequent systems for classical propositional logic, where all weakenings can be “pushed to the leaves”. Ono [11], applying a translation by Grishin [5], exploits this fact to obtain an interpretation of classical propositional logic into propositional linear logic without modalities (also in [13, Ch. 4]).

We extend the Grishin-Ono translation to the modal logic S4, in a such a way that a linear exponential is only needed to translate a modality of S4 modality. To this aim, we use a contraction and cut-free sequent calculus for S4 which contains as a subsystem the contraction-free calculus of Grishin. This shows that, from a proof-theoretical point of view, exponentials behave exactly as S4 modalities.

2 A contraction-free sequent calculus for S4

The sequent calculus for the modal logic S4 which will be the main object of study of this paper is best presented as a one-sided system (à la Tait), thus avoiding, especially in the cut-elimination theorem, many cases to be considered. Formulas are built out of literals, that is atoms (ranged over by p), together with their negations, ¬p; compound formulas are obtained with the connectives: ∧ and ∨ (binary); □ and ◇ (unary). The negation of a compound formula A is defined by ¬¬A = A and the following De Morgan rules: ¬(A ∧ B) = ¬A ∨ ¬B, ¬□A = ◇¬A.

Definition 2.1 The sequent calculus GS4 for the propositional modal logic S4 is given by the following axioms and rules. Γ and Δ are sequences of formulas; A and B are generic formulas; p is a generic atom.

⊢ Γ, p, ¬p

\frac{⊢ Γ, A ⊢ Γ, ¬A}{⊢ Γ} cut

\frac{⊢ Γ′, A, B, Γ′′}{⊢ Γ′, B, A, Γ′′} X

\frac{⊢ Γ, A  ⊢ Γ, B}{⊢ Γ, A ∧ B} ∧  \frac{⊢ Γ, A, B}{⊢ Γ, A ∨ B} ∨

\frac{⊢ ◇Γ, A}{⊢ ◇Γ, □A, Δ} □  \frac{⊢ Γ, A, ◇A}{⊢ Γ, ◇A} ◇

Sequent calculi for modal logics have been studied by several authors, e.g. Curry [1], Ohnishi and Matsumoto [10] and Zeman [14]. System GS4 (without a cut-rule), in particular, has been proposed by Kanger [6] who, according to Dopp [2], proves the equivalence with S4, but do not show an explicit cut-elimination procedure.

The subsystem of GS4 obtained by forgetting the two modal rules (system G, say) appears, with a different cut rule, in [1, Chap. 5, C, formulation IK], where sufficient conditions for contraction admissibility are also given. System G is used by Grishin and Ono for their translation of classical logic into linear logic. The crucial property of G is the invertibility of its rules (note, especially, rule ∨, due to Ketonen [7]), which allows to prove in a straightforward way admissibility of contractions and cut-elimination. The full GS4 does not enjoy a full inversion lemma (see A.1, below), and its cut-elimination is not as straightforward as that for G.

In the modal rules of GS4, note the additional weakening list (Δ) in the conclusion of □. The “context constraints”, in fact, in the premise of rule □ forbid to push arbitrary weakenings to the axioms.

Rule ◇, finally, presents in the premise an occurrence of the main formula of the conclusion, thus hiding an implicit contraction. The following remark shows that this implicit contraction is essential for the completeness of the calculus.

Remark The sequent ⊢ □◇(□p ∨ □◇¬p) does not have any cut-free proof in the system where rule ◇ is substituted with the rule

\frac{⊢ Γ, A}{⊢ Γ, ◇A} ◇′

Any such proof, in fact, by the last rule property of cut-free proofs must terminate in the following way

⊢ □p, □◇¬p ; ∨ ; ⊢ □p ∨ □◇¬p

◇′

⊢ ◇(□p ∨ □◇¬p)

□

⊢ □◇(□p ∨ □◇¬p)

and now the tree cannot be completed, since it is easily checked that two formulas with main connective □ can be in the same sequent only if one of the two has been introduced as part of a weakening list (either in an axiom or in a □ rule). Hence there is no cut-free proof of ⊢ □◇(□p ∨ □◇¬p) in the system with the simpler rule ◇′. The following is, instead, a proof in GS4 (applications of the exchange rule, X, are not shown):

⊢ p, ¬p, ◇¬p, ◇(□p ∨ □◇¬p)
◇
⊢ p, ◇¬p, ◇(□p ∨ □◇¬p)
□
⊢ □p, ◇¬p, ◇(□p ∨ □◇¬p), □◇¬p
∨, ◇
⊢ ◇(□p ∨ □◇¬p), ◇¬p
□
⊢ ◇(□p ∨ □◇¬p), □◇¬p, □p
∨
⊢ ◇(□p ∨ □◇¬p), □p ∨ □◇¬p
◇
⊢ ◇(□p ∨ □◇¬p)
□
⊢ □◇(□p ∨ □◇¬p)

Note that all but the last application of ◇ could have been substituted with applications of ◇′ (with obvious modifications to the weakening lists). Observe, finally, that □◇(□p ∨ □◇¬p) is the modal translation (e.g. [12]) of ¬¬(p ∨ ¬p), a formula whose intuitionistic proof requires an essential contraction.

The equivalence of GS4 (with cut rule) and S4 is an easy exercise. A direct proof of cut-elimination for GS4, instead, is not trivial and cannot be obtained from the analogous result for systems with explicit contraction and weakening, due to the peculiar form of some of the rules. A detailed proof, which we could not locate in the available literature, is in the appendix.

3 From S4 to linear logic

The reader acquainted with linear logic will have already observed the notable similarity of GS4 rules with some linear rules. This gives an almost immediate way of translating S4 into the full propositional linear logic, introduced as a one-sided sequent system in the following definition. As usual, formulas are built out of constants (1, ⊤, 0, ⊥) and atoms (ranged over by p), together with their duals, p^{⊥}. The dual, A^{⊥}, of a compound formula A is defined by A^{⊥}^{⊥} = A and the following De Morgan rules: 1^{⊥} = ⊥, ⊤^{⊥} = 0, (A ⊗ B)^{⊥} = A^{⊥} � B^{⊥}, (A � B)^{⊥} = A^{⊥} ⊕ B^{⊥}.

Definition 3.1 The Linear Logic Sequent Calculus, LL, is given by the following axioms and rules.

⊢ p, p^{⊥}  ⊢ 1  ⊢ Γ, ⊤

\frac{⊢ Γ}{⊢ Γ, ⊥} ⊥

\frac{⊢ Δ, A ⊢ Γ, A^{⊥}}{⊢ Δ, Γ} cut

\frac{⊢ Δ, A, B, Δ′}{⊢ Δ, B, A, Δ′} X

\frac{⊢ Γ, A  ⊢ Δ, B}{⊢ Γ, Δ, A ⊗ B} ⊗  \frac{⊢ Γ, A, B}{⊢ Γ, A � B} �
\frac{⊢ Γ, A  ⊢ Γ, B}{⊢ Γ, A � B} �  \frac{⊢ Γ, A}{⊢ Γ, A ⊕ B} ⊕_{1}  \frac{⊢ Γ, B}{⊢ Γ, A ⊕ B} ⊕_{2}
\frac{⊢ Γ, A}{⊢ Γ,?A} ?  \frac{⊢?Γ, A}{⊢?Γ,!A} !
\frac{⊢ Γ}{⊢ Γ,?A} W?  \frac{⊢ Γ,?A,?A}{⊢ Γ,?A} C?

The system MALL of Multiplicative-Additive Linear Logic is obtained from LL by removing the four exponential rules.

Definition 3.2 Formulas of the language of GS4 are translated into LL formulas as follows (p stands for an atom):

\begin{matrix}(p)^{+} = p & (¬p)^{+} = p^{⊥} ⊗ ⊤ \\ (A ∧ B)^{+} = A^{+} � B^{+} & (A ∨ B)^{+} = A^{+} � B^{+} \\ (□A)^{+} = (!A^{+}) ⊗ ⊤ & (◇A)^{+} =?A^{+} \end{matrix}

The previous definition extends trivially to sequences of formulas.

Remark For non modal formulas this is essentially the Grishin-Ono translation. The translation of compound propositional formulas is forced by the shape of the rules of G, while the main ingredient of the atom case, in charge of validating the implicit weakening in the axioms, is the p^{⊥} ⊗ ⊤, allowing to “split” the sequent in an axiom ⊢ p, p^{⊥} and in an axiom for ⊤. Here the same device is replicated in the translation of □A, for taking into account the additional weakening list of the rule □. Several variations are possible on the atom case, for instance we could set (p)^{+} = p � B for a generic formula B, or translate a literal q as q ⊗ ⊤, independently from the fact that it is positive or negative. The proof of 3.6 may be trivially adapted to these variations.

Definition 3.3 The forgetful interpretation of LL into GS4 is defined as follows.

ν(⊥) = ν(0) = p ∧ ¬p
ν(⊤) = ν(1) = p ∨ ¬p
ν(A ⊗ B) = ν(A � B) = ν(A) ∧ ν(B)
ν(A ⊕ B) = ν(A � B) = ν(A) ∨ ν(B)
ν(!A) = □ν(A)
ν(?A) = ◇ν(A)
ν(p) = p
ν(p^{⊥}) = ¬p

Proposition 3.4 For any modal formula A, ⊢_{GS4} A ≡ ν(A^{+}).

Proof A trivial induction on A.

Proposition 3.5 If ⊢_{LL}Γ, then ⊢_{GS4} ν(Γ).

Proof Let π be a cut free LL proof of ⊢ Γ. Observe that under the interpretation ν, any LL axiom becomes a provable formula in GS4, and any LL logical rule becomes an admissible rule of GS4. Therefore, we obtain a proof ν(π) in GS4 of ⊢ ν(Γ).

The main theorem of this paper shows that any cut-free proof of a sequent ⊢_{GS4} Γ can be effectively and faithfully transformed into a cut-free proof of the sequent ⊢_{LL}Γ^{+}.

Theorem 3.6

⊢_{GS4} Γ ⟺ ⊢_{LL}Γ^{+}

Proof (⇒) Let π be a cut free proof of ⊢_{GS4} Γ. We show how to construct a cut free proof π′ of ⊢_{LL}Γ^{+}. The proof is by induction on the length of π and by cases on the last rule, r, of π.

1. π is an axiom: ⊢ Γ, p, ¬p. Then π′ is the following LL proof:

\frac{⊢ p, p^{⊥} ⊢ ⊤, Γ^{+}}{⊢ p, p^{⊥} ⊗ ⊤, Γ^{+}} ⊗ .

2. r is an exchange rule. Trivial.

3. r is a logical rule with main formula A, having as principal connective ∧ or ∨. Then A^{+} has � or �, respectively, as principal connective. The proof π′ is obtained by induction and the rule of the involved connective.

4. r is □. By induction, we have an LL proof of ⊢?Γ^{+}, A^{+}. The required proof π′ is

⊢?Γ^{+}, A^{+} ; ! ; ⊢?Γ^{+},!A^{+} ⊢ ⊤, Δ^{+}

⊗

⊢?Γ^{+},!A^{+} ⊗ ⊤, Δ^{+}

5. r is ◇. The induction hypothesis gives the LL proof ⊢ Γ^{+}, A^{+},?A^{+}.

Proof π′ is

⊢ Γ^{+}, A^{+},?A^{+}

?

⊢ Γ^{+},?A^{+},?A^{+}

C?

⊢ Γ^{+},?A^{+}

(⇐) By proposition 3.5 ⊢_{GS4} ν(Γ^{+}), and thus ⊢_{GS4} Γ, by proposition 3.4 and simple propositional manipulations.

Corollary 3.7 (Grishin, Ono)

⊢_{G} Γ ⟺ ⊢_{MALL}Γ^{+}

Observe that the translation is an “asymmetrical” interpretation, that is the translation of ∧ is not the linear dual of the translation of ∨. As a consequence, while all logical rules of GS4 are mapped into the corresponding logical rules of LL, this is not the case for the cut rule. Therefore, although the translation of a cut is a correct inference (that is from ⊢_{LL}Γ^{+}, A^{+} and ⊢_{LL}Γ^{+}, (¬A)^{+} it does indeed follow that ⊢_{LL}Γ^{+}), this inference is not obtained by a cut in LL, requiring first the cut-elimination procedure in GS4.

4 Complexity issues

The decision problem for LL is known to be undecidable [8], the culprits being the exponentials (the decision problem for the fragment MALL is PSPACE-complete). On the other hand, all the logics that have been (faithfully) interpreted into LL (intuitionistic [4], implicational intuitionistic [9], classical [11], S4) have decidable decision problems. It is thus interesting to see whether these translations naturally define classes of linear formulas for which the decision problem is as difficult as that for the starting logic.

Lincoln, Scedrov and Shankar [9] showed how intuitionistic implicational logic could be interpreted into the intuitionistic fragment of MALL (IMALL) without using modalities; since IMALL is PSPACE-complete, they obtained an exact complexity correspondence between the two logics.

We address here the complexity of the decision problem for the two classes of linear formulas arising from the Grishin-Ono translation of classical logic and our translation of S4. Let us first recall that the problem whether ⊢_{G} A is derivable in classical propositional logic is a coNP-complete problem, while the problem whether ⊢_{GS4} A is derivable in S4 is PSPACE-complete [3].

Definition 4.1

• The class of Classical Linear formulas is the least set CL of propositional linear formulas such that:

p, p^{⊥} ⊗ ⊤ ∈ CL;

if A, B ∈ CL then A � B, A � B ∈ CL.

• The class of Modal Linear formulas is the least set ML of propositional linear formulas such that:

CL ⊆ ML;
if A ∈ ML then !A ⊗ ⊤,?A ∈ ML.

Theorem 4.2 (i) The problem of deciding whether ⊢_{MALL}A, for A ∈ CL, is coNP-complete. (ii) The problem of deciding whether ⊢_{LL}A, for A ∈ ML, is PSPACEcomplete.

Proof We prove (i); (ii) is analogous. Membership of the given problem into coNP is established by reduction to classical propositional provability. Define the following function ξ on CL-formulas.

ξ(p) = p ξ(p^{⊥} ⊗ ⊤) = ¬p
ξ(A � B) = ξ(A) ∧ ξ(B) ξ(A � B) = ξ(A) ∨ ξ(B) .

By theorem 3.7, ⊢_{G} ξ(A) iff ⊢_{MALL}ξ(A)^{+}; observe now that ξ(A)^{+} = A. Completeness is by reduction from classical propositional provability, which is just Corollary 3.7, observing that CL is exactly the image of the ( )^{+} function.

Remark Like for the translation 3.2, several variations are possible in the definition of CL. We can require, for instance, for any atom p, that p ⊗ ⊤, p^{⊥} ⊗ ⊤ ∈ CL. Also in this case, by adopting a modified translation, we obtain the same complexity results.

Acknowledgments

A. Troelstra drew our attention to the Grishin-Ono translation, which we did not know when we started to work on this subject.

A Appendix

We will give here a direct proof first of the admissibility of the contraction rule, and then of the cut-elimination theorem for GS4.

A formula is propositional if its main connective is ∧ or ∨. The degree of a formula, δ(A), is defined in the usual way: δ(A) = 0 if A is a literal; δ(A ∧ B) = δ(A ∨ B) = max{δ(A), δ(B)} + 1; δ(□A) = δ(◇A) = δ(A) + 1. Also the length of a proof π, ℓ(π), is as usual, with the proviso that exchange rules do not increase ℓ(π) (and will not be displayed in proof trees). The cut degree of a proof, d(π), is the maximum degree of the cut formulas in π.

Lemma A.1 (Inversion) Let π be a proof of ⊢ Γ; for each occurrence of a propositional formula A in ⊢ Γ, there is a proof π_{A} of ⊢ Γ, whose last rule has A as principal formula. Moreover, ℓ(π_{A}) ≤ ℓ(π) + 1, and d(π_{A}) = d(π).

proof By induction on the length of π. If π is an axiom, then A cannot be the principal literal, since A is propositional, and hence non-literal. Suppose that A = A_{1} ∧ A_{2} and π is ⊢ Γ, A_{1} ∧ A_{2}, p, ¬p. Then π_{A} is

⊢ Γ, A_{1}, p, ¬p ⊢ Γ, A_{2}, p, ¬p
⊢ ∧
⊢ Γ, A_{1} ∧ A_{2}, p, ¬p

Note that ℓ(π_{A}) = 1. The case for ∨ is analogous. For the inductive step, which does not modify the length of the proof, if the last rule of π has A as principal formula, we are done; otherwise, for each last rule of π, we have several cases depending on the principal connective of A. We give only three cases when A = A_{1} ∧ A_{2}. The first case is when the last rule is a cut with cut formula B. The induction hypothesis gives the two proofs

⊢ Γ, A_{1}, B ⊢ Γ, A_{2}, B ; ⊢ ∧ ; ⊢ Γ, A_{1} ∧ A_{2}, B ⊢ Γ, A_{1}, ¬B ⊢ Γ, A_{2}, ¬B ; ⊢ ∧ ; ⊢ Γ, A_{1} ∧ A_{2}, ¬B

Proof π_{A} is then

⊢ Γ, A_{1}, B ⊢ Γ, A_{1}, ¬B ; cut ; ⊢ Γ, A_{1}  ⊢ Γ, A_{2}, B ⊢ Γ, A_{2}, ¬B ; cut ; ⊢ Γ, A_{2}
⊢ ∧
⊢ Γ, A_{1} ∧ A_{2}

The second case is when the last rule of π is □. Note that, in this case, A must be a weakening formula, namely the proof π has the form

⊢ ◇Γ, B
□
⊢ ◇Γ, □B, A, Δ

Proof π_{A} is then

⊢ ◇Γ, B ; □ ; ⊢ ◇Γ, □B, A_{1}, Δ  ⊢ ◇Γ, B ; □ ; ⊢ ◇Γ, □B, A_{2}, Δ
∧
⊢ Γ, □B, A_{1} ∧ A_{2}, Δ

The last case we consider is when the last rule of π is ◇: simply apply the induction hypothesis to the premise and then reapply rule ◇.

Lemma A.2 Let π be a proof of ⊢ Γ, A, A in GS4. Then there is a proof ϖ of ⊢ Γ, A. Moreover, d(ϖ) = d(π).

proof By induction on δ(A). If A is a literal p or ¬p, then at least one of the two occurrences of A is a weakening formula introduced by an axiom or by a □ rule, since no other rule can introduce an atom. In both cases, ϖ is obtained from π by erasing one of the two occurrences of the literal from all the sequents between the conclusion of π and the rule (or axiom) introducing the literal. Note that ℓ(ϖ) = ℓ(π). If A is a propositional formula, then apply lemma A.1 to the two occurrences of A, then the induction hypothesis, and finally one rule for the principal connective of A. If A is □A′, the constraints on the premise of the □ rule, guarantee that at least one of the two occurrences of A is a weakening formula introduced by an axiom or by a □ rule. The proof ϖ is obtained as in the literal case. If, finally, A is ◇A′, observe that no rule can add such a formula, but an axiom or a □ rule, and in both cases it has to be a weakening formula. The proof ϖ is obtained as in the literal case.

The previous lemma amounts to the following result.

Theorem A.3 The contraction rule

\frac{⊢ Γ, A, A}{⊢ Γ, A} C

is admissible in GS4.

Next result will be the elimination of the cut rule from G; before, however, we need to show that weakening is an admissible rule.

Lemma A.4 Let π be a (cut-free) proof of ⊢ Γ and let B be any formula. Then there is a (cut-free) proof π[B] of ⊢ Γ, B. Moreover, ℓ(π[B]) = ℓ(π) and d(π[B]) = d(π).

proof By trivial induction on ℓ(π).

In the following we will write π ⊢ Γ for “π is a proof with end sequent ⊢ Γ”. Moreover, given π ⊢ Γ and π′ ⊢ Γ′ the proof-tree-like notation

π ⊢ Γ π′ ⊢ Γ′
= justification
⊢ Δ

will stand for “the proof of ⊢ Δ obtained by applying justification to π ⊢ Γ and π′ ⊢ Γ′” (where justification will usually be a previous lemma or a suitable induction hypothesis).

The following lemma is the crucial ingredient of the cut-elimination theorem for GS4. Its proof is a non-trivial variant of similar results for different systems. In particular, while the absence of contraction rules dispenses from the need of dealing with multiple occurrences of the same formula (as it is the case with the standard formulation of LK), the failure of a fully-fledged inversion lemma, the shape of the cut-rule (the same context Γ is required in both premises), the presence of an occurrence of the main formula in the premise of the ◇ rule, and the weakening list present in the □ rule, introduce several twists in the case when the “cut-formula” is passive (and modal; see in, the proof, the many sub-cases of case 5.4).

Lemma A.5 (Reduction) Let π ⊢ Γ, A and π′ ⊢ Γ, ¬A with d(π) < d(A) and d(π′) < d(A). Then we can construct a proof ϖ ⊢ Γ with d(ϖ) < d(A).

Proof By cases on the last rule r and r′ of π and π′, respectively, and by induction on ℓ(π) + ℓ(π′). In the following, π_{i} (π′_{i}) will denote the proof of the i-th premise ⊢ Γ_{i} (⊢ Γ′_{i}) of rule r (r′).

1 π is an axiom: ⊢ Γ, p, ¬p. We have three sub-cases.

1.1 A = p. Then π′ ⊢ Γ, ¬p, ¬p; proof ϖ is obtained from π′ by applying

lemma A.2. 1.2 A = ¬p. Analogous to case 1.1. 1.3 A ∈ Γ. We have π ⊢ Γ′, A, p, ¬p; ϖ is the axiom ⊢ Γ′, p, ¬p. 2 π′ is an axiom: dual of case 1. 3 r is an exchange: trivial. 4 r′ is an exchange: trivial. 5 r is a logical rule not introducing A or it is a cut. We have several

sub-cases.

5.1 r is ∧. We have π_{1} ⊢ Γ, B_{1}, A π_{2} ⊢ Γ, B_{2}, A

∧
π ⊢ Γ, B_{1} ∧ B_{2}, A

and π_{1}^{∘} ⊢ Γ, B_{1}, ¬A π_{2}^{∘} ⊢ Γ, B_{2}, ¬A

= Inversion Lemma
π′ ⊢ Γ, B_{1} ∧ B_{2}, ¬A

Observe that ℓ(π_{1}^{∘}) ≤ ℓ(π′) and ℓ(π_{2}^{∘}) ≤ ℓ(π′). The proof ϖ is the following:

π_{1} ⊢ Γ, B_{1}, A π_{1}^{∘} ⊢ Γ, B_{1}, ¬A ; = IH ; ⊢ Γ, B_{1}  π_{2} ⊢ Γ, B_{2}, A π_{2}^{∘} ⊢ Γ, B_{2}, ¬A ; = IH ; ⊢ Γ, B_{2}
∧
ϖ ⊢ Γ, B_{1} ∧ B_{2}

5.2 r is ∨. Analogous to case 5.1. 5.3 r is ◇. From π′ ⊢ Γ, ◇B, ¬A obtain first, by Lemma A.4,

π′[B] ⊢ Γ, B, ◇B, ¬A. The proof ϖ is

π_{1} ⊢ Γ, B, ◇B, A π′[B] ⊢ Γ, B, ◇B, ¬A
= IH
⊢ Γ, B, ◇B
◇
ϖ ⊢ Γ, ◇B

5.4 r is □. We have two sub-cases depending on the presence of A in the

weakening list. 5.4.1 An occurrence of the formula A is introduced by weakening. Proof

ϖ is simply obtained by π by omitting that occurrence of A from the weakening list.

5.4.2 The situation is the following, where A must be of the form ◇A_{1}:

π_{1} ⊢ ◇Γ, B, ◇A_{1}

□
π ⊢ ◇Γ, □B, ◇A_{1}, Δ

and π′ ⊢ ◇Γ, □B, ¬◇A_{1}, Δ. We proceed by cases on the last rule, r′, of π′.

5.4.2.1 r′ is propositional (and hence does not introduce A). Apply case

6.1 or 6.2. 5.4.2.2 r′ is ◇ (and hence does not introduce A). Apply case 6.3. 5.4.2.3 r′ is □. We have two more sub-cases (remember that, since

A = □A_{1} for some formula A_{1}, we have ¬A = ¬◇A_{1} = □¬A_{1}). 5.4.2.3.1 r′ introduces ¬◇A_{1}. We have, for some splitting Δ = ◇Δ_{1}, Δ_{2}

π′_{1} ⊢ ◇Γ, ¬A_{1}, ◇Δ_{1}

□
π′ ⊢ ◇Γ, ¬◇A_{1}, ◇Δ_{1}, Δ_{2}

Apply Lemma A.4 to π_{1} ⊢ ◇Γ, B, ◇A_{1} to obtain the proof π_{1}[◇Δ_{1}] ⊢ ◇Γ, B, ◇A_{1}, ◇Δ_{1}; proof ϖ is

π_{1}[◇Δ_{1}] ⊢ ◇Γ, B, ◇A_{1}, ◇Δ_{1}  π′_{1} ⊢ ◇Γ, ¬A_{1}, ◇Δ_{1} ; □ ; ⊢ ◇Γ, ¬◇A_{1}, B, ◇Δ_{1}
= IH
⊢ ◇Γ, B, ◇Δ_{1}
□
ϖ ⊢ ◇Γ, □B, ◇Δ_{1}, Δ_{2}

5.4.2.3.2 r′ does not introduce ¬◇A_{1}. Necessarily, then, the cut-formula ¬◇A_{1} is a weakening formula and ϖ is obtained from π′ by not introducing ¬◇A_{1}.

5.4.2.4 r′ is a cut. Apply case 6.5. 5.5 r is a cut. The situation is the following:

π_{1} ⊢ Γ, A, C π_{2} ⊢ Γ, A, ¬C

\overline{cut}

π ⊢ Γ, A

and π′ ⊢ Γ, ¬A. Proof ϖ is:

π_{1} ⊢ Γ, A, C π′[C] ⊢ Γ, ¬A, C ; = IH ; ⊢ Γ, C  π_{2} ⊢ Γ, A, ¬C π′[C] ⊢ Γ, ¬A, C ; = IH ; ⊢ Γ, ¬C

\overline{cut}

ϖ ⊢ Γ 6 r′ is a logical rule not introducing the cut formula ¬A or it is a cut.

Dual of case 5 (with all its sub-cases). Observe that the sub-cases 6.1, 6.2, 6.3 and 6.5 (used in the reduction of case 5) will be handled directly, thus avoiding loops in the reduction process.

7 Both r and r′ introduce the cut formula. We have four subcases depending on the principal connective of the cut formula A.

7.1 r is ∧ and r′ is ∨. Proof ϖ is

π_{1}[¬A_{2}] ⊢ Γ, A_{1}, ¬A_{2} π′_{1} ⊢ Γ, ¬A_{1}, ¬A_{2} ; \overline{cut} ; ⊢ Γ, ¬A_{2} π_{2} ⊢ Γ, A_{2}

\overline{cut}

ϖ ⊢ Γ

7.2 r is ∨ and r′ is ∧. Dual of case 7.1.

7.3 r is ◇ and r′ is □. We have:

π_{1} ⊢ ◇Γ_{1}, A, ◇A, Γ_{2}
◇
π ⊢ ◇Γ_{1}, ◇A, Γ_{2}

and

π′_{1} ⊢ ◇Γ_{1}, ¬A
□
π′ ⊢ ◇Γ_{1}, ¬◇A, Γ_{2}

Proof ϖ is

π_{1} ⊢ ◇Γ_{1}, A, ◇A, Γ_{2} π′[A] ⊢ ◇Γ_{1}, A, ¬◇A, Γ_{2} ; = IH ; ⊢ ◇Γ_{1}, A, Γ_{2} π′_{1}[Γ_{2}] ⊢ ◇Γ_{1}, ¬A, Γ_{2}

\overline{cut}

ϖ ⊢ ◇Γ_{1}, Γ_{2}

7.4 r is □ and r′ is ◇. Dual of case 7.3.

The previous lemma establishes in the standard way the cut-elimination theorem.

Theorem A.6 Given any proof of ⊢ Γ, it is possible to construct a cut-free proof of the same sequent.

References

[1] Curry, H.B. Foundations of Mathematical Logic. Dover, New York, 1977^{2}.

[2] Dopp, J., Appendix, in Feys, Modal Logics, Gauthier–Villars, Paris and Nauwelaerts, Louvain, 1965.

[3] Garey, M.R. and D.S. Johnson, Computers and Intractability, W.H. Freeman and Co., San Francisco, 1979.

[4] Girard, J.-Y. Linear Logic. Theo. Comp. Science, 50(187), 1–102

[5] Grishin, V.N. A non-standard logic, and its application to set theory (in Russian), in Isslédovanija po formalizovannym jazykam i néklassičéskim logikam (Studies in formalized languages and nonclassical logics), Nakua, Moscow, 135-171, 1974.

[6] Kanger, S.G., Provability in logic, (Acta Universitatis Stockolmiensis, Stockolm Studies in Philosophy, 1), Stockolm, Almquist & Wiksell, 1957, 47pp.

[7] Ketonen, D. Untersuchungen zum Prädikatenkalkül. Ann. Acad. Sci. Fenn., ser. A I Math., vol. 23(1944), 71 pp.

[8] Lincoln, P., J.C. Mitchell, A. Scedrov and N. Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, vol. 56(1992), 239–311.

[9] Lincoln, P., A. Scedrov and N. Shankar. Linearizing Intuitionistic Implication. In Logic in Computer Science 1991 (LICS 91), Amsterdam, 51–61.

[10] Ohnishi, M. and K. Matsumoto, Gentzen Method in Modal Calculi I, Osaka Math. J., 9(1957), 113–130.

[11] Ono, H., Structural rules and a logical hierarchy, in P.P.Petkov (ed), Mathematical Logic, Plenum Press, New York, London, 95–104, 1990

[12] Prawitz, D. and P.-E. Malmnäs, A survey on some connections between classical, intuitionistic and minimal logic, in Contributions to mathematical logic, Logic Colloquium 1966, H.A. Schmidt, K. Schütte, H.-J. Thiele (Eds.), North-Holland, Amsterdam, 1968; 215–229.

[13] Troelstra, A.S., Lectures in Linear Logic, CSLI Lecture Notes n. 29, Chicago Univ. Press, Chicago, 1991.

[14] Zeman, J.J., Modal Logic. The Lewis modal systems, Clarendon Press, Oxford, 1973.