Decision Problems For Second-Order Linear Logic

Reprint from: Tenth Annual IEEE Symposium on Logic in Computer Science (LICS’95) to be held in San Diego, California, June 26-29 1995

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

Abstract

Abstract. The decision problem is studied for fragments of second-order linear logic without modalities. It is shown that the structural rules of contraction and weakening may be simulated by second-order propositional quantifiers and the multiplicative connectives. Among the consequences are the undecidability of the intuitionistic second-order fragment of propositional multiplicative linear logic and the undecidability of multiplicative linear logic with first-order and second-order quantifiers.

1 Introduction

Much of the expressive power and plasticity of linear logic may be traced to the prohibition of structural rules of Contraction and to some extent Weakening [7, 9, 28, 25, 26]. These rules are reintroduced into linear logic in a controlled fashion by the logical rules for modalities (or: exponentials), which allow, for instance, intuitionistic implication or function type A ⇒ B to be expressed as !A −∘B. Without the use of modalities, however, any reintroduction of the structural rules appears unlikely because of a phenomenon of linearity, namely, a formula occurrence may be the principal formula of an inference rule at most once in a (cut free) proof. This phenomenon still holds in second-order linear logic. It is therefore surprising to discover that Contraction and Weakening can indeed be simulated by the multiplicative connectives using second-order propositional quantification.

Perhaps the most interesting consequences of our simulation of the structural rules concern an intuitionistic version of linear logic, presented by two-sided sequents with one consequent formula. These fragments of intuitionistic linear logic have been applied to several aspects of computer science such as Petri nets [6], polynomial time [11, 8], functional programming [1, 19, 3, 4], and logic programming [13]. We show that even the weakest of these fragments is undecidable in the presence of second-order quantification. Our simulation of the structural rules also applies to the classical or multiple-conclusion framework, which has been studied in the context of logic programming in [23, 24, 21], but our simulation yields undecidability only in the presence of the first-order and second-order quantifiers. Undecidability results in the second-order propositional framework have been subsequently obtained in [15, 16].

While the nature of our results is foundational, we believe that the techniques described here contribute to the understanding of the role of linear logic in describing control structure of second-order logic programs. Furthermore, our result addresses the replacement of the programming language issues ‘copy’ and ‘delete’ by second-order polymorphism.

In referring to linear logic fragments, let m stand for multiplicatives, a for additives, e for exponentials (or: modalities), 1 for first-order quantifiers, 2 for second-order quantifiers, and i for intuitionistic version of linear logic fragments. Thus imll2 denotes the multiplicative fragment of second-order propositional intuitionistic linear logic. Furthermore, let lj2 denote second-order intuitionistic propositional logic and let lk12 denote second-order classical predicate logic. The reader should recall that lk12 is undecidable in the presence of at least one binary predicate variable. The undecidability of lj2 was shown in [22, 5].

Decision problems for propositional (quantifierfree) linear logic were first studied by Lincoln et al. [20], where it was shown that full propositional linear logic is undecidable and that mall is pspacecomplete. The main problems left open in [20] were the np-completeness of mll, the decidability of mell, and the decidability of various fragments of propositional linear logic without exponentials but extended with second-order propositional quantifiers.

The decision problem for mell is still open. The np-completeness of mll has been obtained by Kanovich [14]. Lincoln and Winkler [18] have established that the provability of multiplicative propositional sentences built on constants, not literals, is already np-complete. mall1 with function symbols is nexptime-complete: the hardness has been obtained by Lincoln and Scedrov [17] and the membership, and hence completeness, by Lincoln and Shankar [21]. Here we show the undecidability of imll2, imall2, mll12, and mall12. Subsequently, the undecidability of mall2 has been shown by Lafont [15] and the undecidability of mll2 by Lafont and Scedrov [16]. The undecidability of full second-order propositional linear logic was known: it follows from the undecidability of lj2 by Girard’s translation [7], which involves exponentials. Our translation below provides an alternative argument.

∗lincoln@csl.sri.com Computer Science Laboratory, SRI International, Menlo Park, CA 94025-3493. Work supported under NSF Grant CCR-9224858

†andre@cis.upenn.edu Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395. Partially supported by NSF Grant CCR-94-00907 and by ONR Grant N00014-92-J-1916. Scedrov is an American Mathematical Society Centennial Research Fellow.

‡shankar@csl.sri.com Computer Science Laboratory, SRI International, Menlo Park, CA 94025-3493. Work supported under NSF Grants CCR-9224858 and CCR-9300444

2 Logical framework

Gentzen-style sequent calculus is the formal logical framework throughout the paper. For our purposes it is convenient to consider sequents of the form Γ ⊢ Δ where Γ, Δ are finite multisets of formulas. In intuitionistic versions of sequent calculi one considers only those sequents for which Δ consists of a single formula. Let us refer to such sequents Γ ⊢ A as intuitionistic sequents. Note that in standard presentations of sequent calculi, sequents are often built from sets of formulas, where we use multisets here. For second-order predicate calculus we assume a countably infinite set of individual variables, a nonempty set of arities, and for each arity a countably infinite set of predicate variables and a countably infinite set of predicate atoms of that arity. Atomic formulas (other than constants) are of the form X(x_{1}, …, x_{n}) where x_{1}, …, x_{n} are individual variables and X is a predicate symbol (variable or atom) of arity n. For second-order propositional calculus we assume a countably infinite set of propositional variables (i.e., predicate variables of arity zero) and a countably infinite set of propositional atoms. Atomic formulas are propositional variables or atoms.

The following notational conventions are observed throughout this paper: H denotes atomic formulas other than constants, G and G′ denote predicate or propositional atoms (not variables or constants), X denotes propositional or predicate variables (not atoms or constants), A, B, D, and E denote formulas, and Γ, Δ, Σ, Θ, Ξ denote finite multisets of formulas.

A presentation of inference rules for second-order classical propositional calculus, lk2, is given in Figure 1. In the rules ∀R and ∃L the propositional atom G must be chosen so that it does not occur in the conclusion of the rule application. Predicate calculi also include the analogous first-order versions of the quantifier rules with a similar restriction on first-order ∀R and ∃L. This presentation of lk2 differs somewhat from some of the other expositions (say, in [27]) but it is similar to the presentation in [10]. It is prooftheoretic folklore that the presentations are equivalent in the sense that the set of provable sequents is the same. Similar remarks apply to the intuitionistic calculus as well. In particular, let us consider the presentation of second-order intuitionistic propositional calculus, lj2, in which the formulas are built from propositional variables and the constant T rue by the connectives ∧ and ⇒ and by the universal second-order propositional quantifier ∀. The sequents of lj2 are intuitionistic sequents of such formulas (i.e., exactly one formula appears on the right-hand side.) The inference rules of lj2 are the applicable rules of lk2, see Figure 2. It is proof-theoretic folklore that other intuitionistic connectives and the existential second-order propositional quantifier are definable in this presentation.

A presentation of the inference rules for secondorder linear propositional calculus without modalities, mall2, is given in Figure 4. The English names for the rules given in Figure 4 are identities, tensor, linear implication, plus, with, bottom, one, zero, top, universal, existential, and cut, respectively. ⊗, −∘, and^{⊥} are multiplicative connectives; 1 and ⊥ are multiplicative propositional constants. ⊕ and & are additive connectives; 0 and ⊤ are additive propositional constants. second-order multiplicative linear propositional calculus, mll2, may be seen as that part of mall2 that mentions only multiplicatives and second-order quantifiers. The reader will note that linear negation A^{⊥} may be defined by recursion on the structure of formulas.

The formulas of second-order intuitionistic linear propositional calculus without modalities, imall2, are built from propositional variables and constants 1, ⊤ by the linear connectives and by the universal secondorder propositional quantifier ∀. The sequents considered are intuitionistic sequents of such formulas. second-order intuitionistic multiplicative linear propositional calculus, imll2, is that part of imall2 that mentions only multiplicatives and the universal quantifier. The inference rules of imll2 are given in Figure 3. The inference rules of imall2 are the applicable rules of mall2 given in Figure 4, i.e., the rules of imll2 given in Figure 3 together with the following rules from Figure 4: ⊕L, & L (all with Δ consisting of a single formula), and ⊕R & R, and ⊤R (all with Δ empty).

The cut elimination property holds for all calculi considered here (see [7, 10] for cut elimination in second-order calculi). In particular, if a sequent is provable, then it is provable without using the Cut rule.

3 Representing intuitionistic logic

We first define the imll2 formulas C and W as follows:

C =^{Δ} ∀X.X−∘(X ⊗ X)

W =^{Δ} ∀X.X−∘1

The idea is that C represents contraction and W represents weakening. We represent lj2 in imll2 using the formulas C and W.

In order to simplify our constructions, we first develop some derived rules of inference in imll2 for sequents containing the formulas C, C, C, W in the lefthand side. Let us begin by demonstrating that C actually embodies the contraction rule.

Lemma 3.1 If C, C, Σ, B, B ⊢ A is provable in imll2, then C, C, Σ, B ⊢ A is provable in imll2.

Proof. The following proof fragment shows that contraction on the left-hand side of a sequent is a derived rule of inference, “Contract”, for sequents with at least two copies of C. That is, reading this proof fragment from the bottom up, if one has one copy of the formula B in a sequent, then one can effectively copy it and have two copies of the formula B. The

I+  \overline{H ⊢ H}  \overline{¬H ⊢ ¬H}  I-
IL  \overline{H, ¬H ⊢}  \overline{⊢ H, ¬H}  IR

CL  \frac{Γ, A, A ⊢ Δ}{Γ, A ⊢ Δ}  \frac{Γ ⊢ A, A, Δ}{Γ ⊢ A, Δ}  CR

WL  \frac{Γ ⊢ Δ}{Γ, A ⊢ Δ}  \frac{Γ ⊢ Δ}{Γ ⊢ A, Δ}  WR

∧L  \frac{Γ, A, B ⊢ Δ}{Γ, (A ∧ B) ⊢ Δ}  \frac{Σ ⊢ A, Θ  Γ ⊢ B, Δ}{Σ, Γ ⊢ (A ∧ B), Θ, Δ} ∧R

⇒L \frac{Σ ⊢ A, Θ  Γ, B ⊢ Δ}{Σ, Γ, (A ⇒ B) ⊢ Θ, Δ}  \frac{Γ, A ⊢ B, Δ}{Γ ⊢ (A ⇒ B), Δ}  ⇒R
FL  \overline{F alse ⊢}  \overline{⊢ T rue}  TR

∀L  \frac{Γ, A[B/X] ⊢ Δ}{Γ, ∀X.A ⊢ Δ}  \frac{Γ ⊢ A[G/X], Δ}{Γ ⊢ ∀X.A, Δ}  ∀R

∃L  \frac{Γ, A[G/X] ⊢ Δ}{Γ, ∃X.A ⊢ Δ}  \frac{Γ ⊢ A[B/X], Δ}{Γ ⊢ ∃X.A, Δ}  ∃R

\frac{Σ ⊢ A, Θ  A, Γ ⊢ Δ}{Σ, Γ ⊢ Θ, Δ} Cut

Figure 1: Rules for lk2

\overline{H ⊢ H}  I

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

\frac{Γ ⊢ B}{Γ, A ⊢ B}  W
\overline{⊢ T rue}  T

∧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[B/X] ⊢ C}{Γ, ∀X.A ⊢ C}  \frac{Γ ⊢ A[G/X]}{Γ ⊢ ∀X.A}  ∀R

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

Figure 2: Rules for lj2

\overline{H ⊢ H} I

⊗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

1L  \frac{Γ ⊢ A}{Γ, 1 ⊢ A}  \overline{⊢ 1}  1R

∀L  \frac{Γ, A[B/X] ⊢ C}{Γ, ∀X.A ⊢ C}  \frac{Γ ⊢ A[G/X]}{Γ ⊢ ∀X.A}  ∀R

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

Figure 3: Rules for imll2

sequent A ⊢ A is provable in imll2 for any formula A.

\underline{\begin{matrix}\underline{\overline{B ⊢ B} \overline{C ⊢ C}} & ⊗R \\ C, B ⊢ B ⊗ C \end{matrix} \begin{matrix}C, C, Σ, B, B ⊢ A \\ \overline{B, C, B ⊗ C, Σ ⊢ A} & ⊗L \\ \overline{B ⊗ C, B ⊗ C, Σ ⊢ A} & ⊗L \\ \overline{(B ⊗ C) ⊗ (B ⊗ C), Σ ⊢ A} & ⊗L \end{matrix}}_{−∘L}

\underline{(B ⊗ C)−∘(B ⊗ C) ⊗ (B ⊗ C), C, Σ, B ⊢ A}_{∀L}

C, C, Σ, B ⊢ A

In the presence of contraction, W embodies the weakening rule.

Lemma 3.2 If C, C, W, Σ ⊢ A is provable in imll2, then C, C, W, Σ, B ⊢ A is provable in imll2.

Proof. The rule of inference “Weaken” can be derived as follows:

\underline{\overline{B ⊢ B} \begin{matrix}C, C, W, Σ ⊢ A \\ \overline{1, W, C, C, Σ ⊢ A} & 1L \end{matrix}}_{−∘L}

\underline{B−∘1, W, C, C, Σ, B ⊢ A}_{∀L}
\underline{C, C, W, W, Σ, B ⊢ A}_{Contract}

C, C, W, Σ, B ⊢ A

Weaken

Let us proceed to the main result of this section. The representation of lj2 in imll2 for any lj2 multiset of formulas Σ and formula A is given by:

[T rue] =^{Δ} 1
[H] =^{Δ} H
[A ⇒ B] =^{Δ} [A]−∘[B]
[A ∧ B] =^{Δ} [A] ⊗ [B]
[∀X.A] =^{Δ} ∀X.[A]
[A_{1}, …, A_{n}] =^{Δ} [A_{1}], …, [A_{n}]
[Σ ⊢ A] =^{Δ} C, C, C, W, [Σ] ⊢ [A]

Lemma 3.3 If Σ ⊢ A in lj2, then [Σ ⊢ A] in imll2.

Proof. This is proved by induction on the size of the proof. We will construct an imll2 proof from a given lj2 proof.

The lj2 inference rules Contraction and Weakening are derived rules of inference in the class of imll2 sequents we consider, as shown above.

The lj2 inference rule identity can be simulated in imll2 as follows:

\underline{\begin{matrix}\underline{\overline{C ⊢ C} \overline{C ⊢ C} \overline{C ⊢ C}} & ⊗R \\ C, C, C ⊢ C ⊗ C ⊗ C \end{matrix} \begin{matrix}\overline{H ⊢ H} & I \\ \overline{1, H ⊢ H} & 1L \end{matrix}}_{−∘L}

\underline{((C ⊗ C ⊗ C)−∘1), C, C, C, H ⊢ H}_{∀L}
C, C, C, W, H ⊢ H

The lj2 inference rules of ∀L and ∀R coincide with the imll2 inference rules of the same name.

The lj2 inference rules of ⇒R, and ∧L coincide with the imll2 inference rules −∘R and ⊗L.

The lj2 inference rules of ⇒L, and ∧R, and Cut all have two hypotheses. These rules coincide with −∘L, ⊗R, and Cut in imll2, but the C, C, C, W component of the conclusion sequent must be duplicated into both hypotheses in order to apply the inductive

I+  \overline{H ⊢ H}  \overline{H^{⊥} ⊢ H^{⊥}}  I-
IL  \overline{H, H^{⊥} ⊢}  \overline{⊢ H, H^{⊥}}  IR

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

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

⊕L \frac{Γ, A ⊢ Δ  Γ, B ⊢ Δ}{Γ, (A ⊕ B) ⊢ Δ}  \frac{Γ ⊢ A, Δ  Γ ⊢ B, Δ}{Γ ⊢ (A & B), Δ} & R

& L1  \frac{Γ, A ⊢ Δ}{Γ, (A & B) ⊢ Δ}  \frac{Γ ⊢ A, Δ}{Γ ⊢ (A ⊕ B), Δ}  ⊕R1

& L2  \frac{Γ, B ⊢ Δ}{Γ, (A & B) ⊢ Δ}  \frac{Γ ⊢ B, Δ}{Γ ⊢ (A ⊕ B), Δ}  ⊕R2

⊥L  \overline{⊥ ⊢}  \frac{Γ ⊢ Δ}{Γ ⊢ ⊥, Δ}  ⊥R

1L  \frac{Γ ⊢ Δ}{Γ, 1 ⊢ Δ}  \overline{⊢ 1}  1R
0L  \overline{Γ, 0 ⊢ Δ}  \overline{Γ ⊢ ⊤, Δ}  ⊤R

∀L  \frac{Γ, A[B/X] ⊢ Δ}{Γ, ∀X.A ⊢ Δ}  \frac{Γ ⊢ A[G/X], Δ}{Γ ⊢ ∀X.A, Δ}  ∀R

∃L  \frac{Γ, A[G/X] ⊢ Δ}{Γ, ∃X.A ⊢ Δ}  \frac{Γ ⊢ A[B/X], Δ}{Γ ⊢ ∃X.A, Δ}  ∃R

\frac{Σ ⊢ A, Θ  A, Γ ⊢ Δ}{Σ, Γ ⊢ Θ, Δ} Cut

Figure 4: Rules for mall2 hypothesis. This is straightforward since our encoding provides three copies of the formula C. As the contract rule makes use of two copies of the formula C, we need a third copy of this formula to be the object of contraction. For example, the −∘ L rule appears as follows:

\underline{C, C, C, W, Σ ⊢ B  C, C, C, W, Γ, D ⊢ A} _{−∘L}
\underline{C, C, C, C, C, C, W, W, Σ, Γ, B−∘D ⊢ A}_{Contract}
\underline{C, C, C, C, C, C, W, Σ, Γ, B−∘D ⊢ A}_{Contract}
\underline{C, C, C, C, C, W, Σ, Γ, B−∘D ⊢ A}_{Contract}
\underline{C, C, C, C, W, Σ, Γ, B−∘D ⊢ A}_{Contract}
C, C, C, W, Σ, Γ, B−∘D ⊢ A

The other binary rules are similar.

The converse of Lemma 3.3 is straightforward and actually one easily obtains a slightly stronger fact about the fragment imall2.

Lemma 3.4 If [Σ] ⊢ [A] in imall2, then Σ ⊢ A in lj2.

Proof. This is shown by a straightforward induction on size of proof. Essentially, imall2 proof rules are easily derivable from their counterparts in lj2, since the latter blurs the distinction between multiplicatives and additives.

The imll2 formulas C and W are the image of provable lj2 formulas C′ = ∀X.(X ⇒ X ∧ X) and W′ = ∀X.(X ⇒ T rue). That is, [C′] = C, ⊢ C′ is provable in lj2, [W′] = W, and ⊢ W′ is provable in lj2. One then obtains the following result.

Lemma 3.5 If C, C, C, W, [Σ] ⊢ [A] in imall2, then Σ ⊢ A in lj2.

Proof. By Lemma 3.4, given a proof of C, C, C, W, [Σ] ⊢ [A] in imall2, one can obtain a proof of C′, C′, C′, W′, Σ ⊢ A in lj2. By Cut and the above mentioned proofs of ⊢ C′ and ⊢ W′, one can construct the lj2 proof of Σ ⊢ A given in Figure 5 on the next page.

Theorem 3.6 imll2 and imall2 are undecidable.

Proof. By Lemma 3.5 and Lemma 3.3, the provability of lj2 sequents can be decided using imll2 or using imall2. However, lj2 is undecidable [22, 5] and therefore both imll2 and imall2 are undecidable.

3.1 Limitations

Our encoding is quite efficient at the levels of formula and proof, but is somewhat problematic at the level of cut normalization (lambda reduction). The standard sequent calculus cut-elimination procedure is extremely fast (polynomial) for imll and imll2 proofs. Cut normalization in propositional or secondorder intuitionistic logic is equivalent to lambda reduction in the simply or polymorphically typed lambda calculus, which has much greater computational complexity. Thus there is no possibility for the standard cut-elimination procedures to correspond nicely. An alternative is to create a non-standard cut-elimination algorithm that packages up the sequence of proof rules associated with each application of Contract or Weaken and introduce special rules for cut elimination through these packages. If one were able to reliably synchronize the cut-elimination procedure in imll2 with the cut-elimination procedure in lj2, then the two would correspond nicely, although some additional bookkeeping would be necessary in the imll2 proof. However, it is impossible to determine from an imll2 proof which steps correspond to Contract or Weaken and which correspond to lj2 steps. Unfortunately, the result of cut normalization then becomes ill-defined, as there are multiple normal forms for some proofs.

For example, consider the following lj2 proof, which involves cut of a contracted formula:

\underline{⋮ ; Γ ⊢ A  \underline{\overline{A ⊢ A}^{I} \overline{A ⊢ A}^{I}}_{∧R} ; \underline{A, A ⊢ A ∧ A}_{C} ; A ⊢ A ∧ A}_{Cut} ; Γ ⊢ A ∧ A

This proof is mapped to imll2 proof shown in Figure 6. In lj2 there is only one possible result of cut elimination:

\underline{⋮ ; Γ ⊢ A  ⋮ ; Γ ⊢ A} _{∧R}
\underline{Γ, Γ ⊢ A ∧ A}_{C} ⋮ / (\overline{Γ ⊢ A ∧ A}^{C})

In imll2, if one treats Contract as a single unit with special handling during cut elimination, then one obtains a proof analogous to the lj2 cut-free proof:

\underline{⋮ ; C, C, C, W, [Γ] ⊢ [A]  ⋮ ; C, C, C, W, [Γ] ⊢ [A]} _{⊗R}
\underline{C, C, C, C, C, C, W, W, [Γ], [Γ] ⊢ [A] ⊗ [A]}_{Contract}
⋮
\overline{C, C, C, W, [Γ] ⊢ [A] ⊗ [A]}^{Contract}

But if the standard imll2 cut-elimination process is applied to the original imll2 proof given in Figure 6, where the sequence of rule applications that make up Contract are treated individually, the cut-elimination process is short-circuited and the result is the cut-free proof shown in Figure 7.

The point is that the result of imll2 cut elimination is not the image of the reduced lj2 proof. The standard imll2 cut-elimination procedure reduces imll2 cuts very efficiently, but the resulting proofs have no direct correspondence to the reduced lj2 proofs. It is possible to imagine a non-standard cut-elimination process for imll2 that would treat Contract and Weaken as units. However, it would be impossible to tell without direct reference to an lj2 proof whether an imll2 rule application corresponds to a Contract step or the reduction of a similar-looking lj2 formula.

⋮ ⊢ W′

⋮ ⊢ C′ ⋮ ; ⊢ C′  \begin{matrix}\underline{⋮ ; ⊢ C′  ⋮ ; C′, C′, C′, W′, Σ ⊢ A} & Cut \\ C′, C′, W′, Σ ⊢ A \end{matrix} Cut C′, W′, Σ ⊢ A Cut W′, Σ ⊢ A Cut Σ ⊢ A

Figure 5: Faithfulness of the encoding

⋮ C, C, C, W, [Γ] ⊢ [A] \underline{\overline{C, C, C, W, [A] ⊢ [A]}^{I′} \overline{C, C, C, W, [A] ⊢ [A]}^{I′}}_{⊗R} \underline{C, C, C, C, C, C, W, W, [A], [A] ⊢ [A] ⊗ [A]}_{Contract}

C, C, C, W, [A] ⊢ [A] ⊗ [A] Cut

\underline{C, C, C, C, C, C, W, W, [Γ] ⊢ [A] ⊗ [A]}_{Contract}
C, C, C, W, [Γ] ⊢ [A] ⊗ [A]

Figure 6: Cut on a contracted formula in imll2

\underline{⋮ ; C, C, C, W, [Γ] ⊢ [A] \overline{C ⊢ C}^{I}}_{⊗R} C, C, C, C, W, [Γ] ⊢ C ⊗ [A]

\underline{\overline{C, C, C, W, [A] ⊢ [A]}^{I′} \overline{C, C, C, W, [A] ⊢ [A]}^{I′}}_{⊗R}

\underline{C, C, C, C, C, C, W, W, [A], [A] ⊢ [A] ⊗ [A]}_{Contract}
C, C, C, W, [A], [A] ⊢ [A] ⊗ [A]
\overline{C ⊗ [A], C, C, W, [A] ⊢ [A] ⊗ [A]}^{⊗L}
\overline{C ⊗ [A], C ⊗ [A], C, W ⊢ [A] ⊗ [A]}^{⊗L}
\overline{(C ⊗ [A]) ⊗ (C ⊗ [A]), C, W ⊢ [A] ⊗ [A]}^{⊗L} −∘L
\underline{(C ⊗ [A])−∘((C ⊗ [A]) ⊗ (C ⊗ [A])), C, C, C, C, C, W, W, Γ ⊢ [A] ⊗ [A]}_{∀L}
\underline{C, C, C, C, C, C, W, W, [Γ] ⊢ [A] ⊗ [A]}_{Contract}
C, C, C, W, [Γ] ⊢ [A] ⊗ [A]

Figure 7: The result of standard imll2 cut-elimination on the proof in Figure 6

4 Representing classical logic

In this section we represent second-order classical predicate logic lk12 in mll12 and in mall12. This yields the undecidability of both of these fragments of second-order linear logic and thus improves somewhat Amiot’s earlier result that mll12 (and mall12) with function symbols are undecidable [2].

One uses essentially the same encoding given above for lj2, but for the classical connectives and sequents with extension to include first-order quantifiers. The additional clauses are [F alse]=^{Δ}⊥, [¬H]=^{Δ}[H]^{⊥},

[∃X.A]=^{Δ}∃X.[A], [∀x.A]=^{Δ}∀x.[A], and [∃x.A]=^{Δ}∃x.[A].

Soundness and completeness of the representation are obtained as in the previous section.

Lemma 4.1 If Σ ⊢ Δ in lk12, then C, C, C, W, [Σ] ⊢ [Δ] in mll12.

Proof. As before, C and W encode contraction and weakening on the left. Observe that the negation rules are derivable in mll12, namely from Γ, A ⊢ Δ one can infer Γ ⊢ A^{⊥}, Δ, and from Γ ⊢ A, Δ one can infer Γ, A^{⊥} ⊢ Δ. Thus contraction and weakening on the right as well as other inference rules in lk12 become derived rules in mll12.

Lemma 4.2 If C, C, C, W, [Σ] ⊢ [Δ] in mall12, then Σ ⊢ Δ in lk12.

Proof. As before, there exist C′ and W′ such that [C′] = C and [W′] = W. Thus since every proof rule in mll12 is a proof rule of lk12, and C′ and W′ are valid lk12 formulae, completeness follows.

Theorem 4.3 mll12 and mall12 with at least one binary predicate variable are undecidable.

5 Further research

Our encoding of lj2 into imll2 critically depends on the native ‘intuitionistic’ assumption in imll2. There is no obvious way to prevent classically valid but intutionistically invalid formulas from being provable under embeddings into mll2 or mall2 in this vein. Certainly mll2 is not conservative over imll2 nor is mall2 conservative over imall2. For example, our encoding of Peirce’s law C, C, C, W ⊢ (∀X.∀Y.(((X−∘Y)−∘X)−∘X)) is provable in mll2 but not imll2.

The undecidability of mall2 is shown in subsequent work of Lafont [15] by using a weaker version of our formula C in an encoding of register machines. A particularly interesting aspect of the argument in [15] is that the faithfulness of the encoding is obtained as an application of the soundness theorem for phase semantics of linear logic [7, 9]. Furthermore, Lafont and Scedrov [16] show the undecidability of mll2 by similar methods.

The conservativity of imall2 over imll2, an open problem, is not needed for Theorem 4.3. Moreover, when the initially constructed proof of C′, C′, C′, W′, Σ ⊢ A in lj2 contains no uses of contraction or weakening (for instance, when it arises from an imll2 proof), the final proof uses contraction in only three places (the proofs of ⊢ C′) and weakening in only one place (the proof of ⊢ W′). The process of cut elimination essentially distributes the uses of contraction and weakening throughout the proof to all the places where C and W were used in essential ways in the imll2 proof. If one considers a cut-free lj2 proof translated to imll2 and back again using the above two lemmas, cut elimination on the result can be made to produce exactly the original proof. Thus there is a great deal of efficiency in this translation.

It is curious that we require three copies of the formula C in the translated sequent. As it happens, there is an alternate encoding.

T =^{Δ} ∀X.X−∘(X ⊗ X ⊗ X)

[Σ ⊢ A] =^{Δ} T, T, W, [Σ] ⊢ [A]

The formula T (for triplicate) is similar to C, but produces three copies of the target formula. The sequent can then be encoded using only two copies of the formula T and one of W. The contraction and weakening rules are derived rules of inference for sequents of the above form, and the proof of faithfulness proceeds along the same lines as for the above encoding.

Our two encodings use three occurrences of a contraction formula (C) that produces two copies, or two occurrences of a formula (T) that produces three copies. Lafont [15] and Lafont and Scedrov [16] use an encoding with only two copies of a contraction formula that produces two copies of a given formula. This is sufficient for those cases since there is exactly one main branch of their proof, while in our encoding we must follow an intuitionistic proof that may require contraction along many branches. It is the need to copy the contraction formula itself in order to be able to perform contraction along all branches of a proof that motivates using three copies of the formula C in our encoding.

The exact relationships among mll2, mall2, and full second-order propositional linear logic, as well as the relationships among their “intuitionistic” versions, are as yet unknown. For instance, it is not known whether full second-order propositional linear logic is conservative over mall2 and whether mall2 is conservative over mll2. In the later case, an interesting example is provided by Yves Lafont. Consider the formula ∃Z.(Z−∘E)⊗(Z−∘D)⊗(A−∘Z)⊗(B−∘Z) where A−∘E, B−∘E, A−∘D, and B−∘D are all provable in mll2. This formula is readily provable in mall2 by letting Z = E&D. On the other hand, in order to provide a mll2 proof it would be necessary to find an interpolant in mll2, which is problematic even in the relatively simple case when E and D are distinct atoms G and G′ respectively: A = (∀U.U−∘G) ⊗ (∀U.U−∘G′), and B = (∀U.U−∘1) ⊗ G ⊗ G′.

The decidability of the “explicit” version of imll2 analogous to Harper and Mitchell’s explicit ML [12], where the second-order quantification only ranges over quantifier-free formulas, is also open. By the corresponding result for mll, the decision problem is at least np-hard but no upper bound is as yet known.

Some restricted fragments of mall2 are trivially decidable: mall2 is decidable in the case that each essentially existential variable (that is bound by a positive existential or negative universal quantifier) does not have both positive and negative occurrences.

The decidability of mell, the fragment of quantifier-free propositional logic that contains multiplicatives and exponentials (modalities) but not additives, remains an interesting open problem.

6 Conclusion

The main surprise of this study is that the structural rules of contraction and weakening may be simulated by second-order propositional quantifiers and the multiplicatives. This gives rise to direct representations of second-order classical and intuitionistic logic in second-order linear logic without modalities. Primary among these encodings is the embedding of lj2 in imll2, demonstrating the undecidability of imll2. Other embeddings considered here show the undecidability of imall2, mll12, and mall12. These embeddings preserve proof structure including cuts, and can be used to analyze the uses of structural rules in lj2 proofs. This may have applications in the control structure of second-order logic programs.

References

[1] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111:3–57, 1993.

[2] G. Amiot. Unification et logique du second ordre. PhD thesis, Université Paris 7 (Denis Diderot), 1994.

[3] N. Benton, G. Bierman, V. de Paiva, and J.M.E. Hyland. Linear lambda-calculus and categorical models revisited. In Computer Science Logic ’92, Selected Papers, pages 61–84. Springer LNCS, vol. 702, 1993.

[4] J. Chirimar, C. Gunter, and J. Riecke. Reference counting as a computational interpretation of linear logic. Manuscript, 1993. Available by anonymous ftp from the machine research.att.com in the file dist/riecke/linear-logic-journal.ps.

[5] D.M. Gabbay. Semantical investigations in Heyting’s intuitionistic logic. Reidel, Dordrecht, 1981.

[6] V. Gehlot and C.A. Gunter. Normal process representatives. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[7] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[8] J.-Y. Girard. Light linear logic. Manuscript, 1995. Available by anonymous ftp from lmd.univmrs.fr as /pub/girard/LLL.ps.Z.

[9] J.-Y. Girard. Linear logic: its syntax and semantics. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in linear logic.

London Mathematical Society Lecture Note Series, Cambridge University Press, 1995. Available by anonymous ftp from lmd.univ-mrs.fr as /pub/girard/Synsem.ps.Z.

[10] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989.

[11] J.-Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic: A modular approach to polynomial time computability. Theoretical Computer Science, 97:1–66, 1992.

[12] R. Harper and J. C. Mitchell. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15(2):211– 252, April 1993.

[13] J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110:327– 365, 1994. Draft available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/miller/ic92.dvi.Z.

[14] M.I. Kanovich. The complexity of Horn fragments of linear logic. Annals of Pure and Applied Logic, 69:195–241, 1994. Extended abstract in: 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, June 1992, pages 200-210.

[15] Y. Lafont. The undecidability of second order linear logic without exponentials. Journal of Symbolic Logic, to appear, 1995. Available by anonymous ftp from lmd.univ-mrs.fr as /pub/lafont/mall2.ps.Z.

[16] Y. Lafont and A. Scedrov. The undecidability of second order multiplicative linear logic. Manuscript, 1995. Available by anonymous ftp from ftp.cis.upenn.edu as pub/papers/scedrov/mrs.[dvi,ps].Z.

[17] P. Lincoln and A. Scedrov. First order linear logic without modalities is NEXPTIMEhard. Theoretical Computer Science, 135:139– 154, 1994. Available from host ftp.cis.upenn.edu in pub/papers/scedrov/mall1.dvi.Z.

[18] P. Lincoln and T. Winkler. Constant-Only Multiplicative Linear Logic is NP-Complete. Theoretical Computer Science, 135:155–169, 1994. Available using anonymous ftp from host ftp.csl.sri.com and the file pub/lincoln/comultnpc.dvi.

[19] P. D. Lincoln and J. C. Mitchell. Operational aspects of linear lambda calculus. In Proc. 7th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 235– 246. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[20] P. D. Lincoln, J. C. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56:239–311, 1992. Extended abstract in: 31st Annual IEEE Symposium on Foundations of Computer Science, Volume 2, St. Louis, Missouri, October, 1990, pages 662-671.

[21] P. D. Lincoln and N. Shankar. Proof search in first-order linear logic and other cut-free sequent calculi. In Proc. 9-th Annual IEEE Symposium on Logic in Computer Science, Paris, pages 282– 291, July 1994.

[22] M.H. Loeb. Embedding first-order predicate logic in fragments of intuitionistic logic. Journal of Symbolic Logic, 41:705–718, 1976.

[23] D. Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, Proceedings of the 1992 Workshop on Extensions to Logic Programming, number 660 in Lecture Notes in Computer Science. Springer-Verlag, 1993. Available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/miller/pic.dvi.Z.

[24] D. Miller. A multiple-conclusion meta-logic. In Proc. 9-th Annual IEEE Symposium on Logic in Computer Science, Paris, pages 272–281, July 1994.

[25] A. Scedrov. A brief guide to linear logic. In G. Rozenberg and A. Salomaa, editors, Current Trends in Theoretical Computer Science, pages 377–394. World Scientific Publishing Co., 1993.

[26] A. Scedrov. Linear logic and computation: A survey. In H. Schwichtenberg, editor, Proof and Computation, Proceedings Marktoberdorf Summer School 1993, pages 281– 298. NATO Advanced Science Institutes, Series F, Springer-Verlag, Berlin, 1994. Available from the host ftp.cis.upenn.edu as the file pub/papers/scedrov/mdorf93.[dvi,ps].Z. See pub/papers/TableOfContents.

[27] G. Takeuti. Proof Theory. North-Holland, 1987. 2nd edition.

[28] A.S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes No. 29. Center for the Study of Language and Information, Stanford University,