The undecidability of second order multiplicative linear logic

Yves Lafont^{∗}

Laboratoire de Mathématiques Discrètes, UPR 9016 du CNRS, 163 Avenue de Luminy, Case 930, 13288 Marseille Cedex 9, France

and

Andre Scedrov^{†}

Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395, USA

March 21, 1995

Abstract The multiplicative fragment of second order propositional linear logic is shown to be undecidable.

Introduction

Decision problems for propositional (quantifier-free) linear logic were first studied by Lincoln et al. [LMSS]. 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 propositional quantifiers, and I for “intuitionistic” version.

In [LMSS] it was shown that full propositional linear logic is undecidable and that MALL is PSPACEcomplete. The main problems left open in [LMSS] 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, but almost all the other problems have been solved:

• The NP-completeness of MLL has been obtained by Kanovich [K1]. Moreover, Lincoln and Winkler [LW] have established that MLL without proper atoms is already NP-complete.

• MALL1 with function symbols is NEXPTIME-complete: the hardness has been obtained by Lincoln and Scedrov [LSv] and the membership, and hence completeness, by Lincoln and Shankar [LSr].

• Lincoln et al. [LSS] have recently showed the undecidability IMLL2 and IMALL2. Lafont [Lt] then proved the undecidability of MALL2.

Here we use a refinement of the methods from [LSS] and [Lt] to establish the undecidability of MLL2.

In [LSS] a simple encoding of second order propositional intuitionistic logic in IMLL2 is described, which uses the formula ∀α. (α −∘ α ⊗ α) to encode the structural rule of contraction. This encoding does not yield the undecidability in the classical case. Instead, a weaker formula ∀α. (α & 1 −∘ α ⊗ α) is used in [Lt]. The additive formula α & 1 serves as an approximation of the exponential !α in an encoding of register machines in propositional linear logic, which comes from [K2] and essentially goes back to [LMSS]. In [Lt] the faithfulness of the encoding is obtained as an application of the soundness theorem for the phase semantics of linear logic [G1, G2]. The present argument follows a similar pattern. However, the formula α & 1 is replaced by a multiplicative approximation α ⊗(α −∘ 1) and a new encoding of register machines is presented in order to avoid the use of additives in the encoding of the zero-test instruction.

∗E-mail address: lafont@lmd.univ-mrs.fr

†E-mail address: andre@cis.upenn.edu. WWW: http://www.cis.upenn.edu/~andre. Partially supported by NSF Grant CCR-94-00907, by ONR Grant N00014-92-J-1916, and by CNRS. Scedrov is an American Mathematical Society Centennial Research Fellow.

The first two sections of this paper recall the syntax and semantics of second order multiplicative linear logic. For more information, we refer to [G1, G2, Sv].

1 Syntax of IMLL2 and MLL2

The connectives of IMLL2 are the multiplicatives ⊗, 1, −∘ and the second order propositional quantifiers ∀, ∃. The sequents are of the form Γ ⊢ A where Γ is a multiset of formulas and A is a formula. The rules are:

A ⊢ A  {Γ ⊢ A Δ, A ⊢ C \atop Γ, Δ ⊢ C}

{Γ ⊢ A Δ ⊢ B \atop Γ, Δ ⊢ A ⊗ B}  {Γ, A, B ⊢ C \atop Γ, A ⊗ B ⊢ C}  ⊢ 1  {Γ ⊢ C \atop Γ, 1 ⊢ C}  {Γ, A ⊢ B \atop Γ ⊢ A −∘ B}  {Γ ⊢ A Δ, B ⊢ C \atop Γ, Δ, A −∘ B ⊢ C}

{Γ ⊢ A[B] \atop Γ ⊢ ∃α. A[α]}  {Γ, A[β] ⊢ C \atop Γ, ∃α. A[α] ⊢ C}  {Γ ⊢ A[β] \atop Γ ⊢ ∀α. A[α]}  {Γ, A[B] ⊢ C \atop Γ, ∀α. A[α] ⊢ C}

In the ∃-left and ∀-right rules, β is a fresh propositional variable. In fact, ⊗, 1, and ∃ are definable in terms of −∘ and ∀:

A ⊗ B ≡ ∀α. ((A −∘ B −∘ α) −∘ α),  1 ≡ ∀α. (α −∘ α),  ∃α. A[α] ≡ ∀β. ((∀α. (A[α] −∘ β)) −∘ β),

where β is a fresh propositional variable. The connectives of MLL2 are the multiplicatives ⊗, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , 1, ⊥ and the second order propositional quantifiers ∀, ∃. Linear negation A^{⊥} is given for propositional variables or atoms. It is extended to all formulas by α^{⊥⊥} = α and by

\begin{matrix}(A ⊗ B)^{⊥} = A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B^{⊥},  (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} = A^{⊥}⊗ B^{⊥},  1^{⊥} = ⊥,  ⊥^{⊥} = 1, \\ (∃α. A[α])^{⊥} = ∀α. A[α]^{⊥},  (∀α. A[α])^{⊥} = ∃α. A[α]^{⊥}. \end{matrix}

The sequents are of the form ⊢ Γ where Γ is a multiset of formulas, and the rules are:

⊢ A, A^{⊥}  {⊢ A, Γ ⊢ A^{⊥}, Δ \atop ⊢ Γ, Δ}

{⊢ A, Γ ⊢ B, Δ \atop ⊢ A ⊗ B, Γ, Δ}  {⊢ A, B, Γ \atop ⊢ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, Γ}  ⊢ 1  {⊢ Γ \atop ⊢ ⊥, Γ}

{⊢ A[β], Γ \atop ⊢ ∀α. A[α], Γ}  {⊢ A[B], Γ \atop ⊢ ∃α. A[α], Γ}

In the ∀ rule, β is a fresh propositional variable. Linear implication is defined by A −∘ B = A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B. An intuitionistic sequent A_{1}, …, A_{n} ⊢ C is interpreted as ⊢ A_{1}^{⊥}, …, A_{n}^{⊥}, C, so that MLL2 can be seen as a (non-conservative) extension of IMLL2.

2 Phase semantics of MLL2

A phase space [G1, G2] is a commutative monoid M endowed with a subset ⊥ of M. If X, Y ⊂ M define

XY = {xy; x ∈ X and y ∈ Y },  X −∘ Y = {z ∈ M; xz ∈ Y for all x ∈ X},  X^{⊥} = X −∘ ⊥.

Also, if x ∈ M and Y ⊂ M, it is convenient to write xY for {x}Y and x −∘ Y for {x} −∘ Y. A fact is an X ⊂ M such that X^{⊥⊥} = X. It is easy to see that X ⊂ X^{⊥⊥} and X^{⊥} = X^{⊥⊥⊥} for any X ⊂ M, so that X^{⊥} is always a fact. In particular ⊥ = {1}^{⊥} is a fact. Also, X −∘ Y is a fact whenever Y is a fact, and any intersection of facts is a fact. In particular, X^{⊥⊥} is the intersection of all facts containing X, that is, the smallest fact containing X. Define 1 = ⊥^{⊥} = {1}^{⊥⊥}. For any facts X, Y let

X ⊗ Y = (XY)^{⊥⊥}, X^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Y = (X^{⊥}⊗ Y^{⊥})^{⊥} = (X^{⊥}Y^{⊥})^{⊥}.

From these definitions one deduces easily for any X, Y ⊂ M,

X^{⊥⊥}⊗ Y^{⊥⊥} = (XY)^{⊥⊥}, X^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Y^{⊥⊥} = X^{⊥⊥} −∘ Y^{⊥⊥} = X −∘ Y^{⊥⊥} = Y^{⊥} −∘ X^{⊥}.

In particular, X^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Y = X −∘ Y whenever Y is a fact, which justifies the notation a posteriori. Furthermore, for any X_{1}, …, X_{n}, Y ⊂ M, one gets

X_{1}^{⊥⊥}⊗ ⋯ ⊗ X_{n}^{⊥⊥} = (X_{1} ⋯ X_{n})^{⊥⊥}, X_{1}^{⊥⊥}⊗ ⋯ ⊗ X_{n}^{⊥⊥} −∘ Y^{⊥⊥} = X_{1} ⋯ X_{n} −∘ Y^{⊥⊥}.

If a fact α^{•} is given for each atom α occurring in a formula A of MLL, one defines a fact A^{•} by applying the above definitions inductively, and this interpretation is extended to MLL2 as follows:

(∀α. A[α])^{•} = ⋂_{X⊂M} A_{X}^{•}

where A_{X}^{•} is the interpretation defined by A_{X}^{•} = X^{⊥⊥} for A[α] = α. One says that M satisfies a formula A when 1 ∈ A^{•}.

Theorem 1 (Girard [G1]) If A is provable in MLL2, then M satisfies A.

We shall not need the converse, which does not hold for this restricted notion of second order model. An easy consequence of theorem 1 is that A_{1}^{•} ⋯ A_{n}^{•} ⊂ B^{•} whenever A_{1}, …, A_{n} ⊢ B is provable in MLL2. This holds more generally whenever Γ, A_{1}, …, A_{n} ⊢ B is provable and M satisfies all formulas in Γ.

3 Encoding a restricted kind of contraction

Let A^{n} denote the tensor product A ⊗ ⋯ ⊗ A of n occurrences of A. Let #A denote A ⊗(A −∘ 1). If Γ is a multiset A_{1}, …, A_{n} let #Γ denote #A_{1}, …, #A_{n}. Note that the sequent #A ⊢ 1 is always provable. Furthermore, A ⊢ #A is provable whenever A ⊢ 1 is provable. In particular, #1 is equivalent to 1. The following formula encodes a restricted kind of contraction:

ρ = ∀α. ∀β. (#α ⊗ #β −∘ α^{2} ⊗ #β ⊗ β).

Lemma 1 The following rules are derivable in IMLL2:

{Γ ⊢ C \atop ρ^{2}, #Θ, Γ ⊢ C}  {ρ^{2}, #A, A, Γ ⊢ C \atop ρ^{2}, #A, Γ ⊢ C}

Proof. The sequents ρ ⊢ #1 ⊗ #1 −∘ 1^{2} ⊗ #1 ⊗ 1 and ρ ⊢ #ρ ⊗ #A −∘ ρ^{2} ⊗ #A ⊗ A are provable by definition of ρ. But 1 ⊗ #1 −∘ 1^{2} ⊗ #1 ⊗ 1 is clearly equivalent to 1, so that ρ ⊢ 1 is provable, and also ρ ⊢ #ρ by the above remark. It follows easily that our two rules are derivable. Q.e.d.

Lemma 2 ρ is satisfied by any phase space M satisfying the following conditions:

1. The unit 1 is the only element of the fact 1,

2. The unit 1 is the only invertible element in M. Proof. By definition of the interpretation, one has

ρ^{•} = ⋂_{X,Y ⊂M} X(X −∘ 1)Y (Y −∘ 1) −∘ (X^{2}Y^{2}(Y −∘ 1))^{⊥⊥}.

Let X, Y ⊂ M. If x ∈ X and z ∈ X −∘ 1, then xz ∈ 1, so that xz = 1 by the first condition and x = z = 1 by the second one. The same holds for Y, so that

X(X −∘ 1)Y (Y −∘ 1) ⊂ X^{2}Y^{2}(Y −∘ 1) ⊂ (X^{2}Y^{2}(Y −∘ 1))^{⊥⊥},

which means that ρ is satisfied. Q.e.d. Note that the second condition is automatically satisfied if M is a free commutative monoid.

4 Two counter machines

If i ≤ j are integers, we write [i, j] for the set {i, i+1, …, j}. A deterministic two counter machine is given by an integer m > 0 and a map

τ : [1, m] → {+} × {1, 2} × [0, m] ∪ {−} × {1, 2} × [0, m] × [0, m].

If, at a given time, the machine is in the configuration (i, p, q) ∈ [0, m] × N × N, its next configuration is: • (j, p+1, q) if τ(i) = (+, 1, j) (increment first counter),

• (j, p−1, q) if τ(i) = (−, 1, j, k) and p > 0 (decrement first counter),

• (k, p, q) if τ(i) = (−, 1, j, k) and p = 0 (test that first counter is zero),

• (j, p, q+1) if τ(i) = (+, 2, j) (increment second counter),

• (j, p, q−1) if τ(i) = (−, 2, j, k) and q > 0 (decrement second counter),

• (k, p, q) if τ(i) = (−, 2, j, k) and q = 0 (test that second counter is zero). Since τ is only defined for i ∈ [1, m], the machine stops when i = 0. One says that a configuration (i, p, q) is accepted by the machine if, starting from (i, p, q), the machine eventually stops on (0, 0, 0). Theorem 2 (Lambek [Lk], Minsky [M]) There is a deterministic two counter machine for which the set of accepted configurations is not recursive. In the following sections, such a machine is used to show that both IMLL2 and MLL2 are undecidable.

5 Encoding two counter machines

Let a, c_{0}, c_{1}, …, c_{m} be atoms, and let φ[α] and ψ[α] be two formulas with one free propositional variable α. If i ∈ [0, m] and p, q ∈ N, the configuration (i, p, q) will be represented by the formula c_{i} ⊗ φ[a^{p}] ⊗ ψ[a^{q}]. In particular, the configuration (0, 0, 0) will be represented by ω = c_{0} ⊗ φ[1] ⊗ ψ[1]. Let Θ be the multiset consisting of the following formulas:

∀α. (c_{i} ⊗ φ[α] −∘ c_{j} ⊗ φ[a ⊗ α])  for i ∈ [1, m] such that τ(i) = (+, 1, j),
\{ \begin{matrix}∀α. (c_{i} ⊗ φ[a ⊗ α] −∘ c_{j} ⊗ φ[α]) \\ c_{i} ⊗ φ[1] −∘ c_{k} ⊗ φ[1] \end{matrix} for i ∈ [1, m] such that τ(i) = (−, 1, j, k),

and similarly for the second counter, using ψ instead of φ.

Theorem 3 There are formulas φ[α] and ψ[α] such that, for any (i, p, q) ∈ [0, m] × N × N, the following assertions are equivalent:

1. The configuration (i, p, q) is accepted by the machine,

2. The sequent ρ^{2}, #Θ, c_{i}, φ[a^{p}], ψ[a^{q}] ⊢ ω is provable in IMLL2,

3. The latter sequent is provable in MLL2.

The assertion that (1) implies (2) holds independently of the choice of φ[α] and ψ[α]. This is proved by a straightforward induction on the length of the computation. The first rule in lemma 1 is used in the base case. The second rule in lemma 1 is used in the induction step. For instance, an increment transition is handled as follows:

\begin{matrix}\begin{matrix}c_{i} ⊢ c_{i} & φ[a^{p}] ⊢ φ[a^{p}] \\ c_{i}, φ[a^{p}] ⊢ c_{i} ⊗ φ[a^{p}] \end{matrix} & \begin{matrix}· \\ · \\ · \end{matrix} ; ρ^{2}, #Θ, c_{j}, φ[a^{p+1}], ψ[a^{q}] ⊢ ω ; ρ^{2}, #Θ, c_{j} ⊗ φ[a^{p+1}], ψ[a^{q}] ⊢ ω \\ ρ^{2}, #Θ, c_{i} ⊗ φ[a^{p}] −∘ c_{j} ⊗ φ[a^{p+1}], c_{i}, φ[a^{p}], ψ[a^{q}] ⊢ ω \end{matrix} ; ρ^{2}, #Θ, ∀α. (c_{i} ⊗ φ[α] −∘ c_{j} ⊗ φ[a ⊗ α]), c_{i}, φ[a^{p}], ψ[a^{q}] ⊢ ω ; ρ^{2}, #Θ, c_{i}, φ[a^{p}], ψ[a^{q}] ⊢ ω

Also, it is clear that (2) implies (3). The next section is devoted to the hard part of the proof, namely that (3) implies (1) for some appropriate φ[α] and ψ[α]:

φ[α] = α^{3} ⊗(α −∘ d) ⊗(α −∘ e) −∘ f, ψ[α] = α^{3} ⊗(α −∘ d) ⊗(α −∘ e) −∘ g,

where d, e, f, g are new atoms.

6 Faithfulness of the encoding

In order to show that the above encoding is faithful, consider the free commutative monoid M generated by the atoms a, c_{0}, c_{1}, …, c_{m}, \overline{d}, \overline{e}, \overline{f}, \overline{g} and by the infinite families (d_{n}), (e_{n}), (f_{n}), (g_{n}), all indexed by N. The structure of phase space is given by

⊥ = \{c_{i}f_{p}g_{q}; (i, p, q) is accepted by the machine\} ∪ \{\overline{d}d_{n}a^{n}; n ∈ N\} ∪ \{\overline{e}e_{n}a^{n}; n ∈ N\} ∪
\{\overline{f}f_{n}d_{n+p}e_{n+q}a^{3n+p+q}; n, p, q ∈ N\} ∪ \{\overline{g}g_{n}d_{n+p}e_{n+q}a^{3n+p+q}; n, p, q ∈ N\}.

The interpretation is defined by

\begin{matrix}a^{•} = \{a\}^{⊥⊥},  c_{i}^{•} = \{c_{i}\}^{⊥⊥},  d^{•} = \{\overline{d}\}^{⊥} = \{d_{n}a^{n}; n ∈ N\},  e^{•} = \{\overline{e}\}^{⊥} = \{e_{n}a^{n}; n ∈ N\}, \\ f^{•} = \{\overline{f}\}^{⊥} = \{f_{n}d_{n+p}e_{n+q}a^{3n+p+q}; n, p, q ∈ N\},  g^{•} = \{\overline{g}\}^{⊥} = \{g_{n}d_{n+p}e_{n+q}a^{3n+p+q}; n, p, q ∈ N\}. \end{matrix}

Note that the singleton \{a^{n}\} = \{\overline{d}d_{n}\}^{⊥} is a fact for any n ∈ N. In particular, \{1\} = \{a^{0}\} is a fact and 1 = ⊥^{⊥} = {1}, so that ρ is satisfied by lemma 2.

Lemma 3 Let X ⊂ M. If X is of the form {a^{n}}, then φ_{X}^{•} = {f_{n}} and ψ_{X}^{•} = {g_{n}}, else φ_{X}^{•} = ψ_{X}^{•} = M.

Proof. Let us discuss φ_{X}^{•}; the case of ψ_{X}^{•} is similar. By definition of the interpretation, one has

φ_{X}^{•} = X^{3}(X −∘ d^{•})(X −∘ e^{•}) −∘ f^{•}.

If x ∈ M, the fact x −∘ d^{•} is

{d_{n+p}a^{p}; p ∈ N} if x is of the form a^{n},  {a^{n}} if x is of the form d_{n+p}a^{p},  ∅ otherwise.

Similarly, the fact x −∘ e^{•} is

{e_{n+p}a^{p}; p ∈ N} if x is of the form a^{n},  {a^{n}} if x is of the form e_{n+p}a^{p},  ∅ otherwise.

Note that x −∘ d^{•} or x −∘ e^{•} is empty if x is not of the form a^{n}. Since the a^{n} −∘ d^{•} are pairwise disjoint, it follows easily that for any X ⊂ M, the set X^{3}(X −∘ d^{•})(X −∘ e^{•}) is

{d_{n+p}e_{n+q}a^{3n+p+q}; p, q ∈ N} if X is of the form {a^{n}}, ∅ otherwise.

Assume that X is of the form {a^{n}}. Clearly, ⊥ has been defined in such a way that f_{n} ∈ φ_{X}^{•}. Conversely, if z ∈ φ_{X}^{•}, then yz ∈ f^{•} for any y ∈ X^{3}(X −∘ d^{•})(X −∘ e^{•}), in particular for y = d_{n}e_{n}a^{3n}. This is only possible if z is of the form f_{r}a^{s}, in which case yz = f_{r}d_{n}e_{n}a^{3n+s} and there are p, q ∈ N such that

n = r + p,  n = r + q,  3n + s = 3r + p + q.

This gives p = q = −s, so that p = q = s = 0 and r = n, which means that z = f_{n}. Hence φ_{X}^{•} = {f_{n}}. Finally, if X is not of the form {a^{n}}, one gets φ_{X}^{•} = ∅ −∘ f^{•} = M. Q.e.d.

Here is an immediate consequence of this lemma: If i ∈ [0, m] and X is of the form {a^{p}}, then one has (c_{i}φ_{X}^{•})^{⊥} = {c_{i}f_{p}}^{⊥} = {g_{q}; (i, p, q) is accepted}, else (c_{i}φ_{X}^{•})^{⊥} = (c_{i}M)^{⊥} = ∅. It follows that all the formulas of Θ are satisfied:

• If A is ∀α. (c_{i} ⊗ φ[α] −∘ c_{j} ⊗ φ[a ⊗ α]) where τ(i) = (+, 1, j), then

A^{•} = ⋂_{X⊂M} c_{i}φ_{X}^{•} −∘ (c_{j}φ_{aX}^{•})^{⊥⊥} = ⋂_{X⊂M} (c_{j}φ_{aX}^{•})^{⊥} −∘ (c_{i}φ_{X}^{•})^{⊥}.

But if X is of the form {a^{p}}, then aX = {a^{p+1}} and

(c_{j}φ_{aX}^{•})^{⊥} = {g_{q}; (j, p+1, q) is accepted} ⊂ {g_{q}; (i, p, q) is accepted} = (c_{i}φ_{X}^{•})^{⊥},

else the inclusion holds trivially since (c_{j}φ_{aX}^{•})^{⊥} = ∅ = (c_{i}φ_{X}^{•})^{⊥}. So one has 1 ∈ (c_{j}φ_{aX}^{•})^{⊥} −∘ (c_{i}φ_{X}^{•})^{⊥} for any X, which means that A is satisfied.

• If A is ∀α. (c_{i} ⊗ φ[a ⊗ α] −∘ c_{j} ⊗ φ[α]) where τ(i) = (−, 1, j, k), the argument is similar.

• If A is c_{i} ⊗ φ[1] −∘ c_{k} ⊗ φ[1] where τ(i) = (−, 1, j, k), then

A^{•} = c_{i}φ1^{•} −∘ (c_{k}φ1^{•})^{⊥⊥} = (c_{k}φ1^{•})^{⊥} −∘ (c_{i}φ1^{•})^{⊥},

and

(c_{k}φ1^{•})^{⊥} = {g_{q}; (k, 0, q) is accepted} ⊂ {g_{q}; (i, 0, q) is accepted} = (c_{i}φ1^{•})^{⊥},

which means that A is satisfied.

• The three other cases are similar.

In fact, a stronger property is needed to prove the theorem, namely that #A, and not only A, is satisfied for every A in Θ. Let us say that a formula A, which encodes some transition of the machine, is relevant if this transition occurs in at least one accepting computation. It is easy to see that, if A is relevant, then A^{•} = {1} = 1 so that #A is satisfied. Otherwise, A^{•} = M and #A is not satisfied. Nothing ensures that all the formulas of Θ are relevant, but this problem can be solved easily in either of the following ways:

1. One can remove the irrelevant formulas from Θ without loosing the fact that ρ^{2}, #Θ, c_{i}, φ[a^{p}], ψ[a^{q}] ⊢ ω is provable whenever the configuration (i, p, q) is accepted.

2. Without changing Θ, one can introduce extra generators f_{∗}, g_{∗}, and put all c_{i}f_{p}g_{∗} and all c_{i}f_{∗}g_{q} in ⊥. It follows that (c_{i}φ_{X}^{•})^{⊥} = {g_{q}; (i, p, q) is accepted} ∪ {g_{∗}} ≠ ∅ whenever X is of the form {a^{p}}. This property and its analogue for ψ_{X}^{•} ensure that A^{•} = 1 (so that #A is satisfied by the new model) for every A in Θ.

In order to complete the proof of theorem 3, assume that ρ^{2}, #Θ, c_{i}, φ[a^{p}], ψ[a^{q}] ⊢ ω is provable in MLL2. Lemma 3 gives f_{p} ∈ φ[a^{p}]^{•}, g_{q} ∈ ψ[a^{q}]^{•}, and ω^{•} = {c_{0}f_{0}g_{0}}^{⊥⊥} = {1}^{⊥} = ⊥. Since ρ and all formulas of #Θ are satisfied, one gets c_{i}f_{p}g_{q} ∈ c_{i}^{•}φ[a^{p}]^{•}ψ[a^{q}]^{•} ⊂ ω^{•} = ⊥, which means that the configuration (i, p, q) is accepted.

Note that, in theorem 3, IMLL2 and MLL2 can be replaced by IMALL2 and MALL2. Since the phase semantics interprets the additives, the proof is exactly the same. Therefore one gets for free the undecidability of the four fragments, although the problem remained open only for MLL2.

7 Discussion

We do not claim that our encoding is the simplest possible one. In fact, the formulas φ[α] and ψ[α] have been constructed in such a way that lemma 3 holds, but it may happen that theorem 3 holds with simpler formulas. In any case, φ[α] and ψ[α] cannot be too simple. For instance, the trivial encoding given by φ[α] = ψ[α] = α does not work for an obvious reason: it mixes up the counters. Of course, one can try to encode (i, p, q) by c_{i} ⊗ a^{p} ⊗ b^{q}, using distinct atoms for the counters, but then the formula c_{i} ⊗ φ[1] −∘ c_{k} ⊗ φ[1] is equivalent to c_{i} −∘ c_{k}, which entails c_{i} ⊗ a^{p} ⊗ b^{q} −∘ c_{k} ⊗ a^{p} ⊗ b^{q} for any p, q ∈ N. This means that, if τ(i) = (−, 1, j, k), the transition (i, p, q) → (k, p, q) can be simulated even when p ≠ 0. In other words, the encoding of the 0-test is not faithful. For that precise reason, additives were needed in [LMSS, K2, Lt].

Negative formulas φ[α] = α −∘ f and ψ[α] = α −∘ g, where f and g are distinct atoms, lead into trouble as well. Assume indeed that the machine has the following transitions:

(i, p, q) → (j, p+1, q) for any p, q ∈ N, (j, 0, q) → (k, 0, q) for any q ∈ N.

These transitions are encoded by A = ∀α. (c_{i} ⊗(α −∘ f) −∘ c_{j} ⊗(a ⊗ α −∘ f)) and B = c_{j} ⊗ f −∘ c_{k} ⊗ f. In A, the variable α stands for an arbitrary formula, not necessarily of the form a^{n}. For instance, A entails c_{i} ⊗(f −∘ f) −∘ c_{j} ⊗(a ⊗ f −∘ f). Using this, it is easy to prove A, B ⊢ c_{i} ⊗ f −∘ c_{k} ⊗(a −∘ f), which means that the incorrect transition (i, 0, q) → (k, 1, q) can be simulated. In fact, there is another difficulty related to the use of # in the encoding. Assume indeed that the machine has the following transition:

(i, p+1, q) → (i, p, q) for any p, q ∈ N.

This transition is encoded by A = ∀α. (c_{i} ⊗(a ⊗ α −∘ f) −∘ c_{i} ⊗(α −∘ f)). Since α occurs negatively in φ[α], one proves a ⊢ A and then #A ⊢ A ⊗(a −∘ 1). Using this, it is possible to simulate an incorrect transition.

Acknowledgement

Andre Scedrov wishes to thank Jean-Yves Girard and members of the Equipe de Logique de la Programmation at LMD Marseille for their hospitality during his visit in January-March 1995, when this research was done.

References

[G1] Girard, J.-Y. (1987), Linear logic, Theoretical Computer Science 50, 1–102.

[G2] Girard, J.-Y. (1995), Linear logic: its syntax and semantics, to appear in “Advances in Linear Logic” (J.-Y. Girard, Y. Lafont and L. Regnier, Eds.), London Mathematical Society Lecture Note Series, Cambridge University Press.

[K1] Kanovich, M. (1994), The complexity of Horn fragments of linear logic, Annals of Pure and Applied Logic 69, 195–241.

[K2] Kanovich, M. (1995), The Direct Simulation of Minsky machines in Linear logic, to appear in “Advances in Linear Logic” (J.-Y. Girard, Y. Lafont and L. Regnier, Eds.), London Mathematical Society Lecture Note Series, Cambridge University Press.

[Lt] Lafont, Y. (1995), The undecidability of second order linear logic without exponentials, to appear in Journal of Symbolic Logic.

[Lk] Lambek, J. (1961), How to program an infinite abacus, Canadian Math. Bulletin 4, 295–302.

[LMSS] Lincoln, P., Mitchell, J., Scedrov, A., and Shankar, N. (1992), Decision Problems for Propositional Linear Logic, Annals of Pure and Applied Logic 56, 239–311.

[LSv] Lincoln, P., and Scedrov, A. (1994), First Order Linear Logic Without Modalities is NEXPTIME-Hard, Theoretical Computer Science 135, 139–154.

[LSS] Lincoln, P., Scedrov, A. and Shankar, N. (1995), Decision Problems for Second Order Linear Logic, in “Proc. 10-th Annual IEEE Symposium on Logic in Computer Science, San Diego, California.”

[LSr] Lincoln, P., and Shankar, N. (1994), 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,” 282–291.

[LW] Lincoln, P., and Winkler, T. (1994), Constant-Only Multiplicative Linear Logic is NP-Complete, Theoretical Computer Science 135, 155–169.

[M] Minsky, M. (1961), Recursive unsolvability of Post’s problem of ‘tag’ and other topics in the theory of Turing machines, Annals of Mathematics 74, 437–455.

[Sv] A. Scedrov (1993), A Brief Guide to Linear Logic, in “Current Trends in Theoretical Computer Science” (G. Rozenberg and A. Salomaa, Eds.), 377–394, World Scientific Publishing Co.