Linearizing Intuitionistic Implication

(Appeared in ACM Symposium on Logic in Computer Science 1991)

Patrick Lincoln^{∗}  Andre Scedrov^{†}  Natarajan Shankar^{‡}

June 19, 1991

Abstract

An embedding of the implicational propositional intuitionistic logic (iil) into the nonmodal fragment of intuitionistic linear logic (imall) is given. The embedding preserves cut-free proofs in a proof system that is a variant of iil. The embedding is efficient and provides an alternative proof of the pspace-hardness of imall. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in iil proofs.

1 Overview

Linear logic, invented by Girard [Gir87], is a refinement of classical and intuitionistic logic that provides an intrinsic and natural accounting of resources. In Girard’s words [Gir87], “linear logic is a logic behind logic.” He provides a conservative translation from intuitionistic logic into linear logic that is compositional on subformulas and subproofs. In Girard’s translation, intuitionistic implication A ⇒ B becomes !A −∘B , where ! is a modality indicating unlimited availability of a resource, and −∘ is linear implication. In the propositions-as-type interpretation, linear implication is seen as the type of functions that use their argument exactly once. Girard’s embedding in fact covers the full spectrum of the propositions-as-types paradigm: the level of formulas, the level of proofs, and the level of proof reduction (cut-elimination steps). Furthermore, this embedding extends naturally to first-order and second-order logic [Gir87].

The possibility of a dramatic improvement over Girard’s embedding is raised by a recent result in [LMSS90], establishing the pspace-completeness of the so-called multiplicative additive fragment mall, i.e., propositional linear logic without the modality ! or its dual ? . Statman [Sta79] has shown that propositional intuitionistic logic, indeed, even its purely implicational fragment, is pspace-complete. Hence a natural question arises whether (beyond an immediate Turing reduction) there exists another “logical” embedding of intuitionistic logic into linear logic, that does not rely on the modalities.

Let us be realistic. One cannot hope to have such an embedding which would be too “logical”, because on the one hand, first-order multiplicative additive linear logic is pspace-complete (this follows from the results in [LMSS90] by using methods similar to [KW84]). On the other hand, first-order intuitionistic logic is undecidable (this is an immediate corollary of the negative interpretation of classical logic in intuitionistic logic and the undecidability of classical first-order logic, both of which may be found, for example, in [Kle52]). Therefore it is impossible to have a desired embedding for first-order quantifiers.

Another, more subtle, obstruction to obtaining a very “logical” embedding is the discrepancy in complexity on the level of cut-elimination (normalization). Already for the purely implicational fragment of propositional intuitionistic logic, cut-elimination is hyperexponential (the equivalent fact about normalization in the simple typed lambda calculus is usually one of the first exercises in a graduate course on the subject). In contrast, cut-elimination for mall is known to be much lower, at most exponential. In fact, this is true not just in the propositional case, but also for first-order and for second-order mall. The required bounds may be extracted from the Small Normalization Theorem in [Gir87] and are also explicitly computed in [LS90].

∗Lincoln@CS.Stanford.EDU Department of Computer Science, Stanford University, Stanford, CA 94305, and the Computer Science Laboratory, SRI International, Menlo Park, CA 94025. Supported by AT&T Bell Laboratories Doctoral Scholarship, and SRI internal funding.

†Andre@CIS.Upenn.EDU Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395. Partially supported by NSF Grant CCR-87-05596, by ONR Grant NOOO14-88-K-0635 and by the 1987 Young Faculty Award from the Natural Sciences Association of the University of Pennsylvania. Work begun while on sabbatical leave at the Computer Science Department and Center for the Study of Language and Information, Stanford University.

‡Shankar@CSL.SRI.COM Computer Science Laboratory, SRI International, Menlo Park, CA 94025. Supported by SRI internal funding.

These results still leave open the possibility of a syntactic translation of propositional intuitionistic logic into mall so that such a translation does preserve cut-free proofs of a certain normal form. In this paper we construct such a translation. Our translation is an instance of what Girard terms an “asymmetrical interpretation,” that is, positive occurrences of formulas are translated differently from negative occurrences [GLT89]. It can therefore only be viewed as a translation on cut-free proofs, unlike Girard’s symmetric translation of intuitionistic logic into linear logic.

We only consider propositional systems of intuitionistic and linear logic. We use the following notations that are common to both the intuitionistic and linear formalisms:

l_{i}, p_{i}, q_{i}, r_{i}  Propositional literals
A, B, C  Arbitrary formulas
Σ, Γ  Arbitrary multisets of formulas
Γ ⊢ A  Sequent with antecedent Γ

and consequent A

We entirely omit the linear negation operation of mall. Note that a sequent is represented in terms of two multisets, not sets, of formulas. When we speak of a formula in a sequent, we are really referring to an occurrence of the formula. A reduction is the process of applying a rule to a sequent matching the conclusion of the rule in order to generate the corresponding premises. The principal formula of the rule is then said to be reduced by the reduction. The occurrence of an instance of a rule in a proof is said to be an inference. The proper subformulas of a principal formula of a rule that appear in the premises of the rule are called the side formulas.

The main result of this paper is an efficient embedding of the implicational fragment of propositional intuitionistic logic ( iil) in the intuitionistic fragment of multiplicative-additive linear logic (imall). We provide a transformation of an iil sequent σ to an imall sequent ρ so that imall proves ρ exactly when iil proves σ. The sequents σ and ρ are then said to be equiprovable. The system iil is given by a fairly standard sequent formulation of the intuitionistic implicational logic shown in Figure 4. These rules are similar to those of Kleene’s G3. The target system, imall, is shown in Figure 9. Note that the rules for negation, P, and the constant 0 are absent. Since the presentation is in terms of two sided sequents, cut-elimination for imall holds despite these omissions. Cut-elimination is of course a crucial tool in many of our proofs.

The main distinction between iil and imall is in their treatment of the structural rules. iil has an explicit rule of contraction and the rule of weakening is implicitly built into the I rule. Furthermore, the principal formula of an L ⊃ rule is copied into the premise sequents of each iil rule. imall, on the other hand, has neither contraction nor weakening, and expressly forbids the copying of the principal formula of any rule into a premise. What imall does allow is the sharing of the non-principal formulas between the two premises of an additive inference rule. The cut rule and the contraction rule of iil can be shown to be eliminable. In order to further bridge the gap between these two systems, it is important to establish control over the use of structural rules in iil proofs so that any copying of the principal formulas into the premises is made inessential. Consider the iil proof of the sequent l ⊃ r, (p ⊃ q) ⊃ l, (q ⊃ r) ⊃ q ⊢ r, where Σ denotes l ⊃ r, (p ⊃ q) ⊃ l, (q ⊃ r) ⊃ q given in Figure 1.

One clear difficulty in translating that proof into imall is that the multiset Σ appears in every sequent in the proof. In imall, a formula can appear as the principal formula of at most one inference along any branch of the proof. In the above proof, the copying of the principal formula of an inference into the premises seems essential. The formulas (p ⊃ q) ⊃ l and l ⊃ r appear twice as principal formulas, and in both cases, these duplicate occurrences are along the same branch of the proof. We can deal with the duplicate use of l ⊃ r by rearranging the above proof as in Figure 2.

The next step is to deal with the copying of the formula (p ⊃ q) ⊃ l. For this purpose, we modify the L ⊃ rule of IIL to the following two rules:

\begin{matrix}\underline{Γ ⊢ p Γ, B ⊢ C} & L ⊃ 1 \\ Γ, (p ⊃ B) ⊢ C \end{matrix}

\begin{matrix}\underline{Γ, (B ⊃ C) ⊢ (A ⊃ B) Γ, C ⊢ D} & L ⊃ 2 \\ Γ, ((A ⊃ B) ⊃ C) ⊢ D \end{matrix}

We call the resulting system iil*. The advantage of iil* is that there is no copying.^{1} An antecedent principal formula of the form (A ⊃ B) ⊃ C is replaced

1Grigori Mints directed our attention to iil*. He observes that iil* provides a direct proof-theoretic explanation for the membership in pspace of the decision problem for propositional intuitionistic logic. Cut-free proofs in iil* have a height that is bounded by the number of connectives in the conclusion sequent. An alternating Turing machine can therefore generate and check the proof of a given sequent in a nondeterministic manner within polynomial time.

\underline{\begin{matrix}\overline{Σ, p, q, p ⊢ q} & I \\ \overline{Σ, p, q ⊢ p ⊃ q} & R ⊃ \end{matrix} \overline{Σ, p, q, l ⊢ l}^{I}}_{L ⊃}

Σ, p, q ⊢ l Σ, p, q, r ⊢ r I L ⊃

Σ, p, q ⊢ r
\overline{Σ, p ⊢ q ⊃ r}^{R ⊃} \overline{Σ, p, q ⊢ q}^{I} L ⊃
Σ, p ⊢ q
\overline{Σ ⊢ p ⊃ q}^{R ⊃}

\underline{\overline{Σ, r ⊢ r}^{I} \overline{Σ, l ⊢ l}^{I}}_{L ⊃} Σ, l ⊢ r

L ⊃
Σ ⊢ r

Figure 1: Proof of Σ ⊢ r in iil

\begin{matrix}\overline{Σ, p, q, p ⊢ q} & I \\ \overline{Σ, p, q ⊢ p ⊃ q} & R ⊃ \end{matrix} \underline{\overline{Σ, p, q, l ⊢ l}^{I} \overline{Σ, p, q, l, r ⊢ r}^{I}}_{L ⊃} ; Σ, p, q, l ⊢ r L ⊃
Σ, p, q ⊢ r
\overline{Σ, p ⊢ q ⊃ r}^{R ⊃} \overline{Σ, p, q ⊢ q}^{I} L ⊃

Σ, p ⊢ q

\overline{Σ ⊢ p ⊃ q}^{R ⊃}

\underline{\overline{Σ, r ⊢ r}^{I} \overline{Σ, l ⊢ l}^{I}} Σ, l ⊢ r
L ⊃
Σ ⊢ r

Figure 2: Modified Proof

by the simpler formula B ⊃ C in one of the premises of the L ⊃ 2 rule. Let A, B, C, and D label the formulas l ⊃ r, r ⊃ q, (q ⊃ r) ⊃ q, and q ⊃ l, respectively. With these new rules, the above proof can be transformed to an iil* proof as in Figure 3:

The cut-elimination theorem holds for iil* as well. The absence of contraction and copying in iil* along with the restriction on weakening make it possible to embed iil* in imall. We defer the discussion of this part of the encoding until Section 3.

In summary, we provide a transformation from iil sequents to imall sequents by transforming iil proofs. Our main result is:

Theorem 1.1 iil can be embedded into imall. The embedding preserves the structure of cut-free proofs in iil*.

iil proofs are transformed by eliminating any use of the cut and contraction rules, by reducing the depth of any formula in the proof to two or less, permuting the order of the rules, and modifying the L ⊃ rule so as to eliminate the need for copying. The resulting iil* proofs can then be embedded in imall.

The main result of this paper addresses the issue of replacing copying and reuse in intuitionistic proofs by sharing. We believe that our results contribute to the understanding of the role of linear logic as an expressive and natural framework for describing the control structure of logic programs. Indeed, the cut-free, implicational fragment of intuitionistic logic provides a reasonable framework for logic programming [MNPS90].

2 Properties of IIL

In this section, we present a series of lemmas about iil that eventually establish the eliminability of contraction, the admissibility of weakening, and the redundancy of copying in iil proofs.

Proposition 2.1 For any sequent Σ ⊢ A appearing in any iil proof of Γ ⊢ B, the multiset Γ is a submultiset of Σ.

This conservation of hypothesis formulas in iil proofs provides the key to the elimination of contraction as shown by Propositions 2.2 and 2.3. The size of a proof is taken to be the number of inferences in it.

\underline{\underline{\overline{A, B, p, q ⊢ q}^{I} \underline{\overline{B, p, q, l ⊢ l}^{I} \overline{B, p, q, l, r ⊢ r}^{I}}_{L ⊃ 1} ; A, B, p, q, l ⊢ r}_{L ⊃ 1} ; A, D, B, p, q ⊢ r ; \overline{A, D, B, p ⊢ q ⊃ r}^{R ⊃} \overline{A, D, p, q ⊢ q}^{I}} _{L ⊃ 2}

A, D, (q ⊃ r) ⊃ q, p ⊢ q

\overline{A, D, (q ⊃ r) ⊃ q ⊢ p ⊃ q}^{R ⊃}

\underline{\overline{A, C, r ⊢ r}^{I} \overline{A, C, l ⊢ l}^{I}} A, C, l ⊢ r
L ⊃ 2

Σ ⊢ r

Figure 3: “Linear” Proof in iil*

\overline{Γ, p_{i} ⊢ p_{i}}^{I}

\begin{matrix}Γ, A ⊢ B \\ \overline{Γ ⊢ (A ⊃ B)} & R ⊃ \end{matrix}

\begin{matrix}\underline{Γ, (A ⊃ B) ⊢ A Γ, (A ⊃ B), B ⊢ C} & L ⊃ \\ Γ, (A ⊃ B) ⊢ C \end{matrix}

\underline{Γ, A, A ⊢ B}_{Contraction}

Γ, A ⊢ B

\begin{matrix}\underline{Γ ⊢ C Γ, C ⊢ B} & Cut \\ Γ ⊢ B \end{matrix}

Figure 4: Rules for iil

Proposition 2.2 Given a proof of Γ, A, A ⊢ B of size n in iil, we can produce a proof of Γ, A ⊢ B of size n in iil.

Proposition 2.3 Given a proof of Γ ⊢ A of size n in iil, we can construct a proof of Γ ⊢ A in iil of size no greater than n that does not employ the contraction rule.

Proposition 2.4 If there is a proof of Γ ⊢ A in iil then there is a proof of Γ ⊢ A in iil that does not employ the cut rule.

(See the proof for G3 in [Kle52].)

Proposition 2.5 Any proof of Γ ⊢ A in iil can be transformed into a proof of Γ ⊢ A in iil that does not employ the contraction or cut rules.

Proposition 2.6 Given a proof of Γ ⊢ B of size n in iil, we can produce a proof of Γ, A ⊢ B of size n in iil.

\overline{Γ, p_{i} ⊢ p_{i}}^{I}

\begin{matrix}Γ, A ⊢ B \\ \overline{Γ ⊢ (A ⊃ B)} & R ⊃ \end{matrix}

\begin{matrix}\underline{Γ ⊢ p_{i} Γ, B ⊢ C} & L ⊃ 1 \\ Γ, (p_{i} ⊃ B) ⊢ C \end{matrix}

\begin{matrix}\underline{Γ, (B ⊃ C) ⊢ (A ⊃ B) Γ, C ⊢ D} & L ⊃ 2 \\ Γ, ((A ⊃ B) ⊃ C) ⊢ D \end{matrix}

Figure 5: Rules for iil*

Proposition 2.7 Given a proof of Γ, A ⊃ B, B ⊢ C of size n in iil, we can find a proof of Γ, B ⊢ C of size less than or equal to n in iil.

Proposition 2.8 For all iil formulas A, B, C the sequent (A ⊃ B) ⊃ C ⊢ B ⊃ C is provable in iil.

Proposition 2.9 Given an iil proof of Γ, (A ⊃ B) ⊃ C, B ⊃ C, A ⊢ D of size n, we can construct an iil proof of Γ, B ⊃ C, A ⊢ D of size no more than n.

We now introduce an interesting refinement of iil called iil*, and prove that cut-free, contraction-free iil proofs are easily transformed to proofs in iil*. The proof rules for iil* are given in Figure 5. Similar logics have been studied by others [Vor58, Pli65, Hud89, Dyc91].

Note that the identity rule is only applicable to atomic propositions, and that weakening is only allowed at the leaves of a proof, i.e., at an application of identity. Most important, however, is the property that the principal formula is not duplicated in the premises of any of the rules in iil*.

Proposition 2.10 Given a proof of Γ ⊢ B of size n in iil*, we can produce a proof of Γ, A ⊢ B of size n in iil*.

Lemma 2.11 Given a proof of Γ ⊢ A in iil*, a proof of Γ ⊢ A can be constructed in iil.

Proof. By induction on iil* proofs using Propositions 2.10 and 2.9.

The other direction of the equivalence of iil and iil* is somewhat more complicated. We adapt an argument due to Dyckhoff [Dyc91] to achieve this result.

Consider an L ⊃ inference in an iil proof with a principal antecedent formula of the form p ⊃ A. Let Γ ⊢ C be the conclusion sequent of the inference. The inference is said to be backward if p does not occur in Γ. A forward proof is one with no backward inferences. These names are chosen to be reminiscent of forward and backward chaining.

Lemma 2.12 Any cut-free, contraction-free iil proof Π of size n can be transformed to a cut-free, contraction-free forward proof Θ of size no more than n with the same conclusion as Π.

Proof. The proof is by induction on the size of the cut-free, contraction-free proof Π.

If the final inference in Π is not a backward inference, then we have the result immediately by induction.

If the final step is a backward inference in Π, then we use the induction hypothesis to eliminate the backward inferences in the subproofs of the premises. This transforms the proof Π to the form below, where the only backward inference is the final one.

\begin{matrix}\underline{\begin{matrix}Θ_{1} & Θ_{2} \\ ⋮ & ⋮ \\ Γ, p ⊃ A ⊢ p & Γ, p ⊃ A, A ⊢ C \end{matrix}} & L ⊃ \\ Γ, p ⊃ A ⊢ C \end{matrix}

The premise Γ, p ⊃ A ⊢ p cannot be an axiom since p does not occur in Γ. The final inference in the proof Θ_{1} of Γ, p ⊃ A ⊢ p must therefore be an L ⊃ inference whose principal formula is either of the form (D ⊃ E) ⊃ F or of the form q ⊃ B where q occurs in Γ. In either case, these inferences can be permuted below the final inference in Π, as in Figure 6.

In Figure 6 Θ′_{2} is obtained from Θ_{2} by Proposition 2.6 but has the same size as Θ_{2}. The backward inference with the subproofs Θ_{12} and Θ′_{2} is smaller than Π and we can therefore employ the induction hypothesis to eliminate the backward inference from it. The resulting proof is therefore free of backward inferences and has size no larger than Π.

The other possibility is that the principal formula is of the form q ⊃ B where q occurs in Γ. In this case the inferences permute similarly, and the resulting proof may be seen to be forward by induction, and the fact that q occurs in Γ.

Lemma 2.13 Given a proof of Γ ⊢ C in iil, a proof of Γ ⊢ C can be constructed in iil*.

Proof. By Lemma 2.12, we can restrict our attention to forward proofs. We proceed by induction on weight(σ) for a sequent σ, as defined in Figure 7.

It is easy to show by induction on the structure of A that if 0 < c < d, then 0 < m(A, c) < m(A, d).

If the given iil proof of Γ ⊢ C is an axiom, then the proof is also an iil* proof.

If the final inference in the given iil proof is R ⊃ applied to a conclusion of the form Γ ⊢ A ⊃ B to generate the premise Γ, A ⊢ B, then this premise is of smaller weight. We can therefore apply the induction hypothesis to the premise to get an iil* proof of Γ, A ⊢ B from which the iil* proof of Γ ⊢ A ⊃ B can be completed by the R ⊃ rule of iil*.

If the final inference in the given iil rule is L ⊃ applied to a principal formula of the form p ⊃ B where Γ has the form Σ, p ⊃ B, then p must occur in Σ. The nontrivial premise is then Σ, p ⊃ B, B ⊢ C. By Proposition 2.7, the sequent Σ, B ⊢ C must also have an iil proof and since it is of smaller weight than Σ, p ⊃ B ⊢ C, the induction hypothesis can be applied to it yielding an iil* proof of Σ, B ⊢ C. Since p occurs in Σ, the sequent Σ ⊢ p is an iil* axiom. The required iil* proof of Σ, p ⊃ B ⊢ C can be constructed using the L ⊃ 1 rule with the premises Σ, B ⊢ C and Σ ⊢ p.

If the final inference in the given iil proof is L ⊃ applied to a principal formula of the form (D ⊃ E) ⊃ F, where Γ is of the form Σ, (D ⊃ E) ⊃ F, then we have iil proofs for the two premises Σ, (D ⊃ E) ⊃ F ⊢ D ⊃ E and Σ, (D ⊃ E) ⊃ F, F ⊢ C. Proposition 2.7 applied to the second premise yields an iil proof of Σ, F ⊢ C to which the induction hypothesis can be applied yielding an iil* proof of Σ, F ⊢ C. Since in iil we can prove D, (E ⊃ F) ⊢ (D ⊃ E) ⊃ F and D, (D ⊃ E) ⊢ E, we can use the cut rule twice with the sequent Σ, (D ⊃ E) ⊃ F ⊢ D ⊃ E to get an iil

\begin{matrix}\underline{\begin{matrix}Θ_{11} & Θ_{12} \\ ⋮ & ⋮ \\ Γ, p ⊃ A ⊢ D ⊃ E & Γ, p ⊃ A, F ⊢ p \end{matrix}} & L ⊃ \\ Γ, p ⊃ A ⊢ p \end{matrix}  Θ_{2} ; ⋮ ; Γ, p ⊃ A, A ⊢ C L ⊃

Γ, p ⊃ A ⊢ C

becomes

Θ_{11} ; ⋮ ; Γ, p ⊃ A ⊢ D ⊃ E  \begin{matrix}\underline{Θ_{12} ; ⋮ ; Γ, p ⊃ A, F ⊢ p  Θ′_{2} ; ⋮ ; Γ, p ⊃ A, F, A ⊢ C} & L ⊃ \\ Γ, p ⊃ A, F ⊢ C \end{matrix} L ⊃

Γ, p ⊃ A ⊢ C

Figure 6: Permuting backward inferences

weight(A_{1}, …, A_{n} ⊢ C) = m(A_{1}, 1) + … + m(A_{n}, 1) + m(C, 1)
m(A ⊃ B, d) = m(A, d + 1) + (d ∗ m(B, d)) + 1
m(p, d) = d

Figure 7: Definition of weight

proof of Σ, E ⊃ F, D ⊢ E. The difference in weight between this last sequent and the original conclusion sequent Σ, (D ⊃ E) ⊃ F ⊢ C is given in Figure 8.

So the induction hypothesis yields an iil* proof of Σ, E ⊃ F, D ⊢ E which by R ⊃ yields an iil* proof of Σ, E ⊃ F ⊢ D ⊃ E. This last sequent with Σ, F ⊢ C yield an iil* proof of Σ, (D ⊃ E) ⊃ F ⊢ C by the L ⊃ 2 rule of iil*.

The lack of contraction in iil* makes this formulation of the sequent rules for implicational intuitionistic propositional logic amenable to encoding into imall.

3 iil* to imall

An intuitionistic linear logic sequent is composed of two multisets of linear logic formulas separated by a ⊢. We assume a set of propositional atoms p_{i} to be given. The rules of imall are such that every derivable sequent contains no more than one formula in its consequent multiset. Figure 9 gives the inference rules for the intuitionistic linear sequent calculus, with the slight restriction that the 0 rule is omitted. This omission does not pose problems for cut elimination.

We now give a pair of translation functions which transform any iil* formula into an imall formula.

The simultaneous definitions of [ ]^{+} and [ ]^{−} given in Figure 10 can be seen to be well defined by induction on the size of the formulas.

For any iil* sequent Γ ⊢ C we define

θ(Γ ⊢ C) =^{Δ} [Γ]^{−}, k ⊢ [C]^{+}

Here [Γ]^{−} stands for the result of the application of [ ]^{−} to each element of Γ. Note that the “key” k is present in the context of the encoding of a sequent. We have chosen the notations [ ]^{+} and [ ]^{−} to suggest the interpretation of positive and negative polarity of occurrences.

Lemma 3.1 For any iil* Γ and C, the sequent [Γ]^{−}, k, ⊥ ⊢ [C]^{+} is provable in imall.

This lemma is proved by induction on the right-hand depth of C. If C = p_{i} is a proposition, we can construct an imall proof as in Figure 11.

In the case that C = (A ⊃ B) is an implication, we know that B is of smaller depth than C, and we can construct the proof as in Figure 12. weight(Σ, (D ⊃ E) ⊃ F ⊢ C) − weight(Σ, E ⊃ F, D ⊢ E)

= m((D ⊃ E) ⊃ F, 1) + m(C, 1) − m(E ⊃ F, 1) − m(D, 1) − m(E, 1)
= m(D, 3) + 2m(E, 2) + 2 + m(F, 1) + 1 + m(C, 1) − m(E, 2) − m(F, 1) − 1 − m(D, 1) − m(E, 1)
> 0

Figure 8: Example calculation of weight

I  \overline{A ⊢ A}  \frac{Σ ⊢ A  A, Γ ⊢ B}{Σ, Γ ⊢ B} Cut

⊗L  \frac{Σ, A, B ⊢ C}{Σ, (A ⊗ B) ⊢ C}  \frac{Σ ⊢ A  Γ ⊢ B}{Σ, Γ ⊢ (A ⊗ B)}  ⊗R

−∘L  \frac{Σ ⊢ A  Γ, B ⊢ C}{Σ, Γ, (A−∘B) ⊢ C}  \frac{Σ, A ⊢ B}{Σ ⊢ (A−∘B)}  −∘R

⊕L \frac{Σ, A ⊢ C  Σ, B ⊢ C}{Σ, (A ⊕ B) ⊢ C}  \frac{Σ ⊢ A  Σ ⊢ B}{Σ ⊢ (A&B)}  &R

&L1  \frac{Σ, A ⊢ C}{Σ, (A&B) ⊢ C}  \frac{Σ ⊢ A}{Σ ⊢ (A ⊕ B)}  ⊕R1

&L2  \frac{Σ, B ⊢ C}{Σ, (A&B) ⊢ C}  \frac{Σ ⊢ B}{Σ ⊢ (A ⊕ B)}  ⊕R2

⊥L  \overline{⊥ ⊢}  \frac{Σ ⊢}{Σ ⊢ ⊥}  ⊥R

1L  \frac{Σ ⊢ A}{Σ, 1 ⊢ A}  \overline{⊢ 1}  1R
\overline{Σ ⊢ ⊤}  ⊤R

Figure 9: Rules for imall

\begin{matrix}[A ⊃ B]^{+} & =^{Δ} & k ⊗ ([A]^{−}−∘(k−∘[B]^{+})) \\ [p_{i}]^{+} & =^{Δ} & k ⊗ ((p_{i} ⊕ ⊥) ⊗ ⊤) \\ [p_{i}]^{−} & =^{Δ} & p_{i} \\ [p_{i} ⊃ A]^{−} & =^{Δ} & k−∘(((k−∘[p_{i}]^{+})−∘(k ⊗ ⊥)) ⊕ (k ⊗ [A]^{−})) \\ [(A ⊃ B) ⊃ C]^{−} & =^{Δ} & k−∘((([(B ⊃ C)]^{−}−∘(k−∘[(A ⊃ B)]^{+}))−∘(k ⊗ ⊥)) ⊕ (k ⊗ [C]^{−})) \end{matrix}

Figure 10: Definition of translation

\underline{\underline{\begin{matrix}\overline{⊥ ⊢} & ⊥L \\ \overline{⊥ ⊢ ⊥} & ⊥R \\ \overline{⊥ ⊢ p_{i} ⊕ ⊥} & ⊕R \end{matrix} \overline{[Γ]^{−} ⊢ ⊤}^{⊤R}}_{⊗R} ; [Γ]^{−}, ⊥ ⊢ (p_{i} ⊕ ⊥) ⊗ ⊤ \overline{k ⊢ k}^{I}}_{⊗R} ; [Γ]^{−}, k, ⊥ ⊢ k ⊗ ((p_{i} ⊕ ⊥) ⊗ ⊤)

Figure 11: Case one of Lemma 3.1.

\underline{⋮ ; [Γ]^{−}, [A]^{−}, k, ⊥ ⊢ [B]^{+} ; \overline{[Γ]^{−}, [A]^{−}, ⊥ ⊢ k−∘[B]^{+}}^{−∘R} ; \overline{[Γ]^{−}, ⊥ ⊢ [A]^{−}−∘(k−∘[B]^{+})}^{−∘R} \overline{k ⊢ k}^{I}} _{⊗R}

[Γ]^{−}, k, ⊥ ⊢ k ⊗ ([A]^{−}−∘(k−∘[B]^{+}))

Figure 12: Case two of Lemma 3.1.

Lemma 3.2 For any iil* multiset Γ and proposition p_{i}, the sequent [Γ]^{−}, [p_{i}]^{−}, k ⊢ [p_{i}]^{+} is provable in imall.

This lemma is proved by expanding the definition of [p_{i}]^{+}, as seen in Figure 13.

In order to show that the translation is correct and faithful, we need to show that there exists a cut-free proof of Γ ⊢ C in iil* if and only if there is a cut-free proof of θ(Γ ⊢ C) in imall. We demonstrate this in two steps below, after demonstrating how parts of our example iil* sequent are translated into imall.

Consider the sequent Σ′, (p ⊃ q) ⊃ l ⊢ r, where Σ′ abbreviates l ⊃ r, (q ⊃ r) ⊃ q. This sequent has the θ-translation [Σ′]^{−}, [(p ⊃ q) ⊃ l]^{−}, k ⊢ [r]^{+}. By the above definition, [(p ⊃ q) ⊃ l]^{−} = k−∘((([(q ⊃ l)]^{−}−∘(k−∘[(p ⊃ q)]^{+}))−∘(k ⊗ ⊥)) ⊕ (k ⊗ [l]^{−})). In the example iil* proof given in Figure 3, the proof of this sequent ends in an application of the L ⊃ 2 rule.

The intuitive structure of the proof in Figure 14 is as follows. The leftmost application of I and the bottommost application of −∘L correspond to “unlocking” the formula of interest. The unlocked formula corresponding to (p ⊃ q) ⊃ l has ⊕ as its main connective. The proof tree therefore forks, and after a simple application of ⊗L, the rightmost branch can be seen to be the translation of the rightmost branch of the iil* proof.

The left main branch of the proof progresses by applying the −∘L rule. Here there is a choice to be made in the way we split the context Σ′ among the branches of the proof. However, because of the form of our translation, we can without loss of generality choose to keep the entire context on the left branch. By lemma 3.1 k, ⊥ ⊢ [r]^{+}, the upper right branch, is provable. And finally, we see that after two applications of R ⊃ we are left with the translation of the right hand branch of the iil* proof.

In fact, the encoding is such that there are essentially no choices to be made in the proof of the imall translation that cannot be made in the proof of an iil* formula. For example, once a formula is unlocked with the “key” k, no other formula may be unlocked until the unlocked formula is reduced completely, at which point it provides another key k. We argue that there is a proof of an iil* formula if and only if there is a proof its translation in imall.

Lemma 3.3 If there is a cut-free proof of Σ ⊢ C in iil*, then there is a cut-free proof of θ(Σ ⊢ C) in imall.

This lemma is proved by induction on the height of proof in iil*.

We now introduce two propositions which simplify the other direction of the main theorem. These propositions are mild alterations of lemmas used to establish the pspace-completeness of imall [LMSS90]. The first proposition is only used to prove the second, and

\underline{\underline{\begin{matrix}\overline{p_{i} ⊢ p_{i}} & I \\ \overline{p_{i} ⊢ p_{i} ⊕ ⊥} & ⊕R \end{matrix} \overline{[Γ]^{−} ⊢ ⊤}^{⊤R}}_{⊗R} ; [Γ]^{−}, p_{i}, ⊢ (p_{i} ⊕ ⊥) ⊗ ⊤ \overline{k ⊢ k}^{I}}_{⊗R} ; [Γ]^{−}, p_{i}, k ⊢ k ⊗ ((p_{i} ⊕ ⊥) ⊗ ⊤)

Figure 13: Proof of Proposition 3.2.

\begin{matrix}\underline{⋮ ; Σ′, (q ⊃ l) ⊢ (p ⊃ q)  ⋮ ; Σ′, l ⊢ r} & L ⊃ 2 \\ Σ′, ((p ⊃ q) ⊃ l) ⊢ r \end{matrix}

⇓

k ⊢ k I

\underline{⋮ ; [Σ′]^{−}, [(q ⊃ l)]^{−}, k ⊢ [(p ⊃ q)]^{+} ; \overline{[Σ′]^{−}, [(q ⊃ l)]^{−} ⊢ k−∘[(p ⊃ q)]^{+}}^{−∘R} ; \overline{[Σ′]^{−} ⊢ ([(q ⊃ l)]^{−}−∘(k−∘[(p ⊃ q)]^{+}))}^{−∘R} ⋮ ; k, ⊥ ⊢ [r]^{+} ; \overline{k ⊗ ⊥ ⊢ [r]^{+}}^{⊗L}}_{−∘L}

[Σ′]^{−}, ([(q ⊃ l)]^{−}−∘(k−∘[(p ⊃ q)]^{+}))−∘(k ⊗ ⊥) ⊢ [r]^{+}

⋮ [Σ′]^{−}, k, [l]^{−} ⊢ [r]^{+}_{\overline{[Σ′]^{−}, k ⊗ [l]^{−} ⊢ [r]^{+}}^{⊗L}}

⊕L

[Σ′]^{−}, (([(q ⊃ l)]^{−}−∘(k−∘[(p ⊃ q)]^{+}))−∘(k ⊗ ⊥)) ⊕ (k ⊗ [l]^{−}) ⊢ [r]^{+} −∘L

[Σ′]^{−}, k, k−∘((([(q ⊃ l)]^{−}−∘(k−∘[(p ⊃ q)]^{+}))−∘(k ⊗ ⊥)) ⊕ (k ⊗ [l]^{−})) ⊢ [r]^{+}

Figure 14: iil* and imall proofs of example.

the second proposition formally states that in a cutfree imall proof no lock can be opened before there is a key available at top level.

Proposition 3.4 For any atomic proposition p, and sequence Δ not containing the constant 1 or the constant 0 the sequent Δ ⊢ p is not provable in imall unless Δ is identically p, or contains a subformula of the form p&A, A&p, p ⊕ A, A ⊕ p, or A−∘p for some formula A.

Note that the clause about the constant 0 is not actually needed in our formulation of imall. However, this property could be of interest outside the scope of this paper, and thus we state it exactly for full intuitionistic two-sided multiplicative additive linear logic.

Proposition 3.5 For any formula F which is a subformula of an encoding [ ]^{−} or [ ]^{+} and which is not identically k, F must be reduced below any other formula in any imall proof of [Γ]^{−}, F ⊢ [C]^{+} or [Γ]^{−} ⊢ F.

Lemma 3.6 If there is a proof of θ(Γ ⊢ C) in imall, then there is a proof of Γ ⊢ C in iil*.

Proof. (Sketch) To prove this lemma, we perform cut-elimination on the given imall proof, and then observe that the resulting proof must be of a very special form. In fact, an iil* proof can be directly read from any such proof. The action of the “locks and keys” encoded by the positive and negative occurrences of k in the imall translations forces any cut-free imall proof of a sequent to have a very specific form. Proposition 3.5 states this formally. It is exactly this sort of control over the shape of a proof which one can encode in linear logic sequents, but which is impossible to encode in intuitionistic and classical logic. The proof of this lemma proceeds by induction on the size of cut-free imall proof.

Given a cut-free imall proof of a sequent θ(Γ ⊢ C), we see which imall proof rule was applied last. Because the proof is cut-free, the last rule cannot be cut. Investigating the forms of imall formulas which can appear in a θ-translation, we see that the last proof rule applied must be either −∘L, ⊗R, or identity. However, even identity cannot apply, since k always appears on the left in any θ-translation, and k never appears at top level on the right in such a translation. Thus there are only two cases to consider, left implication, and right tensor. For example, consider the case when ⊗R is the last rule applied in a proof, and the principal formula is of the form k ⊗ ([A]^{−}−∘(k−∘[B]^{+})). The imall proof must then have the form:

\underline{⋮ ; [Γ]^{−}, [A]^{−}, k ⊢ [B]^{+} ; \overline{[Γ]^{−}, [A]^{−} ⊢ k−∘[B]^{+}}^{−∘R} ; \overline{[Γ]^{−} ⊢ [A]^{−}−∘(k−∘[B]^{+})}^{−∘R} \overline{k ⊢ k}^{I}} _{⊗R}

[Γ]^{−}, k ⊢ k ⊗ ([A]^{−}−∘(k−∘[B]^{+}))

We know that the imall proof takes this form, since if any part of [Γ]^{−} were to be included in the right premise, imall identity would not apply, and in fact there could be no proof of that branch of the proof, as stated in proposition 3.4. Also, since there is no k at top level in the left premise of the ⊗R rule, reducing any formulas in [Γ]^{−} could not lead to a proof by proposition 3.5. This reasoning applies twice, leaving us with the proof displayed above. This proof can be simulated in iil* by applying the R ⊃ rule, and the hypothesis, itself a θ-translation, can be simulated by induction. The other case of ⊗R and the two cases of −∘L are similar.

4 Efficiency of Transformation

For any iil sequent ρ we have provided an equiprovable imall sequent θ(ρ). This encoding into imall could be exponential in the size of ρ, but if ρ is of depth two or less, then θ(ρ) is linear in the size of ρ. Below we give a depth-reduction procedure which takes polynomial time and which produces a depth two term Ξ(ρ) which is only linearly larger than ρ. The transformation θ(Ξ(ρ)) therefore provides an argument for the pspace-hardness of the decision problem for imall. The argument for membership of this problem in pspace is immediate and appears in [LMSS90]. The transformation from iil* to imall is efficient in another stronger manner. It preserves the structure of iil* proofs. The imall translation of an iil* proof is linear in the size of the given iil* proof. Note that our transformation from iil to iil* does not necessarily preserve the structure of cut-free proofs in iil due to the permutations that are needed to achieve make copying redundant. Neither of our transformations preserves the structure of proofs with cut.

4.1 Depth Reduction in IIL

An iil formula of depth one is either an atom p or has the form (p_{i} ⊃ p_{j}). A formula of depth two is one of the form (p_{i} ⊃ (p_{j} ⊃ p_{k})), or the form ((p_{i} ⊃ p_{j}) ⊃ p_{k}). Given a sequent Γ ⊢ D, we define Ξ(Γ ⊢ D) to be the result of repeatedly applying any of the the set of transformations given in Figure 15 until none of them apply.

These transformations each reduce the depth of implications, at the expense of building a new implication (which is also shallower than the original). Thus this sequence of reductions always terminates. Notice that the only kinds of formulas left after the Ξ transformation are of the form: p_{i}, p_{i} ⊃ p_{j}, p_{i} ⊃ (p_{j} ⊃ p_{k}), or (p_{i} ⊃ p_{j}) ⊃ p_{k}, where p_{i}, p_{j}, and p_{k} are atomic propositions. Although all the formulas appearing are very small, there may be many more of them. This technique goes back to [Waj38], see also [Min90].

The following lemma is stated, without proof, for iil. The analogous lemma holds for iil* as well.

Lemma 4.1 For any iil sequent σ, the iil sequent Ξ(σ) contains formulas of depth at most two, and Ξ(σ) is provable exactly when σ is provable.

Depth reduction, Ξ, defined above takes place in polynomial time and the size of Ξ(σ) is linear in the size of σ since, in the worst case, we introduce a constant number of new formulas for each subformula of σ.

5 Conclusion

Linear logic has already found a number of fruitful applications in computing. One reason for this is that linear logic is a well-motivated refinement of both classical and intuitionistic logic. It admits a Curry-Howard isomorphism that provides a mechanism for typing programs in such a way that intensional aspects of the program are made explicit in its type. The sequent formulation of linear logic admits a cutelimination theorem. An interesting aspect of cut elimination is that it is possible in linear logic to encode constraints on the form of a cut-free proof in the conclusion sequent. Linear logic is therefore expressive in a manner that intuitionistic and classical logic are not. Our classification of the complexity and decidability of fragments of linear logic highlights some of this expressiveness [LMSS90].

Our embedding of the implicational fragment of propositional intuitionistic logic in the imall fragment of linear logic provides an alternative proof for the pspace-hardness of imall. More importantly, it provides insight into the use and elimination of the structural rules from iil through the embedding of iil into iil*. The system iil* is an interesting optimization of intuitionistic logic that could be useful

Γ, (A ⊃ B) ⊃ (C ⊃ D) ⊢ Z ⇒ x ⊃ (C ⊃ D), Γ, (A ⊃ B) ⊃ x ⊢ Z
Γ, p_{i} ⊃ ((A ⊃ B) ⊃ C) ⊢ Z ⇒ (A ⊃ B) ⊃ x, Γ, p_{i} ⊃ (x ⊃ C) ⊢ Z
Γ, p_{i} ⊃ (A ⊃ (B ⊃ C)) ⊢ Z ⇒ x ⊃ (B ⊃ C), Γ, p_{i} ⊃ (A ⊃ x) ⊢ Z
Γ, ((A ⊃ B) ⊃ C) ⊃ p_{i} ⊢ Z ⇒ x ⊃ (A ⊃ B), Γ, (x ⊃ C) ⊃ p_{i} ⊢ Z
Γ, (A ⊃ (B ⊃ C)) ⊃ p_{i} ⊢ Z ⇒ (B ⊃ C) ⊃ x, Γ, (A ⊃ x) ⊃ p_{i} ⊢ Z
Γ ⊢ (A ⊃ B) ⊃ (C ⊃ D) ⇒ (C ⊃ D) ⊃ x, Γ ⊢ (A ⊃ B) ⊃ x
Γ ⊢ p_{i} ⊃ (A ⊃ (B ⊃ C)) ⇒ (B ⊃ C) ⊃ x, Γ ⊢ p_{i} ⊃ (A ⊃ x)
Γ ⊢ p_{i} ⊃ ((A ⊃ B) ⊃ C)) ⇒ x ⊃ (A ⊃ B), Γ ⊢ p_{i} ⊃ (x ⊃ C)
Γ ⊢ (A ⊃ (B ⊃ C)) ⊃ p_{i} ⇒ x ⊃ (B ⊃ C), Γ ⊢ (A ⊃ x) ⊃ p_{i}
Γ ⊢ ((A ⊃ B) ⊃ C)) ⊃ p_{i} ⇒ (A ⊃ B) ⊃ x, Γ ⊢ (x ⊃ C) ⊃ p_{i}

Figure 15: Definition of Ξ

in theorem proving and logic programming applications [Mil90].

A number of questions remain open. An extension of our techniques to all intuitionistic propositional connectives should be investigated. On the other hand, it would be interesting to know whether there is an embedding of intuitionistic implication in imall that preserves the structure of all cut-free proofs. We would also like to know the complexity of cut-elimination for the system iil* with a cut rule. It is worth examining what transformations such as depth reduction mean at the level of proof terms given by the Curry-Howard isomorphism, and whether there are some useful optimizations in the evaluation of proof terms arising from such a study.

We would like to thank Jean-Yves Girard, Grigori Mints, and John Mitchell for very stimulating discussions. We are also grateful to Grigori Mints for help in investigating the literature.