Decision Problems for Propositional Linear Logic

Patrick Lincoln^{1,3}  John Mitchell^{1}  Andre Scedrov^{2}

Natarajan Shankar^{3}

September 13, 1994

1Department of Computer Science, Stanford University, Stanford, CA 94305 2Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104 3Computer Science Laboratory, SRI International, Menlo Park, CA 94025

Abstract

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the “structural” rules of contraction and weakening; adding a modal operator; and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection, and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation and proof normalization in a bounded form of linear logic.

In this paper we show that unlike most other propositional (quantifier-free) logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes pspace-complete. We also establish membership in np for the multiplicative fragment, np-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic.

Contents

1 Introduction 3

2 Multiplicative Additive Propositional Linear Logic is PSPACE-complete 7 2.1 Membership in pspace . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 Informal Outline of pspace-hardness of mall . . . . . . . . . . . . . 8

2.2.1 Encoding Boolean Evaluation . . . . . . . . . . . . . . . . . . 9 2.2.2 Encoding Boolean Quantification . . . . . . . . . . . . . . . . 12

2.3 Formal Definition of the Encoding . . . . . . . . . . . . . . . . . . . 14 2.4 Proof of pspace-hardness of mall . . . . . . . . . . . . . . . . . . . 15

3 Propositional Linear Logic is Undecidable 23 3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.2 Linear Logic Augmented With Theories . . . . . . . . . . . . . . . . 24 3.3 Coding Theories in Formulas . . . . . . . . . . . . . . . . . . . . . . 26 3.4 And-Branching Two Counter Machines Without Zero-Test . . . . . . 28

3.4.1 Two Counter Machines . . . . . . . . . . . . . . . . . . . . . 29 3.5 From Machines to Logic . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.6 Example Computation . . . . . . . . . . . . . . . . . . . . . . . . . . 37

4 Noncommutative Propositional Linear Logic 40 4.1 ncl Proof Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.2 ncl is Undecidable . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.3 ncl Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

4.3.1 Semi-Thue Systems . . . . . . . . . . . . . . . . . . . . . . . 43 4.4 From Semi-Thue Systems to Noncommutative Linear Logic . . . . . 44 4.5 Other Noncommutative Logics . . . . . . . . . . . . . . . . . . . . . 46

4.5.1 Rotate Rule versus Embedding . . . . . . . . . . . . . . . . . 47 4.5.2 ncl without ?E . . . . . . . . . . . . . . . . . . . . . . . . . 47 4.5.3 Alternate ⊗ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.5.4 Mix and Match . . . . . . . . . . . . . . . . . . . . . . . . . . 48

4.6 Degenerate Noncommutative Linear Logics . . . . . . . . . . . . . . 49 2 Decision Problems for Propositional Linear Logic

4.6.1 Intermingling ⊗ . . . . . . . . . . . . . . . . . . . . . . . . . 49 4.6.2 Intermingling Cut . . . . . . . . . . . . . . . . . . . . . . . . 49

5 The Multiplicative Fragment 51 5.1 Multiplicatives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 5.2 Direct Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

6 Conclusion 56 Bibliography 58 A Cut Elimination 61

A.1 Cut of non-principal formulas . . . . . . . . . . . . . . . . . . . . . . 63 A.1.1 ⊗ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 A.1.2 � . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 A.1.3 ⊕ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 A.1.4 & . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

A.1.5 ?W . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
A.1.6 ?C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
A.1.7 ?D . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

A.1.8 ⊥ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 A.1.9 ⊤ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

A.1.10 Cut . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

A.2 Cut of principal formulas . . . . . . . . . . . . . . . . . . . . . . . . 66 A.2.1 I versus any . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 A.2.2 ⊗ versus � . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 A.2.3 & versus ⊕ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 A.2.4 ?W versus !S . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 A.2.5 ?C versus !S . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 A.2.6 ?D versus !S . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 A.2.7 !S versus !S . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 A.2.8 Cut∗ versus !S . . . . . . . . . . . . . . . . . . . . . . . . . . 70 A.2.9 ⊗ versus !S . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 A.2.10 ⊥ versus 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

A.3 Subformula Property . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 B Propositional Linear Logic Proof Rules 74

Chapter 1

Introduction

Linear logic is a refinement of classical logic introduced by Girard [Gir87a]. This logic has a “resource sensitive” character, reflected in the fact that two assumptions of a formula A are distinguished from a single assumption of A. In this paper, we study the decision problem for full propositional linear logic and several natural fragments. The easiest result to state is that full propositional linear logic is undecidable. We also show that an “intuitionistic” fragment is undecidable, a natural fragment is pspace-complete, and a smaller fragment that is in np becomes npcomplete with an additional rule. Before describing these results, we give a short overview of linear logic by explaining the passage from classical to linear logic.

Formally, linear logic may be derived in three steps from a Gentzen-style sequent calculus axiomatization of classical logic. The first step is to drop two structural rules, contraction and weakening. This forces a reexamination of conjunction and disjunction, leading to two forms of each connective. The third step is to recover the full expressive power of classical logic by adding two modal operators, ! and ?. These three steps are described in more detail in the following paragraphs. The resulting logic is surprisingly natural, from both proof-theoretic and computational standpoints. In particular, Gentzen-style cut-elimination, a crucial proof-theoretic property (see [Gen69, GLT89], for example), has been established for linear logic in [Gir87a]. This yields consistency and provides a natural computational mechanism that resembles reduction in lambda calculus (e.g., [HS86, GLT89]).

The derivation of linear logic begins by dropping the structural rules contraction and weakening, which are an essential part of classical and intuitionistic logic. Each rule may be applied to either the left or right side of a sequent. On the left, contraction allows repeated assumptions of some formula to be replaced by a single assumption of the same formula. This means that a single hypothesis is as good as any number of duplicates, or, a hypothesis may be “reused” as often as desired. Contraction on the right also allows duplicates to be dropped, which has essentially the same effect. Weakening on the left allows us to add irrelevant hypotheses, and, on the right, to extend the set of possible conclusions arbitrarily. Since contraction and weakening make it possible to use an assumption as little or as often as desired, these rules are responsible for what we may regard as a loss of control over resources in both classical and intuitionistic logic. Excluding these rules produces a linear system in which each assumption must be used exactly once, and each conclusion must follow from the hypotheses. In linear logic, formulas may be regarded as fixed resources that cannot necessarily be discarded or duplicated without effort.

The second step in deriving linear logic involves the propositional connectives. Briefly, the change in structural rules leads to two forms of conjunction and disjunction. The reason for the split is that we must decide whether we require linearity of the entire conjunction or disjunction, or whether it suffices to have each conjunct or disjunct alone depend linearly on the surrounding formulas. One form, called additive conjunction or disjunction, is informally described as “sharing of resources” since the two conjuncts or disjuncts may depend on a shared set of hypotheses. In the other multiplicative form, there is no such sharing. The general situation may be illustrated by examining two consequences of the pair of linear implications A−∘B and A−∘C. Intuitively, A−∘B says that from A we may conclude B, or, in more computational terms, we have a process that will consume A and produce B. Given the two assumptions A−∘B and A−∘C, there are two possible conclusions involving conjunctions of B and C. Using additive conjunction, written & , we may conclude A−∘(B & C) since from A we are capable of obtaining B and we are capable of obtaining C. With multiplicative conjunction, written ⊗, sharing is not allowed. However, we may obtain B and C from two separate A’s. This is written symbolically as (A ⊗ A)−∘(B ⊗ C). One way of describing the distinction is that B & C indicates a choice between B and C, while B ⊗ C reflects an ability to have both simultaneously.

The final step in deriving linear logic is to add two modal operators. These are a storage or reuse operator, ! , and a dual consumption operator ? , definable from ! using negation. Intuitively, the formula !A provides unlimited use of the resource A and ?B allows the unlimited consumption of B. Using a computational metaphor that we have found useful and faithful to the logic, we may read !A as, “the datum A is stored in the memory and may be referenced an unlimited number of times”. In deductive terms, if B follows from any number of assumptions of A, then B follows from the single assumption !A. A view of ! which suggests the translation of classical logic into linear logic is that while we do not have contraction and weakening as structural rules, we may apply contraction and weakening to formulas beginning with !. Since the basic framework remains linear, unbounded use is allowed only “locally”, at formulas specifically marked with ! or ?.

The first application of the resource-sensitive aspect of the logic was the development of a functional programming language implementation in which garbage collection was replaced by explicit duplication operations based on linear logic [Laf88]. Further studies have demonstrated connections with Petri nets [Asp87, GG89, MOM89, AFG90, GG90] and other models of concurrency [Laf90, AV90]. With regard to concurrency, there is a similarity between proof nets, the inherent model of computation associated with cut-elimination in multiplicative linear logic (cf [Gir87a, Gir87b, DR89, Laf90]), and connection graphs, which were designed to model connection machine computation [Baw86]. Other applications include optimization of copying in lazy functional programming language implementation [GH90] and analyzing the control structure of logic programs [Cer90, AP90]. A natural characterization of polynomial time computations can be given in a bounded version of linear logic [GSS90] obtained by limiting reuse to specified bounds, i.e., by bounding the number of references to each datum in memory. Informal introductions to linear logic may be found in [Gir90, Sce90].

We now summarize the main results of this paper (which were sketched in [LMSS90]), beginning with the smallest fragment considered. Multiplicative linear logic contains only linear implication, negation, and the multiplicative forms of conjunction and disjunction. Recall that these forms require the available resource to be partitioned rather than shared. We show that the decision problem for this fragment is in np. With unrestricted weakening added, we show that the multiplicative fragment is np-complete.

There are two natural fragments extending pure multiplicative linear logic, one with additive connectives and the other with the ! operator. We show that the first extension, with additive and multiplicative connectives but not !, is pspacecomplete. The proof, by reduction from classical quantified boolean formulas, involves encoding quantifier order using only commutative propositional connectives. We note here in passing that the fragment with only multiplicative connectives and the ! operator is at least as hard as the reachability problem for Petri nets (or, equivalently, commutative semi-Thue systems or vector addition systems). This follows from conservativity properties established in this paper and previous work relating linear logic and Petri nets. Although reachability is decidable [May81, Kos82], the best known lower bound is expspace [Lip76, MM82]. A likely upper bound on Petri net reachability is primitive recursive in the Ackermann function [McA84, Clo86]. We do not know if multiplicative linear logic with ! is decidable.

Finally, we show that provability in full propositional linear logic with additive and multiplicative connectives and modal storage operator is undecidable. It follows from this undecidability result that when propositional linear logic is extended with quantification over propositions, the resulting logic is also undecidable. (Provability is trivially recursively enumerable, since the proof system is effective.) Undecidability also holds for a restricted form called intuitionistic propositional linear logic. In addition, we establish the undecidability of a noncommutative variant of linear logic (even without additive connectives), a system that extends the calculus in [Lam58]; see [Gir89, Yet90].

Our undecidability proof uses a direct encoding of a form of alternating counter machines. Our “and-branching counter machines” resemble the alternating Turing machines of [CKS81]), but lack a basic operation to test for zero. The basic transitions of these machines may be axiomatized using the multiplicative and additive connectives, while the ! operator is needed to allow an instruction to be executed an arbitrary number of times. Additive connectives are used to encode and-branching, which is needed to simulate the zero tests of conventional counter machines. As for the other lower bounds, the bulk of the technical work lies in establishing that the encoding is faithful, i.e., each deduction in linear logic determines some computation. Faithfulness is demonstrated using a detailed examination of cut-elimination in linear logic [Gir87a]. This yields a version of the deduction theorem for linear logic and various conservativity results of independent interest.

A key insight is that searching for a proof of a certain special form for a given linear logic sequent corresponds directly to searching for an accepting computation in a particular machine model. A successful search is exactly an accepting computation.

For propositional linear logic without storage, membership in pspace is shown using a proof bound based on cut-elimination. pspace-hardness is demonstrated by a (log-space) construction of formulas that may be proved only by alternating between rules that simulate classical universal and existential propositional quantifiers. This construction demonstrates a surprising property of linear logic: the connectives are sufficient to express synchronization to the point of “sequentiality”. Undecidability of noncommutative linear logic is proved by encoding the word problem for semigroups. Unlike our other reductions, this does not require the additive connectives. Membership in np for multiplicative linear logic, with or without unrestricted weakening, is based on a polynomial bound on proof-size resulting from cut-elimination. With unrestricted weakening, we show np-completeness by reduction from the vertex cover problem [GJ79].

A logic that is superficially related to linear logic is propositional relevance logic, which is proved undecidable in [Urq84]. Like linear logic, relevance logic lacks weakening. However, relevance logic does have unrestricted contraction. In addition, relevance logic has a distributivity axiom, absent from linear logic. Without the distributivity axiom, relevance logic becomes decidable [Mey66]. The system with distributivity also lacks cut-free Gentzen-type formulation. See, for example, [Avr88]. Thus both the motivation and technical properties of linear logic are significantly different from relevance logic.

Multiplicative Additive Propositional Linear Logic is PSPACE-complete

In this chapter, we analyze the complexity of the fragment of propositional linear logic without the modal storage operator ! and its dual ?, but including all the remaining connectives and constants of linear logic.

We begin with some standard definitions. A deduction in propositional linear logic is a tree, usually presented with the root at the bottom, and the leaves at the top. Each branch of a deduction is a sequence of applications of the proof rules given in Appendix B, some of which, such as & , represent branching points in the deduction tree, some, such as � , which extend the length of a branch, and some, such as identity, which terminate a branch. The leaves embody the assumptions, and the root the conclusion. Such a structure is said to be a deduction of the conclusion from the assumptions. A proof in linear logic is a deduction with no assumptions. That is, each branch terminates with an application of identity, ⊤, or 1. One interesting feature of linear logic, as presented in Appendix B, is that negation is defined, and it is not a connective. In particular, the propositional literals are assumed to be given in pairs, one positive (written p_{i} for some i) and one negative (written p_{i}^{⊥}).

In this chapter we are concerned with the multiplicative-additive fragment of linear logic, which we abbreviate as mall. The logical symbols used in this fragment are multiplicative conjunction (⊗) and disjunction ( � ), additive conjunction (&) and disjunction (⊕), and the constants 0, 1, ⊤, and ⊥. mall formulas and sequents contain only these connectives and constants, in addition to the positive and negative literals. The proof rules of mall are all of the rules in the Appendix B that are associated with these connectives and constants. This logic has been studied by Girard [Gir87a] and Bellin [Bel90]. While provability for the classical propositional logic is co-NP-complete, we show below that provability for mall is pspacecomplete.

An important property of the sequent calculus formulation of mall is cutelimination. This property follows from the Theorem A.3 of Appendix A.

Theorem 2.1 Any sequent provable in mall is provable without the cut rule.

Proof. Since mall is a fragment of linear logic, we may use the cut-elimination procedure from Theorem A.3 to convert a mall proof to a cut-free proof in linear logic. By the subformula property (Theorem A.4), such a cut-free proof of a mall sequent contains only mall formulas. Since all the rules which apply to mall formulas are already in mall, any cut-free proof of a mall sequent must already be a mall proof.

Membership in pspace is straightforward, given cut elimination, but we include a short sketch to illustrate the importance of Theorem 2.1. The proof of pspacehardness is more technical. Proof search in the cut-free sequent calculus is crucial to the proof. The primitive step in proof search is a reduction, namely the application of an inference rule to transform a sequent matching the conclusion of the rule to the collection of sequents given by the corresponding premises of the rule. A reduction is the inverse of an inference rule, and drives conclusions to premises. Proof search is the process of constructing a cut-free proof in a bottom-up manner by nondeterministically applying reductions starting from the conclusion sequent.

2.1 Membership in PSPACE

Theorem 2.2 The provability in mall of a given sequent can be decided by a polynomial-space bounded Turing machine.

Proof. By Theorem 2.1, a provable mall sequent has a cut-free mall proof. In a cut-free mall proof, there are at most two premises to each rule, and each premise is strictly smaller than the consequent. Therefore, the depth of a cut-free mall proof tree is at most linear in the length of the final sequent of the proof. An alternating Turing machine [CKS81] may guess and check a cut-free proof in linear time, using OR-branching to nondeterministically guess a reduction in the cut-free proof, and AND-branching to generate and check the proofs of both premises of a two premise rule in parallel.

Membership in pspace can also be proved without reference to alternation. A nondeterministic Turing machine can be defined to generate and check a cut-free sequent proof in a depth-first manner. Given the linear bound on the depth of any cut-free proof with respect to the size of the conclusion sequent, the search stack need contain no more than a linear number of sequents. Since each sequent in a cut-free proof is no larger than the conclusion sequent, we get a quadratic bound on the stack size.

2.2 Informal Outline of PSPACE-hardness of MALL

Since there are a number of technical details to the proof of pspace-hardness, we will illustrate the key intuitions by means of an example; the details of the proof are given in Section 2.4.

The pspace-hardness of mall provability is demonstrated by a transformation from the validity problem for quantified Boolean formulas (QBF). A quantified Boolean formula has the (prenex) form Q_{m}X_{m} … Q_{1}X_{1}: M, where

1. each Q_{i} is either ∀ or ∃,

2. M is a quantifier-free Boolean matrix containing only the connectives ¬ and ∧, and Boolean variables.

A closed QBF contains no free variables. Our conventions in this section are that G and H range over quantified Boolean formulas; M and N range over quantifierfree Boolean formulas; U, V, X, Y, Z range over Boolean variables; and I ranges over truth value assignments. For expository convenience, we refer to quantifier-free Boolean formulas simply as Boolean formulas.

An assignment I for a set of Boolean variables {X_{1}, …, X_{n}} maps each X_{i} to a truth value from {T, F }. An assignment is represented by a sequence of Boolean variables and negated Boolean variables. For example, the assignment X_{1}, ¬X_{2}, X_{3} maps X_{1} to T, X_{2} to F, and X_{3} to T. The assignment I, X assigns T to X, but behaves like I, otherwise. If I is an assignment for the free variables in G, we use the standard notation I ⊧ G to indicate that G is valid under I, and write I |̸= G if I falsifies G. Note that

I ⊧ ∀X: G iff I, X ⊧ G and I, ¬X ⊧ G
I ⊧ ∃X: G iff I, X ⊧ G or I, ¬X ⊧ G

If G is a QBF and I is an assignment for the free variables in G, we say G is valid under I exactly if I ⊧ G. If G is a closed QBF, then G is said to be valid if it is valid under the empty assignment. The validity of a closed QBF G is represented as ⊧ G. The QBF validity problem is: Given a closed QBF G, is G valid?

We demonstrate the pspace-hardness of mall provability by defining a succinct encoding of a QBF as a mall sequent that is provable exactly when the given QBF is valid.

The transformation of the QBF validity problem to mall provability takes place in two steps:

• Given a quantifier-free Boolean formula M and an assignment I for the free variables in M, we show that there is a mall sequent encoding M and I which is provable exactly when M is valid under I. This essentially demonstrates that the process of evaluating Boolean functions can be represented by the process of cut-free proof search in the mall sequent calculus.

• Given a QBF G and an assignment I for the free variables in G, there exists a mall sequent encoding the quantifier prefix and the Boolean matrix of G so that the mall sequent is provable exactly when G is valid under I. The idea here is to simulate the Boolean quantifiers ∃ and ∀ by using the additive connectives ⊕ and &.

Two-sided vs. one-sided sequents. We use a formulation of mall with onesided sequents to simplify the proofs. In linear logic, a two-sided sequent A_{1}, …, A_{m} ⊢ B_{1}, …, B_{n} has the one-sided form ⊢ A_{1}^{⊥}, …, A_{m}^{⊥}, B_{1}, …, B_{n}. Thus, a formula A−∘B on the left of a two-sided sequent becomes A⊗B^{⊥} in a one-sided sequent. Similarly, the provable two-sided sequent A, A−∘B ⊢ B becomes ⊢ A^{⊥}, A ⊗ B^{⊥}, B. While one-sided sequents simplify the technical arguments considerably, the reader might gain further insight by rewriting parts of our encoding in a two-sided form.

2.2.1 Encoding Boolean Evaluation

The encoding of the Boolean connectives and quantifiers in mall is described here by means of an example. The full definition of the encoding appears in Section 2.3. The encoding from QBF validity to mall provability makes no use of the mall constants. Consider the valid QBF G given by

∀X_{2}∃X_{1}: ¬(¬X_{1} ∧ X_{2}) ∧ ¬(¬X_{2} ∧ X_{1}).

The matrix M of G is essentially a restatement of (X_{1} ⟺ X_{2}). Let H be the falsifiable formula ∃X_{1}∀X_{2}: M that is obtained from G by reversing the order of the quantifiers. It is crucial that the encodings of G and H in mall respect the ordering of quantifiers so that the encoding of G is provable but the encoding of H is not.

The encoding of the Boolean matrix describes the formula as a circuit with signals labeled by mall literals. Let the assignment I be encoded by a sequence of mall formulas ⟨I⟩, and [M]_{a} be the mall formula encoding M with output labeled by the literal a. Then I ⊧ M is encoded by the sequent

⊢ ⟨I⟩, [M]_{a}, a

whereas I |̸= M is encoded by

⊢ ⟨I⟩, [M]_{a}, a^{⊥}.

Since we are using one-sided sequents, we encode the assignment X_{1}, ¬X_{2} by x_{1}^{⊥}, x_{2}. The mall literals encoding the assignment are to be seen as the input signals to the encoding of the Boolean formula.

We first consider the Boolean connectives ¬ and ∧, then construct the full encoding of M. The encoding [¬X_{1}]_{a} of ¬X_{1} with output labeled a is the formula not(x_{1}, a). For literals x and y, the definition of not(x, y) is just the representation of the truth table for negation within mall, as shown below:

not(x, y) = (x ⊗ y) ⊕ (x^{⊥} ⊗ y^{⊥}).  (2.1)

not(x_{1}, a) is simply the linear negation of the formula

(x_{1}−∘a^{⊥})&(x_{1}^{⊥}−∘a)

which is more perspicuous in describing a as the Boolean negation of x_{1}. The sequent

⊢ x_{1}, not(x_{1}, a), a  (2.2)

encodes the situation where the input X_{1} is F, and asserts (correctly) that the output ¬X_{1} is T.

The sequent (2.2) is easily seen to have the mallproof

\underline{\overline{⊢ x_{1}, x_{1}^{⊥}}^{I}  \overline{⊢ a^{⊥}, a}^{I}}_{⊗}
⊢ x_{1}, (x_{1}^{⊥} ⊗ a^{⊥}), a
\overline{⊢ x_{1}, (x_{1} ⊗ a) ⊕ (x_{1}^{⊥} ⊗ a^{⊥}), a}^{⊕}

Similarly, the sequent (2.3) representing {X_{1} ← T } |̸= ¬X_{1} is also provable.

⊢ x_{1}^{⊥}, not(x_{1}, a), a^{⊥}.  (2.3)

On the other hand, the sequent

⊢ x_{1}^{⊥}, not(x_{1}, a), a  (2.4)

asserts (falsely) that {X_{1} ← T } ⊧ ¬X_{1}. To see why sequent (2.4) is not provable, we observe that mall is a refinement of classical logic in which no classically falsifiable sequents are provable. The sequent ⊢ x_{1}^{⊥}, not(x_{1}, a), a is falsified by assigning T to x_{1} and F to a, while interpreting ⊗ and & as classical conjunction and ⊕ and � as classical disjunction. A sequent is interpreted classically as the disjunction of the sequence of formulas that it contains.

The encoding for conjunction, [X ∧ Y]_{b} is given by and(x, y, b) as defined below.

and(x, y, b) = [ \begin{matrix}(x ⊗ y ⊗ b^{⊥}) & ⊕ \\ (x^{⊥} ⊗ y^{⊥} ⊗ b) & ⊕ \\ (x ⊗ y^{⊥} ⊗ b) & ⊕ \\ (x^{⊥} ⊗ y ⊗ b) \end{matrix} ]  (2.5)

Sequent (2.6) represents X, Y ⊧ (X ∧ Y):

⊢ x^{⊥}, y^{⊥}, and(x, y, b), b.  (2.6)

Sequent (2.6) has the proof

\underline{\overline{⊢ x^{⊥}, x}^{I}  \begin{matrix}\underline{\overline{⊢ y^{⊥}, y}^{I}  \overline{⊢ b^{⊥}, b}^{I}} & ⊗ \\ ⊢ y^{⊥}, (y ⊗ b^{⊥}), b \end{matrix}}_{⊗}
\underline{⊢ x^{⊥}, y^{⊥}, (x ⊗ y ⊗ b^{⊥}), b}_{⊕}
⊢ x^{⊥}, y^{⊥}, and(x, y, b), b

As with sequent (2.4), the mall sequent representing the false assertion ¬X, Y ⊧ (X ∧ Y) is given by

⊢ x, y^{⊥}, and(x, y, b), b

and is not provable since it can be falsified by the classical interpretation assigning F to x and b, and T to y.

The next step is to construct the encoding of the Boolean formula M given at the beginning of this section, from the encodings of the Boolean connectives. The formula M is thought of as a Boolean circuit with the distinctly labeled signals. The encoding [(¬X_{1} ∧ X_{2})]_{b} is given by the formula and(a, x_{2}, b) � not(x_{1}, a). Let implies(x, y, u, v, w) represent the formula

not(v, w) � and(u, y, v) � not(x, u),

then implies(x_{1}, x_{2}, a, b, c) is the encoding [¬(¬X_{1} ∧ X_{2})]_{c}. The literals a, b and c are the distinct literals labeling the output signals of the Boolean gates.

We now consider the problem that the input signals in M have a fanout greater than one. An almost correct encoding in mall of the Boolean formula M is given by the formula

and(c, f, g) � implies(x_{1}, x_{2}, a, b, c) � implies(x_{2}, x_{1}, d, e, f).

The validity of M under the assignment {X_{1} ← T, X_{2} ← T } would then be represented by

⊢ x_{1}^{⊥}, x_{2}^{⊥}, and(c, f, g) � implies(x_{1}, x_{2}, a, b, c) � implies(x_{2}, x_{1}, d, e, f), g. (2.7)

The following deduction represents one attempt to prove sequent (2.7).

\overline{⊢ g^{⊥}, g}^{I}

⋮ ; ⊢ x_{1}^{⊥}, x_{2}^{⊥}, implies(x_{1}, x_{2}, a, b, c), c  ⋮ ; ⊢ implies(x_{2}, x_{1}, d, e, f), f ⊗

⊢ x_{1}^{⊥}, x_{2}^{⊥}, (c ⊗ f), implies(x_{1}, x_{2}, a, b, c), implies(x_{2}, x_{1}, d, e, f) ⊗

⊢ x_{1}^{⊥}, x_{2}^{⊥}, (c ⊗ f ⊗ g^{⊥}), implies(x_{1}, x_{2}, a, b, c), implies(x_{2}, x_{1}, d, e, f), g ⊕

⊢ x_{1}^{⊥}, x_{2}^{⊥}, and(c, f, g), implies(x_{1}, x_{2}, a, b, c), implies(x_{2}, x_{1}, d, e, f), g

⊢ x_{1}^{⊥}, x_{2}^{⊥}, and(c, f, g) � implies(x_{1}, x_{2}, a, b, c) � implies(x_{2}, x_{1}, d, e, f), g �

Since mall lacks a rule of contraction, each of the assignment literals, x_{1}^{⊥} and x_{2}^{⊥}, can appear in only one premise of a ⊗ rule. As a result, one of the remaining subgoals in the above deduction lacks the required input literals. We therefore need to be able to explicitly duplicate the assignment literals in the sequent (2.7) to match the number of duplicate occurrences of X_{1} and X_{2} in M. The formula copy(x_{1}) defined as

(x_{1} ⊗ (x_{1}^{⊥} � x_{1}^{⊥})) ⊕ (x_{1}^{⊥} ⊗ (x_{1} � x_{1}))

serves to duplicate an instance of x_{1} or x_{1}^{⊥}. If M is now encoded as

and(c, f, g) � copy(x_{1}) � copy(x_{2}) � Γ_{1} � Γ_{2}

where Γ_{1} abbreviates implies(x_{1}, x_{2}, a, b, c), and Γ_{2} abbreviates implies(x_{2}, x_{1}, d, e, f), the desired deduction of (2.7) can then be constructed.

\overline{⊢ x_{1}, x_{1}^{⊥}}^{I}

\overline{⊢ x_{2}, x_{2}^{⊥}}^{I}  \underline{\overline{⊢ g, g^{⊥}}^{I}  \begin{matrix}\underline{⋮ ; ⊢ x_{1}^{⊥}, x_{2}^{⊥}, Γ_{1}, c  ⋮ ; ⊢ x_{1}^{⊥}, x_{2}^{⊥}, Γ_{2}, f} & ⊗ \\ ⊢ x_{1}^{⊥}, x_{1}^{⊥}, x_{2}^{⊥}, x_{2}^{⊥}, (c ⊗ f), Γ_{1}, Γ_{2} \end{matrix}}_{⊗} ; ⊢ x_{1}^{⊥}, x_{1}^{⊥}, x_{2}^{⊥}, x_{2}^{⊥}, (c ⊗ f ⊗ g^{⊥}), Γ_{1}, Γ_{2}, g ⊗

⊢ x_{1}^{⊥}, x_{1}^{⊥}, x_{2}^{⊥}, and(c, f, g), x_{2} ⊗ (x_{2}^{⊥} � x_{2}^{⊥}), Γ_{1}, Γ_{2}, g ⊗

⊢ x_{1}^{⊥}, x_{2}^{⊥}, and(c, f, g), x_{1} ⊗ (x_{1}^{⊥} � x_{1}^{⊥}), copy(x_{2}), Γ_{1}, Γ_{2}, g ⊕

⊢ x_{1}^{⊥}, x_{2}^{⊥}, and(c, f, g), copy(x_{1}), copy(x_{2}), Γ_{1}, Γ_{2}, g

⊢ x_{1}^{⊥}, x_{2}^{⊥}, and(c, f, g) � copy(x_{1}) � copy(x_{2}) � Γ_{1} � Γ_{2}, g

�

In summary, we have informally described the encoding in mall of the evaluation of Boolean formulas under an assignment. The connectives � , ⊗, and ⊕ were used to represent the truth tables of ¬ and ∧, and mall literals were used to represent the “signals” in the Boolean formula. The duplication of input signals forms a crucial part of the encoding since mall lacks a rule of contraction.

2.2.2 Encoding Boolean Quantification

Recall that G is the formula ∀X_{2}∃X_{1}: M, and H is the formula ∃X_{1}∀X_{2}: M, where M is ¬(¬X_{1} ∧X_{2})∧¬(¬X_{2} ∧X_{1}). Intuitively, it is useful to separate the encoding of the Boolean quantifier prefix as separately encoding the individual quantifiers and the dependencies between quantifiers. Given the above encoding for assignments and Boolean formulas, an almost correct way to encode Boolean quantifiers would be to encode ∃X_{1} as the formula (x_{1} ⊕ x_{1}^{⊥}), and ∀X_{2} as (x_{2}&x_{2}^{⊥}). The encoding of G would then be given by the sequent

⊢ (x_{2}&x_{2}^{⊥}), (x_{1} ⊕ x_{1}^{⊥}), [M]_{g}, g.

The formula (x_{1} ⊕ x_{1}^{⊥}) behaves like existential quantification in proof search since a nondeterministic choice can be made between

⋮ ; ⊢ x_{1}^{⊥}, Γ ; \overline{⊢ (x_{1} ⊕ x_{1}^{⊥}), Γ}^{⊕}  and  ⋮ ; ⊢ x_{1}, Γ ; \overline{⊢ (x_{1} ⊕ x_{1}^{⊥}), Γ}^{⊕}

according to the assignment (T or F, respectively) to X_{1} which makes ∃X_{1}: M valid. Similarly, the rule for reducing (x_{2}&x_{2}^{⊥}) in a proof behaves like universal quantification requiring proofs of both ⊢ x_{2}^{⊥}, Γ and ⊢ x_{2}, Γ.

\begin{matrix}\underline{⋮ ; ⊢ x_{2}^{⊥}, Γ  ⋮ ; ⊢ x_{2}, Γ} & & \\ ⊢ (x_{2}&x_{2}^{⊥}), Γ \end{matrix}

However, with this mapping of quantifiers, the mall encoding of G and H would be identical and provable, but H is not a valid QBF.

A correct encoding of ∃X_{1}∀X_{2}: M should ensure that if the encoding is provable in mall, then there is a proof in which the choice of a truth value for X_{1} is independent of whether X_{2} is T or F. The order of reductions below show how the choice of a truth value for ∃X_{1} in a proof of the mall encoding can depend on the quantifier ∀X_{2}.

\underline{⋮ ; ⊢ x_{1}, x_{2}, Γ ; \overline{⊢ (x_{1} ⊕ x_{1}^{⊥}), x_{2}, Γ}^{⊕}  ⋮ ; ⊢ x_{1}^{⊥}, x_{2}^{⊥}, Γ ; \overline{⊢ (x_{1} ⊕ x_{1}^{⊥}), x_{2}^{⊥}, Γ}^{⊕}}_{&} ; ⊢ (x_{1} ⊕ x_{1}^{⊥}), (x_{2}&x_{2}^{⊥}), Γ

In this ordering of the reductions, (x_{1} ⊕ x_{1}^{⊥}) is reduced differently on the x_{2} and x_{2}^{⊥} branches of the proof leading to distinct witnesses for X_{1} according to whether X_{2} is T or F. The solution to this quantifier order problem is to encode the quantifier dependencies in the mall formula so that if there is any proof, then there is some proof of the encoding in which (x_{1} ⊕ x_{1}^{⊥}) is reduced below (x_{2}&x_{2}^{⊥}), thus ensuring that the truth value of X_{1} has been chosen independently of the truth value for X_{2}. For this purpose, we introduce new mall atoms q_{0}, q_{1}, q_{2}, and encode ∃X_{1}∀X_{2}: M as

⊢ q_{2},
q_{2}^{⊥} ⊗ ((q_{1} � x_{1}) ⊕ (q_{1} � x_{1}^{⊥})),
q_{1}^{⊥} ⊗ ((q_{0} � x_{2})&(q_{0} � x_{2}^{⊥})),
q_{0}^{⊥} ⊗ [M]_{g}, g

The idea here is that the quantifier encoding for ∃X_{1} hides the “key” q_{1} that is needed to unlock the quantifier encoding for ∀X_{2}. If we now attempt to violate the quantifier dependencies, the following would be one possible deduction.

\begin{matrix}\underline{\underline{\overline{⊢ q_{2}, q_{2}^{⊥}}^{I}  \begin{matrix}? \\ ⊢ q_{1}^{⊥}, q_{1}, x_{1} \\ \overline{⊢ q_{1}^{⊥}, q_{1} � x_{1}} & � \\ \overline{⊢ q_{1}^{⊥}, ((q_{1} � x_{1}) ⊕ (q_{1} � x_{1}^{⊥}))} & ⊕ \end{matrix}}_{⊗} ; ⊢ q_{2}, q_{1}^{⊥}, q_{2}^{⊥} ⊗ ((q_{1} � x_{1}) ⊕ (q_{1} � x_{1}^{⊥})) ⋮ ; ⊢ (q_{0} � x_{2})&(q_{0} � x_{2}^{⊥}), q_{0}^{⊥} ⊗ [M]_{g}, g} & ⊗ \\ ⊢ q_{2}, q_{2}^{⊥} ⊗ ((q_{1} � x_{1}) ⊕ (q_{1} � x_{1}^{⊥})), q_{1}^{⊥} ⊗ ((q_{0} � x_{2})&(q_{0} � x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g \end{matrix}

In the above deduction, we are left with a subgoal of the form ⊢ q_{1}^{⊥}, q_{1}, x_{1}, and since x_{1} is not a constant, we cannot reduce this sequent to a mall axiom. (Recall that mall lacks an unrestricted weakening rule.) Other deductions attempting to violate the quantifier ordering also fail. On the other hand, the deduction which does respect the order of the quantifier encodings can be performed as shown below. The quantifier encoding for ∃X_{1} provides the key q_{1} for unlocking the quantifier encoding of ∀X_{2}.

\underline{\overline{⊢ q_{2}, q_{2}^{⊥}}^{I}  ⋮ ; ⊢ q_{1}, x_{1}, q_{1}^{⊥} ⊗ ((q_{0} � x_{2})&(q_{0} � x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g ; \overline{⊢ q_{1} � x_{1}, q_{1}^{⊥} ⊗ ((q_{0} � x_{2})&(q_{0} � x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g} ^{�} ; \overline{⊢ ((q_{1} � x_{1}) ⊕ (q_{1} � x_{1}^{⊥})), q_{1}^{⊥} ⊗ ((q_{0} � x_{2})&(q_{0} � x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g} ^{⊕}}_{⊗} ; ⊢ q_{2}, q_{2}^{⊥} ⊗ ((q_{1} � x_{1}) ⊕ (q_{1} � x_{1}^{⊥})), q_{1}^{⊥} ⊗ ((q_{0} � x_{2})&(q_{0} � x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g

The formal definition of the polynomial time encoding of QBF validity in terms of mall provability is given in Section 2.3. In Section 2.4, we demonstrate the correctness of the encoding.

2.3 Formal Definition of the Encoding

For our purpose, a Boolean formula is constructed from Boolean variables using the Boolean connectives ¬ and ∧. All quantified variables are assumed to occur in the matrix. V ar(M) is the set of variables occurring in the Boolean formula M. Overlined syntactic variables such as \overline{X} and \overline{Y} range over sets of Boolean variables.

The mall sequent encoding a QBF G is represented by σ(G). We need to be careful about keeping literals distinct. The annotation “a new” in the definition indicates that the literal a is a freshly chosen one that has not been used elsewhere in the encoding.

The sequent σ(G) consists of the encoding of the QBF [[G]]_{g}, where g labels the output signal, the key q_{n}, and the output value g. The definition of [[G]]_{g} constructs the quantifier encodings by induction on the length of the quantifier prefix. The definition of [M]_{g} is by induction on the structure of M, so that [N ∧P]_{g} is constructed by

• choosing the fresh labels a and b for the outputs of subformulas N and P, respectively

• defining the relation between a, b, and g by and(a, b, g)

• if needed, providing a copying formula for each Boolean variable common to both N and P

• and recursively constructing [N]_{a} and [P]_{b}

To be precise, we provide the following definition of the encoding.

Definition 2.3

σ(G) = ⊢ q_{n}, [[G]]_{g}, g  q_{n}, g new
[[(∀X_{i+1}: G)]]_{g} = (q_{i+1}^{⊥} ⊗ ((x_{i+1} � q_{i})&(x_{i+1}^{⊥} � q_{i}))), [[G]]_{g}  q_{i+1} new
[[(∃X_{i+1}: G)]]_{g} = (q_{i+1}^{⊥} ⊗ ((x_{i+1} � q_{i}) ⊕ (x_{i+1}^{⊥} � q_{i}))), [[G]]_{g} q_{i+1} new
[[M]]_{g} = (q_{0}^{⊥} ⊗ [M]_{g})  q_{0} new
[X]_{g} = (x^{⊥} ⊗ g) ⊕ (x ⊗ g^{⊥})
[¬N]_{g} = not(a, g) � [N]_{a}  a new

[N ∧ P]_{g} = \{ \begin{matrix}and(a, b, g) & � \\ copyall(V ar(N) ∩ V ar(P)) & � \\ [N]_{a} & � \\ [P]_{b} \end{matrix}  a, b new; V ar(N) ∩ V ar(P) ≠ ∅

[N ∧ P]_{g} = and(a, b, g) � [N]_{a} � [P]_{b}  a, b new; V ar(N) ∩ V ar(P) = ∅
copyall(\overline{X}) = �_{X_{i}∈\overline{X}}copy(x_{i})

Note that the sequent σ(G) contains no mall constants. The complexity of computing σ(G) is at most quadratic in the size of G since the encoding function is defined inductively over the structure of the formula, and the intersection operation can be performed in linear time with a bit-vector representation of sets, where the length of each bit-vector is the number of distinct Boolean variables occurring in G. The cost of constructing the copy formulas at each step in the recursion is also linear in the size of G. The cost of each not and and formula is fixed with respect to the representation of the literals, and the literals can be represented with a cost that is logarithmic in the size of G.

The encoding may be computed in log-space, although the algorithm described above uses more than log-space, because of the work space required to save the set of variables that must be copied when encoding a conjunction. The encoding algorithm could be modified to make a number of passes over the input to determine the number of occurrences of each variable and generate the required number of copy formulas. Each pass would use only log-space, and the remainder of the algorithm may be performed in log-space.

2.4 Proof of PSPACE-hardness of MALL

The main theorem is that for any closed QBF G, G is valid if and only if σ(G) is a provable mall sequent. The first set of lemmas demonstrates that the encoding of Boolean formulas works correctly. The second set of lemmas demonstrates that the Boolean quantifiers have been correctly encoded.

If I is a truth value assignment for the Boolean variables X_{1}, …, X_{n}, then I is encoded as ⟨I⟩, where

⟨I⟩ = ⟨X_{1}⟩_{I}, …, ⟨X_{n}⟩_{I}
⟨X_{i}⟩_{I} = \{ \begin{matrix}x_{i}^{⊥} & if I(X_{i}) = T \\ x_{i}, otherwise \end{matrix}

If I is an assignment for a set of variables \overline{Y}, and \overline{X} ⊆ \overline{Y}, then I/\overline{X} is the assignment I restricted to the subset \overline{X}, and by abuse of notation I/M is I/V ar(M). The following lemma is stated without proof.

Lemma 2.4 Given sets of variables \overline{X} and \overline{Y}, and an assignment I for \overline{X} ∪ \overline{Y}, there is a deduction of the sequent ⊢ ⟨I⟩, copyall(\overline{X} ∩ \overline{Y}), Γ from the sequent ⊢ ⟨I/\overline{X}⟩, ⟨I/\overline{Y} ⟩, Γ.

Lemma 2.5 Let M be a Boolean formula and I an assignment for the variables in M, then

1. if I ⊧ M then ⊢ ⟨I⟩, [M]_{g}, g

2. if I |̸= M then ⊢ ⟨I⟩, [M]_{g}, g^{⊥}

Proof. By induction on the structure of M, as follows. The cases in the proof correspond closely to those in the definition of [M]_{g}.

Base case: M ≡ X. Suppose I(X) = T, then I ⊧ M and ⟨I⟩ = x^{⊥}. The following proof can then be constructed, expanding the definition of [M]_{g}

\underline{\overline{⊢ x^{⊥}, x}^{I}  \overline{⊢ g^{⊥}, g}^{I}}_{⊗}
⊢ x^{⊥}, (x ⊗ g^{⊥}), g
\overline{⊢ x^{⊥}, (x^{⊥} ⊗ g) ⊕ (x ⊗ g^{⊥}), g}^{⊕}

The case when I(X) = F is similarly straightforward.

Induction step: There are a number of cases here corresponding to the definition of [M]_{g}. We consider a typical case and leave the remaining ones to the reader.

Let M ≡ N ∧ P, and suppose that V ar(N) ∩ V ar(P) ≠ ∅. Consider the case when I/N ⊧ N and I/P |̸= P, so that I |̸= N ∧ P. Expanding [M]_{g}, and(a, b, g), and using Lemma 2.4, the following deduction can be constructed.

\underline{\overline{⊢ g, g^{⊥}}^{I}  \begin{matrix}\underline{⋮ ; ⊢ ⟨I/N⟩, [N]_{a}, a ⋮ ; ⊢ ⟨I/P ⟩, [P]_{b}, b^{⊥}} & ⊗ \\ ⊢ ⟨I/N⟩, ⟨I/P ⟩, (a ⊗ b^{⊥}), [N]_{a}, [P]_{b} \end{matrix}}_{⊗}
\underline{⊢ ⟨I/N⟩, ⟨I/P ⟩, (a ⊗ b^{⊥} ⊗ g), [N]_{a}, [P]_{b}, g^{⊥}}_{⊕}
\underline{⊢ ⟨I/N⟩, ⟨I/P ⟩, and(a, b, g), [N]_{a}, [P]_{b}, g^{⊥}}
⋮

⊢ ⟨I⟩, and(a, b, g), copyall(V ar(N) ∩ V ar(P)), [N]_{a}, [P]_{b}, g^{⊥}

⊢ ⟨I⟩, and(a, b, g) � copyall(V ar(N) ∩ V ar(P)) � [N]_{a} � [P]_{b}, g^{⊥} �

Applying the induction hypothesis to I/N, N, and a, and to I/P, P, and b, we can establish that the remaining subgoals of the deduction are provable.

The remaining subcases in the evaluation of N ∧ P are similar, as are the remaining cases in the induction argument.

The next step is to establish the converse of Lemma 2.5. The classical interpretation of the mall connectives may be used to give a relatively easy proof. In the classical interpretation, truth values, T and F, are assigned to the mall atoms, A^{⊥} is read as classical negation, A ⊗ B and A&B are read as classical conjunction, and A � B and A ⊕ B are read as classical disjunction. A sequent is interpreted as the classical disjunction of the formulas contained in it.

Lemma 2.6 If ⊢ Γ is a provable mall sequent, then for any assignment of truth values to the atoms in Γ, there exists a formula A in the sequence Γ such that A is true under the classical interpretation.

Proof. The proof is by a straightforward induction on cut-free mall proofs. Clearly, for axioms ⊢ x, x^{⊥}, one of x or x^{⊥} must evaluate to T in a given truth assignment. In the induction case, suppose that the last step in the proof of Γ is a ⊗-rule of the form

\begin{matrix}\underline{⋮ ; ⊢ B, Γ_{1}  ⋮ ; ⊢ C, Γ_{2}} & ⊗ \\ ⊢ (B ⊗ C), Γ_{1}, Γ_{2} \end{matrix}

By the induction hypothesis, the sequence B, Γ_{1} contains a formula A_{1}, and the sequence C, Γ_{2} contains a formula A_{2}, and both A_{1} and A_{2} are true. If A_{1} is different from B, then A_{1} occurs in the conclusion sequent yielding the required A, and similarly, when A_{2} is different from C. Otherwise, the formula (B ⊗ C) is (A_{1} ⊗ A_{2}) and is hence true under the classical interpretation of ⊗ as conjunction. The induction arguments corresponding to the other connectives are similar.

The main intuition behind Lemma 2.7 is that by appropriately assigning truth values to the literals in ⟨I⟩ and [M]_{g}, it is possible to mimic the evaluation of the Boolean formula M under I. Due to our use of one-sided sequents and the form of our encoding, there is exactly one truth value falsifying each formula in ⟨I⟩ and [M]_{g}. This assignment turns out be the appropriate one, i.e., the value of g under this assignment is T exactly when I ⊧ M. For example, if I is {X ← F } and M is ¬X, then ⟨I⟩ is x^{⊥} and [M]_{g} is (x ⊗ g) ⊕ (x^{⊥} ⊗ g^{⊥}). The only falsifying assignment here is {x ← F, g ← T }.

Lemma 2.7 Let M be a Boolean formula and I be an assignment for the variables in M. There exists an assignment K of truth values to the atoms in ⟨I⟩ and [M]_{g} such that for every formula A in the sequence ⟨I⟩, [M]_{g}, assignment K falsifies A under the classical interpretation, and K(g) = T iff I ⊧ M.

Proof. The proof is by induction on the construction of [M]_{g}. Note that the induction is parametric in I and g (I and g are universally quantified in the induction hypothesis), so that when M ≡ (N ∧ P), the induction hypothesis on N has I/N replacing I and a replacing g, where a labels the output of N.

Base case: M ≡ X. Then [M]_{g} = (x^{⊥} ⊗ g) ⊕ (x ⊗ g^{⊥}). If I ⊧ X, then I(X) = T and ⟨I⟩ = x^{⊥}, and ⟨I⟩ is falsified if K assigns T to x. [M]_{g} is falsified if K assigns T to g, and the second part of the conclusion, K(g) = T also follows. If I |̸= X, then I(X) = F. Let K assign F to x and F to g to falsify both ⟨I⟩ and [M]_{g}. Then K(g) = F as required.

Induction step: Observe first that the formula copy(x) defined as (x⊗(x^{⊥} � x^{⊥}))⊕ (x^{⊥} ⊗ (x � x)) is classically false.

When M ≡ ¬N, the encoding [M]_{g} is not(a, g), [N]_{a}. By the induction hypothesis, we have an assignment K_{1} falsifying ⟨I⟩, [N]_{a} such that K_{1}(a) = T iff I ⊧ N. Suppose K_{1}(a) = T, and hence I ⊧ N. The formula not(a, g) is (a ⊗ g) ⊕ (a^{⊥} ⊗ g^{⊥}). Let K be K_{1}{g ← F }. Since g does not occur in ⟨I⟩ or [N]_{a}, K agrees with K_{1} on ⟨I⟩, [N]_{a}. The assignment K also falsifies not(a, g), thus falsifying ⟨I⟩, [M]_{g}. Note that K(g) = F as required, since I |̸= M.

If K_{1}(a) = F, then I |̸= N. Letting K be K_{1}{g ← T } falsifies ⟨I⟩, [M]_{g}.

When M ≡ (N ∧P), then by the induction hypotheses for N and P, there exists

1. K_{1} falsifying ⟨I/N⟩, [N]_{a} such that K_{1}(a) = T iff I/N ⊧ N, and

2. K_{2} falsifying ⟨I/P ⟩, [P]_{b} such that K_{2}(a) = T iff I/P ⊧ P

The encoding ⟨I⟩ is a sequence of literals such that no two distinct literals in ⟨I⟩ share a common atom. Since ⟨I/N⟩ and ⟨I/P ⟩ are subsets of ⟨I⟩, there is no literal x such that x is in ⟨I/N⟩ and x^{⊥} is in ⟨I/P ⟩. Formulas [N]_{a} and [P]_{b} have no atoms in common outside of those in ⟨I⟩. Then the union of the assignments K_{1} ∪ K_{2}, is still an assignment, i.e., it assigns a unique truth value to each atom in ⟨I⟩, [N]_{a}, [P]_{b}.

Suppose that K_{1}(a) = T, and hence I/N ⊧ N, and K_{2}(b) = F, so that I/P |̸= P. Let K be (K_{1} ∪ K_{2}){g ← F }. Note that g does not occur in ⟨I⟩, [N]_{a} or [P]_{b} so that K agrees with K_{1} on [N]_{a} and with K_{2} on [P]_{b}. Each disjunct in and(a, b, g) expanded as

(a ⊗ b ⊗ g^{⊥}) ⊕
(a^{⊥} ⊗ b^{⊥} ⊗ g) ⊕
(a ⊗ b^{⊥} ⊗ g) ⊕
(a^{⊥} ⊗ b ⊗ g)

is falsified by K. As already observed, the copy formulas are all classically false, and thus K falsifies ⟨I⟩, [M]_{g}. Since in this case, I |̸= N ∧ P, the second part of the conclusion is also satisfied.

The remaining cases are similar.

Lemma 2.8 If I is an assignment for the variables in a given Boolean formula M, then

1. if ⊢ ⟨I⟩, [M]_{g}, g is provable, I ⊧ M

2. if ⊢ ⟨I⟩, [M]_{g}, g^{⊥} is provable, I |̸= M.

Proof. By Lemma 2.6, we know that if ⊢ ⟨I⟩, [M]_{g}, g is provable, then no assignment can simultaneously falsify ⟨I⟩, [M]_{g}, and g under the classical interpretation.

By Lemma 2.7, we can find an assignment K which falsifies ⟨I⟩ and [M]_{g} such that K(g) = T iff I ⊧ M. Since K cannot also falsify g, K(g) = T and hence I ⊧ M.

Similarly, when ⊢ ⟨I⟩, [M]_{g}, g^{⊥} is provable, we can, by Lemmas 2.7 and 2.6, find an assignment K such that K(g) = F and as a consequence, I |̸= M.

Lemma 2.9 ⊢ ⟨I⟩, [M]_{g}, g is provable iff I ⊧ M.

Proof. Follows immediately from Lemmas 2.5 and 2.8.

So far, we have demonstrated the correctness of the encoding of the Boolean matrix of a given quantified Boolean formula. The remainder of the proof deals with the encoding of Boolean quantifiers. The next lemma states the crucial reason why the mall encoding of quantifiers is faithful to the quantifier orderings. As observed in Section 2.2.2, the goal is to ensure that in any successful proof search, the ith quantifier encoding is reduced after, i.e, above, the reduction of the (i + 1)st quantifier encoding in any cut-free proof. To achieve this, we need to argue that the key q_{i} needed to unlock the ith quantifier encoding is only made available when the (i + 1)st quantifier encoding has been reduced. In order for the ith quantifier encoding, which has the form q_{i}^{⊥} ⊗ U_{i}, to be reduced before the (i + 1)st quantifier encoding, a subgoal of the form ⊢ q_{i}^{⊥}, Γ would have to be provable. The only occurrences of q_{i} are in the subformula U_{i+1} given by (q_{i} � x_{i+1}) ∘ (q_{i} � x_{i+1}^{⊥}), where ∘ may be either ⊕ or &. If U_{i+1} occurs in Γ, then the only occurrences of q_{i} in Γ are as immediate arguments to a � . By exploiting the absence of an unrestricted weakening rule in mall, it can be shown that in the absence of constants, ⊢ q_{i}^{⊥}, Γ is not provable when all of the occurrences of q_{i} in Γ appear as immediate arguments to � . Therefore, regardless of whether U_{i+1} occurs in Γ, the sequent ⊢ q_{i}^{⊥}, Γ would not be provable, thus making it impossible to reduce the ith quantifier encoding below the (i + 1)st quantifier encoding in a cut-free proof.

Lemma 2.10 If q is a positive or negative literal and the sequent ⊢ q, Γ contains no constants, then ⊢ q, Γ is provable only if either Γ ≡ q^{⊥} or Γ contains at least one occurrence of a subformula either of the form q^{⊥} ∘ A, or the form A ∘ q^{⊥}, where ∘ may be either ⊕, &, or ⊗.

Proof. We fix ∘ to be either ⊕, &, or ⊗ for this proof. The proof is by induction on cut-free mall proofs of ⊢ q, Γ. In the base case, for a cut-free proof of depth 0, the sequent ⊢ q, Γ must be a mall axiom, and Γ ≡ q^{⊥} holds.

In the induction step, when in the given cut-free proof of ⊢ q, Γ, the conclusion sequent is derived by an application of either a ⊗, & or a ⊕ rule, then at least one premise must be of the form ⊢ q, Δ. We know by the induction hypothesis for the proof of ⊢ q, Δ, either Δ = q^{⊥} or Δ either contains a subformula of the form q^{⊥} ∘ A, or the form A ∘ q^{⊥}. In either case, Γ contains one of the forms, q^{⊥} ∘ A or A ∘ q^{⊥}.

If in the cut-free proof of ⊢ q, Γ, the conclusion sequent is derived by an application of the � rule, the premise sequent must be of the form ⊢ q, Δ, where Δ is not a single formula, Then by the induction hypothesis on the proof of ⊢ q, Δ, the sequence Δ must contain one of the forms, q^{⊥} ∘ A or A ∘ q^{⊥}. Since every subformula of Δ is a subformula of Γ as well, Γ must also contain one of the forms q^{⊥} ∘ A or A ∘ q^{⊥}.

The following lemma demonstrates the correctness of the mall encoding of Boolean quantifiers. Each Q_{i} in the statement below is either ∀ or ∃.

Lemma 2.11 (Main Induction) Let M be a Boolean formula in the variables X_{1}, …, X_{n}, then for any m, 0 ≤ m ≤ n, and assignment I for X_{m+1}, …, X_{n}, the relation I ⊧ Q_{m}X_{m} … Q_{1}X_{1}: M holds iff the sequent ⊢ q_{m}, ⟨I⟩, [[Q_{m}X_{m} … Q_{1}X_{1}: M]]_{g}, g is provable in mall.

Proof. The proof is by induction on m between 0 and n. Note that I is universally quantified in the induction hypothesis.

Base case ⇒: Here m = 0. Then [[M]]_{g} ≡ q_{0}^{⊥} ⊗[M]_{g}, and we can easily construct the following deduction of the required conclusion ⊢ q_{0}, ⟨I_{0}⟩, [[M]]_{g}, g.

\begin{matrix}\underline{\overline{⊢ q_{0}, q_{0}^{⊥}}^{I}  ⋮ ; ⊢ ⟨I⟩, [M]_{g}, g} & ⊗ \\ ⊢ ⟨I⟩, q_{0}, q_{0}^{⊥} ⊗ [M]_{g}, g \end{matrix}

The proof of the remaining subgoal ⊢ ⟨I⟩, [G]_{g}, g, follows from Lemma 2.5.

Base case ⇐: The deduction shown above is the only possible one in a cut-free proof of ⊢ ⟨I⟩, q_{0}, q_{0}^{⊥} ⊗ [M]_{g}, g since q_{0}^{⊥} ⊗ [G] is the only compound formula in the conclusion. So if ⊢ ⟨I⟩, q_{0}, q_{0}^{⊥} ⊗ [M]_{g}, g is provable, by Theorem 2.1, it must have a cut-free proof containing a proof of ⊢ ⟨I⟩, [M]_{g}, g. By Lemma 2.8, we get I ⊧ M.

Induction step ⇒: Assume 0 < m ≤ n. Let G abbreviate Q_{m−1}X_{m−1} … Q_{1}X_{1}: M. We must prove the lemma for Q_{m}X_{m}G. If Q_{m} ≡ ∃, then

[[Q_{m}X_{m}: G]]_{g} = (q_{m}^{⊥} ⊗ ((x_{m} � q_{m−1}) ⊕ (x_{m}^{⊥} � q_{m−1}))), [[G]]_{g}

If I ⊧ ∃X_{m}: G, then either I, X_{m} ⊧ G or I, ¬X_{m} ⊧ G. In the former case, the following deduction of the required conclusion can be constructed.

\underline{\overline{⊢ q_{m}, q_{m}^{⊥}}^{I}  ⋮ ; ⊢ ⟨I⟩, x_{m}^{⊥}, q_{m−1}, [[G]]_{g}, g ; \overline{⊢ ⟨I⟩, ((x_{m} � q_{m−1}) ⊕ (x_{m}^{⊥} � q_{m−1})), [[G]]_{g}, g} ^{⊕}}_{⊗} ; ⊢ ⟨I⟩, q_{m}, (q_{m}^{⊥} ⊗ ((x_{m} � q_{m−1}) ⊕ (x_{m}^{⊥} � q_{m−1}))), [[G]]_{g}, g

Since ⟨I, X_{m}⟩ = ⟨I⟩, x_{m}^{⊥}, the induction hypothesis can be applied to show that the remaining subgoal of the above deduction is provable.

When I, ¬X_{m} ⊧ G, the proof construction only differs from the above one on the ⊕ rule corresponding to the quantifier encoding.

If Q_{m} ≡ ∀, then

[[∀X_{m}: G]]_{g} = (q_{m}^{⊥} ⊗ ((x_{m} � q_{m−1})&(x_{m}^{⊥} � q_{m−1}))), [[G]]_{g}

Since I ⊧ ∀X_{m}: G, it follows that I, X ⊧ G and I, ¬X ⊧ G. The following deduction can be constructed.

\underline{\overline{⊢ q_{m}, q_{m}^{⊥}}^{I}  \begin{matrix}\underline{⋮ ; ⊢ ⟨I⟩, x_{m}, q_{m−1}, [[G]]_{g}, g  ⋮ ; ⊢ ⟨I⟩, x_{m}^{⊥}, q_{m−1}, [[G]]_{g}, g} & & \\ ⊢ ⟨I⟩, ((x_{m} � q_{m−1})&(x_{m}^{⊥} � q_{m−1})), [[G]]_{g}, g \end{matrix}}_{⊗} ; ⊢ ⟨I⟩, q_{m}, (q_{m}^{⊥} ⊗ ((x_{m} � q_{m−1})&(x_{m}^{⊥} � q_{m−1})), [[G]]_{g}, g

Since ⟨I, X_{m}⟩ is ⟨I⟩, x_{m}^{⊥} and ⟨I, ¬X_{m}⟩ is ⟨I⟩, x_{m}, the two remaining subgoals in the deduction are provable by the induction hypotheses.

Induction step ⇐: This is the critical step in the proof. We are given that m > 0 and that the conclusion sequent ⊢ q_{m}, ⟨I⟩, [[Q_{m}X_{m} … Q_{1}X_{1}: M]]_{g}, g is provable. Theorem 2.1 can be applied to construct a cut-free proof of ⊢ q_{m}, ⟨I⟩, [[Q_{m}X_{m} … Q_{1}X_{1}: M]]_{g}, g. We show that this cut-free proof respects the quantifier ordering, i.e., the reduction of the encoding of Q_{m}X_{m} occurs below any other step in the proof.

It is easy to see that every formula in the multiset [[Q_{m}X_{m} … Q_{1}X_{1}: M]]_{g} is of the form q_{i}^{⊥} ⊗A_{i}, for 0 ≤ i ≤ m, with A_{0} ≡ [M]_{g}, and A_{j+1} ≡ ((x_{j+1} � q_{j})∘(x_{j+1}^{⊥} � q_{j})). The connective written as ∘ can be either & or ⊕. The formulas q_{i}^{⊥} ⊗A_{i} are the only compound formulas in the conclusion sequent ⊢ q_{m}, ⟨I⟩, [[Q_{m}X_{m} … Q_{1}X_{1}: M]]_{g}, g. From the mall rules, it is clear that the only applicable reduction in a cut-free proof search would be an application of the ⊗-rule. Hence for some k, we can partition the formulas other than q_{k}^{⊥} ⊗ A_{k} in the conclusion sequent into Γ and Δ to get a deduction of the conclusion sequent of the following form.

\begin{matrix}\underline{⋮ ; ⊢ Γ, q_{k}^{⊥}  ⋮ ; ⊢ A_{k}, Δ} & ⊗ \\ ⊢ Γ, (q_{k}^{⊥} ⊗ A_{k}), Δ \end{matrix}

Suppose for the sake of deriving a contradiction that k < m. Recall that there are no constants in the encoding. The formula q_{k+1}^{⊥} ⊗ A_{k+1} must either occur in Γ or Δ, and definitely not in both. Since the only occurrences of q_{k} are within A_{k+1}, by Lemma 2.10, if q_{k+1}^{⊥} ⊗ A_{k+1} occurs in Δ, then we cannot complete the proof ⊢ q_{k}, Γ. Thus we assume q_{k+1}^{⊥} ⊗ A_{k+1} occurs in Γ. It is easy to see by inspection of the form of A_{k+1} that the only occurrences of q_{k} in A_{k+1} have the form q_{k} ∘ B or the form B ∘ q_{k}, where ∘ is either ⊕, &, or ⊗. Therefore, again by Lemma 2.10, ⊢ q_{k}^{⊥}, Γ is not provable.

Thus it follows that k ≮ m.

When k = m, we can apply Lemma 2.10 to infer that Γ ≡ q_{m}, since otherwise, Γ would not contain any occurrences of q_{m} as immediate arguments to ⊗, & or ⊕. If Q_{m} ≡ ∃, this yields the deduction

\begin{matrix}\underline{\overline{⊢ q_{m}, q_{m}^{⊥}}^{I}  ⋮ ; ⊢ ⟨I⟩, ((x_{m} � q_{m−1}) ⊕ (x_{m}^{⊥} � q_{m−1})), [[Q_{m−1}X_{m−1} … Q_{0}X_{0}: M]]_{g}, g} & ⊗ \\ ⊢ ⟨I⟩, q_{m}, (q_{m}^{⊥} ⊗ ((x_{m} � q_{m−1}) ⊕ (x_{m}^{⊥} � q_{m−1})), [[Q_{m−1}X_{m−1} … Q_{0}X_{0}: M]]_{g}, g \end{matrix}

For the same reason as before, the remaining subgoal cannot be reduced by applying the ⊗-rule to a formula q_{i}^{⊥}⊗A_{i} since all of the occurrences of q_{i} remain as immediate arguments to � . The only possible reduction then is to “unwind” the quantifier encoding for Q_{m}X_{m} as in the (⇐) direction of the proof until q_{m−1} is introduced as a sequent formula. If the left ⊕ reduction is applied in the given cut-free proof, we have

⋮
⊢ ⟨I⟩, x_{m}, q_{m−1}, [[Q_{m−1}X_{m−1} … Q_{0}X_{0}: M]]_{g}, g
\overline{⊢ ⟨I⟩, (x_{m} � q_{m−1}), [[Q_{m−1}X_{m−1} … Q_{0}X_{0}: M]]_{g}, g} ^{�}
\overline{⊢ ⟨I⟩, ((x_{m} � q_{m−1}) ⊕ (x_{m}^{⊥} � q_{m−1})), [[Q_{m−1}X_{m−1} … Q_{0}X_{0}: M]]_{g}, g} ^{⊕}

Then by the induction hypothesis applied to the proof of the sequent

⊢ ⟨I⟩, x_{m}, q_{m−1}, [[Q_{m−1}X_{m−1} … Q_{0}X_{0}: M]]_{g}, g

we get I, ¬X_{m} ⊧ Q_{m−1}X_{m−1} … Q_{0}X_{0}: M, and hence I ⊧ ∃X_{m}Q_{m−1}X_{m−1} … Q_{0}X_{0}: M.

The argument is similar when the right ⊕ reduction is applied in the given cut-free proof.

The proof when Q_{m} ≡ ∀ is also similar.

When m = n in Lemma 2.11, it follows that a closed QBF G is valid iff σ(G) is provable in mall. Since σ is a log-space encoding of a given QBF, the final result below follows immediately from Theorems 2.11 and 2.2.

Theorem 2.12 mall provability is pspace-complete.

With two-sided sequents, the intuitionistic fragment of mall constrains the right-hand side of the sequent to contain at most one formula. A two-sided reformulation of the above proof could be carried out entirely within the intuitionistic fragment of mall, showing that intuitionistic mall is also pspace-complete.

Propositional Linear Logic is Undecidable

In the previous chapter, the decision problem for mall was shown to be pspacecomplete. We now show that if nonlogical (mall) axioms are added to mall, the decision problem becomes recursively unsolvable. We also show that nonlogical mall axioms may be encoded in full propositional linear logic without nonlogical axioms, and thus we have the result that full propositional linear logic is undecidable.

The proof of undecidability consists of a reduction from the halting problem for a form of counter machine to a decision problem in linear logic. In more detail, we begin by extending propositional linear logic with theories whose (nonlogical) axioms may be used any number of times in a proof. We then describe a form of and-branching two-counter machine with an undecidable halting problem and show how to encode these machines in propositional linear logic with theories. Since the axioms of our theories must have a special form, we are able to show the faithfulness of this encoding using a natural form of cut-elimination in the presence of nonlogical axioms. To illustrate the encoding of two-counter machines, we present an example simulation of a simple computation in Section 3.6. On first reading, the reader may wish to jump ahead to that section since it demonstrates the basic mechanism used in the undecidability proof. Also, the crucial cut-standardization step used in this section relies heavily on the cut-elimination procedure for linear logic without nonlogical axioms, first sketched by Girard in [Gir87a]. We give a very explicit proof of cut-elimination for full propositional linear logic in Appendix A, which some readers may find helpful to skim before continuing.

The key to our encoding of an undecidable problem in linear logic is the combination of three powerful mechanisms: resource accumulation, arbitrary reuse, and and-branching. In linear logic, ⊢ A, A is very different from ⊢ A, and this allows us to represent counters in unary. Indefinitely reusable formulas such as ?(B−∘C), (or axioms of the form ⊢ B^{⊥}, C) may be used to implement machine instructions. Note that the ? operator is used here to indicate a reusable resource, since we are working with one-sided sequents. If we were to express an axiom as a formula on the left-hand side of the ⊢ in a two-sided presentation of linear logic, we would use ! to express the unlimited potential for reuse of instructions.

The operator & may be used to test a conjunction of properties of the simulated machine, such as whether a counter is zero, and if the rest of the computation can continue normally. Together this machinery is enough to encode recursively unsolvable problems in linear sequents.

3.1 Overview

• We define linear logic theories, and prove a cut-standardization theorem for linear logic augmented with theories in Lemma 3.1.

• We prove theories are sound and faithful to a pure linear logic translation in Lemmas 3.3 and 3.2.

• We describe and-branching two counter machines, and note that their halting problem is unsolvable by reduction from standard two counter machines in Lemma 3.4.

• We demonstrate an encoding of our automata into linear logic theories, and prove that the encoding is sound and faithful in Lemmas 3.5 and 3.6.

• We present an example computation, showing the correspondence between the automaton and the (standardized) linear logic proof.

• We combine these lemmas to obtain our main result in Theorem 3.7.

3.2 Linear Logic Augmented With Theories

Essentially, a theory is a set of nonlogical axioms (sequents) that may occur as leaves of a proof tree. The use of theories described here is an extension of earlier work on multiplicative theories [GG89, MOM89].

We define a positive literal to be one of the given propositional symbols p_{i}. A negative literal is one of the p_{i}^{⊥} symbols. An atomic formula is any positive or negative literal.

For the theories of interest here, an axiom may be any linear logic sequent of the form ⊢ C, p_{i_{1}}^{⊥}, p_{i_{2}}^{⊥}, ..., p_{i_{n}}^{⊥}, where C is a mall formula (a linear logic formula without ! or ?) and the remainder of the sequent is made up of negative literals. For example, the sequents ⊢ p_{1}, p_{2}^{⊥}, ⊢ (p_{1} ⊗ p_{2}), p_{2}^{⊥}, ⊢ (p_{1} � p_{1}), and ⊢ p_{1}^{⊥}, p_{2}^{⊥} may all be axioms.

However, ⊢ p_{1}, p_{1} and ⊢ (p_{1} ⊗ p_{2}), p_{3} may not be axioms. We use this restriction on axioms to achieve strict control over the shape of a proof, as described in Lemma 3.1. Some of this control is lost if the definition of theory is generalized, although for some applications the weaker available results would be sufficient.

Any finite set of axioms is a theory. We consider only finite theories so that theories may be encoded as formulas of linear logic. For any theory T, we say that a sequent ⊢ Γ is provable in T exactly when we are able to derive ⊢ Γ using the standard set of linear logic proof rules, in combination with axioms from T. Thus each axiom of T is treated as a reusable sequent which may occur as a leaf of a proof tree. For notational convenience, in the case that the axiom ⊢ Γ occurs in the theory T, we will write

\overline{⊢ Γ}^{T}

A directed cut is one where at least one premise is an axiom ⊢ C, p_{i_{1}}^{⊥}, p_{i_{2}}^{⊥}, ..., p_{i_{n}}^{⊥} in T, and C is the cut-formula in that axiom. We call any axiom premise of a directed cut where the cut-formula in that axiom is not a negative literal a principal axiom of that directed cut. By definition, all directed cuts have at least one principal axiom. A cut between two axioms is always directed, and if the cut-formula of such a cut is non-atomic, that cut has two principal axioms. A directed or standardized proof is a proof with all cuts directed.

When theories are added to linear logic the cut-elimination Theorem A.3 no longer holds, due to the added axioms which may participate directly in cuts. However, we do obtain the following result:

Lemma 3.1 (Cut Standardization) If there is a proof of ⊢ Γ in theory T, then there is a directed proof of ⊢ Γ in theory T.

Proof. We modify the cut-elimination procedure defined in Appendix A in two ways. First we alter the definition of degree to ignore the measure of directed cuts. Formally, we say that if a cut is directed, its degree is zero. Second, we modify the procedure given in Lemma A.1 to handle the extra cases brought about by the presence of axioms. We must allow all the reductions as stated in Appendix A to apply to the case when one of the premises is an axiom, but we need not introduce any truly novel reductions.

We will follow the notation used in Appendix A, where Cut∗ is used to ambiguously refer to the Cut rule or the extra rule of inference introduced in the appendix called Cut!. Also, we will define all the formulas which appear in an axiom to be principal in that application of the axiom.

In Appendix A most of the reductions are given for some specific derivation versus any possible derivation. For example, all the non-principal cases are stated for any derivation of the “other” hypothesis of Cut∗. Similarly, the Identity and ⊤ rules are stated for any derivation of the “other” hypothesis. We simply now state that even if the other derivation involves an axiom, the reduction still applies.

For example, if the last rule applied in the left hypothesis is ⊗, and the last rule in the right hypothesis is an axiom, we apply the following transformation:

\begin{matrix}\underline{⋮ ; ⊢ Σ, C  ⋮ ; ⊢ B, Δ, p_{i}} & ⊗ \\ ⊢ Σ, (C ⊗ B), Δ, p_{i} \end{matrix} \overline{⊢ Γ, p_{i}^{⊥}}^{T} Cut
⊢ Σ, (C ⊗ B), Δ, Γ

⟹

⋮ ⊢ Σ, C \underline{⋮ ; ⊢ B, Δ, p_{i} \overline{⊢ Γ, p_{i}^{⊥}}^{T}}_{Cut}

⊢ B, Δ, Γ ⊗

⊢ Σ, (C ⊗ B), Δ, Γ

This is simply a special case of the reduction given in case A.1.1 in Appendix A.

Also, as a second example, the reduction given for Identity is applicable even to the axiom case:

\underline{\overline{⊢ p_{i}, p_{i}^{⊥}}^{I}  \overline{⊢ Γ, p_{i}^{⊥}}^{T}}_{Cut} ; ⊢ Γ, p_{i}^{⊥} ⟹ \overline{⊢ Γ, p_{i}^{⊥}}^{T}

Again, this is simply a special case of the reduction given in Appendix A.

As a third and final example of specializations of reductions given in the appendix, the ⊤ rule also applies to axioms:

\underline{\overline{⊢ ⊤, Σ, p_{i}}^{⊤} \overline{⊢ Γ, p_{i}^{⊥}}^{T}}_{Cut}

⊢ ⊤, Σ, Γ

⟹ \overline{⊢ ⊤, Σ, Γ}^{⊤}

This is also simply a special case of the reduction given in the appendix.

Now, some simple analysis is required to show that there are no new cases of principal cuts involving axioms. If the cut in question is already directed, the cut has degree zero, by our modified definition, and thus we are done. Otherwise, by definition of axiom we know that the cut-formula is a negative atomic literal. There are only two rules where an atomic literal may be principal: Identity and ⊤. However, both of these cases are handled by existent reductions (restated above). One should also note that since any cut involving two axioms must be directed, we needn’t provide a reduction for that case.

This completes the discussion of the modifications to Lemma A.1 necessary to handle nonlogical axioms. Fortunately, Lemma A.2 and Theorem A.3 then follow without modification (although the definition of degree has changed somewhat).

Therefore, given any proof of a sequent ⊢ Γ in theory T, we can construct a directed proof of ⊢ Γ in theory T.

The cut-elimination procedure in Appendix A introduces a new rule of inference called Cut!. If we generalized axioms to allow ? and ! formulas in axioms, we would have to generalize the notion of directed proof to include cases involving Cut!, and a post processing step would be required to transform all directed Cut!s into a sequence of contractions followed by a single directed Cut, or perhaps simply into a sequence of Cuts. In any event, our axioms are restricted to mall formulas so that any cut involving an axiom is always an application of Cut, never of Cut!.

3.3 Coding Theories in Formulas

In the next few sections, we show that adding nonlogical axioms to mall increases the difficulty of deciding if a sequent is provable from pspace to undecidable. However, we first show that adding nonlogical axioms to full propositional linear logic does not increase its expressive power, or the difficulty of its decision problem. To accomplish this we show how to encode nonlogical axioms in full propositional linear logic, and then prove that the translation is sound and faithful.

We define the translation [T] of a theory T with k axioms into a multiset of pure linear logic formulas by

[{t_{1}, t_{2}, ⋯, t_{k}}] =?[t_{1}],?[t_{2}], ⋯,?[t_{k}]

where [t_{i}] is defined for each axiom t_{i} as follows:

[ ⊢ C, p_{a}^{⊥}, p_{b}^{⊥}, ..., p_{z}^{⊥}] =^{Δ} (C � p_{a}^{⊥} � p_{b}^{⊥} � ⋯ � p_{z}^{⊥})^{⊥} = (C^{⊥} ⊗ p_{a} ⊗ p_{b} ⊗ ⋯ ⊗ p_{z})

Note that the p_{j}^{⊥}’s are negative literals, and that since linear logic is commutative, we needn’t be concerned with the order of formulas in an axiom. Thus each axiom becomes a reusable formula, where the parity of the subformulas of the axiom have been inverted in the formula.

Intuitively, it should be clear that for any theory T, the sequent ⊢ Γ should be provable in theory T if and only if ⊢ [T], Γ is provable without nonlogical axioms. However, due to the unusual nature of linear logic, we will present the proof in detail.

Lemma 3.2 (Theory ⇒) For any finite set of axioms T, ⊢ Γ is provable in theory T only if ⊢ [T], Γ is provable without nonlogical axioms.

Proof. Given some proof of ⊢ Γ in theory T, we have a linear logic proof tree with axioms of T at some leaves. For each leaf of the proof tree of the form ⊢ Δ, where ⊢ Δ is some axiom t_{i}, we replace that leaf with a small proof of ⊢ [T], Δ. This proof tree will be constructed from the proof tree for ⊢ [t_{i}], Δ, and then one application of dereliction leaves us with ⊢?[t_{i}], Γ. Since each formula in [T] begins with ?, we may weaken in the remainder of [T], and thus with some number of weakening steps we have ⊢ [T], Δ. For example, if there are k axioms, and ⊢ Δ is the axiom t_{1} =⊢ q_{1}^{⊥}, (q_{2} ⊗ a), then we know [t_{1}] = q_{1} ⊗ (q_{2}^{⊥} � a^{⊥}). We then perform the following transformation:

\overline{⊢ q_{1}^{⊥}, (q_{2} ⊗ a)}^{T} ⟹

\underline{\overline{⊢ q_{1}, q_{1}^{⊥}}^{I}  \underline{\overline{⊢ q_{2}^{⊥}, q_{2}}^{I} \overline{⊢ a^{⊥}, a}^{I}}_{⊗} ; ⊢ q_{2}^{⊥}, (q_{2} ⊗ a), a^{⊥} ; \overline{⊢ (a^{⊥} � q_{2}^{⊥}), (q_{2} ⊗ a)} ^{�}}_{⊗}
\underline{⊢ q_{1}^{⊥}, q_{1} ⊗ (q_{2}^{⊥} � a^{⊥}), (q_{2} ⊗ a)} _{?D}

⊢ q_{1}^{⊥},?[t_{1}], (q_{2} ⊗ a)

\underline{\overline{⊢?[t_{1}],?[t_{2}], q_{1}^{⊥}, (q_{2} ⊗ a)}^{?W}}_{?W}

⋮

\underline{\overline{⊢?[t_{1}],?[t_{2}], ...?[t_{k−1}], q_{1}^{⊥}, (q_{2} ⊗ a)}^{?W}}_{?W}

⊢ [T], q_{1}^{⊥}, (q_{2} ⊗ a)

For each leaf sequent which was originally an application of identity, we weaken in all the ?[t_{i}] formulas:

\overline{⊢ p_{i}, p_{i}^{⊥}}^{I} ⟹ \overline{⊢ p_{i}, p_{i}^{⊥}}^{I} ; \overline{⊢?[t_{1}], p_{i}, p_{i}^{⊥}}^{?W} ; \underline{\overline{⊢?[t_{1}],?[t_{2}], p_{i}, p_{i}^{⊥}}^{?W}}_{?W} ; ⋮ ; \underline{\overline{⊢?[t_{1}],?[t_{2}], ...?[t_{k−1}], p_{i}, p_{i}^{⊥}}^{?W}}_{?W} ; ⊢ [T], p_{i}, p_{i}^{⊥}

We then continue by adding [T] to every sequent in the entire proof tree. At every application of ⊗ and Cut, we extend the proof tree with an extra copy of the conclusion sequent of the binary rule, to which we add an extra copy of [T]. Then we extend the proof further, adding one contraction step for each ?[t_{i}] between that sequent and the original conclusion of that binary rule.

\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ B, Δ} & ⊗ \\ ⊢ Σ, (A ⊗ B), Δ \end{matrix} ⟹

\underline{⋮ ; ⊢ [T], Σ, A  ⋮ ; ⊢ [T], B, Δ} _{⊗}
\underline{⊢ [T], Σ, (A ⊗ B), Δ, [T]}_{?C}
⋮
\overline{⊢ [T], Σ, (A ⊗ B), Δ}^{?C}

Thus we have given a construction which builds a proof of ⊢ [T], Γ without any nonlogical axioms from a given proof of ⊢ Γ using axioms from T.

Lemma 3.3 (Theory ⇐) For any finite set of axioms T, ⊢ Γ is provable in theory T if ⊢ [T], Γ is provable without nonlogical axioms.

Proof. For each axiom t_{i} ≡ ⊢ C, p_{a}^{⊥}, p_{b}^{⊥}, ..., p_{z}^{⊥}, we may prove !([t_{i}]^{⊥}) ≡ !(C � p_{a}^{⊥} � p_{b}^{⊥} � ⋯ � p_{z}^{⊥}) by several applications of � and one application of !S, as follows.

\overline{\underline{⊢ C, p_{a}^{⊥}, p_{b}^{⊥}, ⋯, p_{z}^{⊥}}_{�}}^{T}
\underline{⊢ (C � p_{a}^{⊥}), p_{b}^{⊥}, ⋯, p_{z}^{⊥}} _{�}
\underline{⊢ (C � p_{a}^{⊥} � p_{b}^{⊥}), ⋯, p_{z}^{⊥}} _{�}
⋮
\overline{\underline{⊢ (C � p_{a}^{⊥} � p_{b}^{⊥} � ⋯ � p_{z}^{⊥})} _{!S}}^{�}
⊢!(C � p_{a}^{⊥} � p_{b}^{⊥} � ⋯ � p_{z}^{⊥})

By cutting this proof against a given proof of ⊢ [T], Γ, we obtain a proof of ⊢ [T − {t_{i}}], Γ, where T − {t_{i}} is the multiset difference of T and {t_{i}}.

⋮ ⊢!([t_{1}]^{⊥}) ⋮ ; ⊢!([t_{2}]^{⊥})  \underline{⋮ ; ⊢!([t_{k}]^{⊥}) ⋮ ; ⊢ [T], Γ} _{Cut} ; \underline{⊢ [\{t_{1}, ⋯, t_{k−1}\}]Γ} ; ⋮ ; \overline{⊢?([t_{1}]),?([t_{2}]), Γ} Cut

⊢?([t_{1}]), Γ Cut

⊢ Γ

Thus by induction on the number of axioms, we can derive ⊢ Γ in theory T.

We have just shown how a decision problem for mall with the addition of nonlogical axioms may be encoded in full propositional linear logic without nonlogical axioms. Thus the upcoming proof of undecidability of mall with nonlogical axioms will yield undecidability for full propositional linear logic.

3.4 And-Branching Two Counter Machines Without Zero-Test

In this section we describe nondeterministic two counter machines with and-branching but without a zero-test instruction. We show that these machines have a recursively unsolvable halting problem, and then we will show how the halting problem for these machines may be encoded as a decision problem in mall, with nonlogical axioms corresponding to the machine instructions.

The machines described here are similar to standard two counter machines except for the lack of an explicit zero test transition, and the addition of “fork” transitions. Intuitively, Q_{i} F ork Q_{j}, Q_{k} is an instruction which allows a machine in state Q_{i} to continue computation from both states Q_{j} and Q_{k}, each computation continuing with the current counter values. For brevity in the following proofs, we emphasize two counter machines. However, there is no intrinsic reason to restrict the machines to two counters. All of our arguments and results generalize easily to N counters, for N ≥ 2. Formally, an And-Branching Two Counter Machine Without Zero-Test, or acm for short, is given by a finite set Q of states, a finite set δ of transitions, and distinguished initial and final states, Q_{I} and Q_{F}, as described below.

An instantaneous description, or ID, of an acm M is a finite list of ordered triples ⟨Q_{i}, A, B⟩, where Q_{i} ∈ Q, and A and B are natural numbers, each corresponding to a counter of the machine. Intuitively, a list of triples represents a set of machine configurations. One may think of an acm state as some sort of parallel computation which terminates successfully only if all its concurrent computation fragments terminate successfully.

We define the accepting triple as ⟨Q_{F} , 0, 0⟩. We also define an accepting ID as any ID where every element of the ID is the accepting triple. That is, every andbranch of the computation has reached an accepting triple. We say that an acm M accepts from an ID s if and only if there is some computation from s to an accepting ID. It is essential for our encoding in linear logic that both counters be zero in all elements of an accepting ID.

The set δ may contain transitions of the following form:

(Q_{i} Increment A Q_{j}) taking
⟨Q_{i}, A, B⟩ to ⟨Q_{j}, A + 1, B⟩
(Q_{i} Increment B Q_{j}) taking
⟨Q_{i}, A, B⟩ to ⟨Q_{j}, A, B + 1⟩
(Q_{i} Decrement A Q_{j}) taking
⟨Q_{i}, A + 1, B⟩ to ⟨Q_{j}, A, B⟩
(Q_{i} Decrement B Q_{j}) taking
⟨Q_{i}, A, B + 1⟩ to ⟨Q_{j}, A, B⟩
(Q_{i} Fork Q_{j}, Q_{k}) taking
⟨Q_{i}, A, B⟩ to (⟨Q_{j}, A, B⟩, ⟨Q_{k}, A, B⟩)

where Q_{i}, Q_{j}, and Q_{k} are states in Q. The Decrement instructions only apply if the appropriate counter is not zero, while the Increment and Fork instructions are always enabled from the proper state.

For example, the single transition Q_{i} Increment A Q_{j} takes an acm from ID: {⋯, ⟨Q_{i}, A, B⟩, ⋯} to ID: {⋯, ⟨Q_{j}, A + 1, B⟩, ⋯}

3.4.1 Two Counter Machines

Standard two counter machines have a finite set of states, Q, a finite set of transitions, δ, a distinguished initial state Q_{I}, and a set of final states F [Min61, HU79]. An instantaneous description of the state of a two counter machine is given by a triple ⟨Q_{i}, A, B⟩, which consists of the current state, and the values of two counters, A and B. The transitions in δ are of four kinds:

(Q_{i} Increment A Q_{j}) taking ⟨Q_{i}, A, B⟩ to ⟨Q_{j}, A + 1, B⟩
(Q_{i} Increment B Q_{j}) taking ⟨Q_{i}, A, B⟩ to ⟨Q_{j}, A, B + 1⟩
(Q_{i} Decrement A Q_{j}) taking ⟨Q_{i}, A + 1, B⟩ to ⟨Q_{j}, A + 1, B⟩
(Q_{i} Decrement B Q_{j}) taking ⟨Q_{i}, A, B + 1⟩ to ⟨Q_{j}, A, B + 1⟩
(Q_{i} Zero-Test A Q_{j}) taking ⟨Q_{i}, 0, B⟩ to ⟨Q_{j}, 0, B⟩
(Q_{i} Zero-Test B Q_{j}) taking ⟨Q_{i}, A, 0⟩ to ⟨Q_{j}, A, 0⟩

A two counter machine accepts if it is able to reach any one of the final states in the set F with both counters at zero. It is important that these machines have a Zero-Test instruction since the halting problem becomes decidable otherwise, by obvious reduction to the word problem in commutative semi-Thue systems, which is decidable [MM82]. Since Zero-Test is the most difficult to encode in linear logic, we concentrate on a machine with and-branching, which provides a basic mechanism powerful enough to simulate Zero-Test, but which is more easily simulated in linear logic.

Using two counter machines, we show that acm’s have an undecidable halting problem.

Lemma 3.4 It is undecidable whether an and-branching two counter machine without zero-test accepts from ID {⟨Q_{I}, 0, 0⟩}. This remains so if the transition relation of the machine is restricted so that there are no outgoing transitions from the final state.

Proof. Since acm’s may simulate zero-test with and-branching, acm’s are sufficiently powerful to simulate two counter machines, for which the halting problem is known to be recursively unsolvable [Min61, Lam61]. We will give a construction from standard two counter machines to acms, and argue that the construction is sound and faithful. This construction and the proof of its soundness is routine, and its steps should be familiar to anyone versed in automata theory. In our simulation of the test for zero instruction of two counter machines, we make essential use of the fact that all branches of computation terminate with both counters set to zero.

Given a nondeterministic two counter machine M we first construct an equivalent two counter machine M′ with a unique final state Q_{F} which has no outgoing transitions. One simply adds two new states, Q_{D} and Q_{F} to M′, and for each Q_{f} ∈ F of M, one adds the instructions (Q_{f} Increment A Q_{D}) and (Q_{D} Decrement A Q_{F}). Note that one may simply look at these new transitions as a single nondeterministic step from each old final state to the new (unique) final state, which has no outgoing transitions. However, since there is no general “silent” move, we make the transition in two steps.

We claim without proof that M and M′ accept the same set of input values, and are therefore equivalent machines.

From a nondeterministic two counter machine M′ with unique final state without outgoing transitions, we construct an acm M′′ as follows. The acm M′′ will have the same set of states, and same initial and final states as M′. The transition function of M′′ is built by first taking all the Increment and Decrement instructions from the transition function of M′. We then add two new states to M′′, Z_{A} and Z_{B}, which are used to test for zero in each of the two counters. For Z_{A}, we add two instructions, (Z_{A} Decrement B Z_{A}), and (Z_{A} Fork Q_{F}, Q_{F}), to the transition function of M′′. Similarly for Z_{B}, we add (Z_{B} Decrement A Z_{B}), and (Z_{B} Fork Q_{F}, Q_{F}). Then for each Zero-Test instruction of M′ of the form

(Q_{i} Zero-Test A Q_{j})

we add one instruction to M′′:

(Q_{i} Fork Q_{j}, Z_{A}).

An important feature of M′′ is that once a zero testing or final state is entered, no configuration of that branch of computation may ever leave that set of states. More specifically, where M′ would test for zero, M′′ will fork into two “parallel” computations. One continues in the “same” state as M′ would have if the Zero-Test had succeeded, and the other branch “verifies” that the counter is indeed zero. While the second branch may change the value of one of the counters (the counter which is not being tested), this cannot affect the values of the counters in the “main” branch of computation. Further, the zero-testing branch of computation never enters any states other than zero-test states or the final state. This holds because there are no outgoing transitions from the final state whatsoever, and the only transitions from the two zero testing states either loop back to that state or move directly to the final state. Also note that any branch of an acm M′′ computation which arrives at the state Z_{A} may be part of a terminating computation if and only if the counter A is zero when the machine reaches that state. This can be seen by observing that once arriving in Z_{A}, there is no possibility of modifications to the counter A. The Decrement B transition from Z_{A} to itself allows M′′ to loop and decrement the counter B arbitrarily. In particular it is possible for B to be decremented to the value 0. Since Q_{F} has no outgoing transitions, the Fork instruction which moves from Z_{A} to Q_{F} and Q_{F} allows this branch of computation to terminate correctly if and only if both counters are zero when it is executed. Since we are considering nondeterministic acms, it is possible for a branch of computation which reaches Z_{A} to terminate if and only if the A counter is zero when it reaches Z_{A}. Similarly, any branch of computation reaching Z_{B} reaches an accepting ID if and only if the B counter is zero.

We claim that there is a halting computation for the given two counter machine M′ if and only if there is one for the constructed acm M′′. This is proven by two simulations.

The and-branching machine M′′ may mimic the original two counter machine in the performance of any instruction, by following any Increment of M′ with the corresponding Increment instruction, and a Decrement with the corresponding Decrement. When M′ executes a Zero-Test A instruction, M′′ forks off an and branch which verifies that the counter A is in fact zero, and the other branch continues to follow the computation of M′.

For the converse simulation, there is always at most one and-branch of any M′′ computation which corresponds to a nonfinal, non-zero-testing state in the original machine. There may be many and branches of the computation which are in states Z_{A}, Z_{B}, and Q_{F}, but at most one and branch is in any other state. Thus, M′ may mimic M′′ by following the branch of acm computation which does not enter Z_{A}, Z_{B}, or Q_{F} until the final step of computation, when it enters Q_{F}. For every Increment and Decrement instruction in the accepting computation of M′′, M′ may performs the corresponding instruction. Every Fork instruction executed by M′′ from a nonfinal, non-zero-testing state corresponds to a Zero-Test instruction in M′, and by the above observation, if M′′ forks into state Z_{A}, then M′′ accepts only if the counter A is zero (and similarly for Z_{B} and the counter B). Since we are assuming an accepting M′′ computation, we know that M′ may execute the corresponding Zero-Test instruction successfully.

3.5 From Machines to Logic

We give a translation from acms to linear logic with theories and show that our sequent translation of a machine in a particular state is provable in linear logic if and only if the acm halts from that state. In fact, our translation uses only mall formulas and theories, thus with the use of our earlier encoding, Lemma 3.2 and Lemma 3.3, we will have our result for propositional linear logic without nonlogical axioms. Since an instantaneous description of an acm is given by a list of triples, it is somewhat delicate to state the induction we will use to prove soundness.

We have already seen how the linear connective & may be used to achieve andbranching in the proof of pspace-completeness of mall. We now make use of that, along with some other machinery, to simulate acm computations.

Given an acm M = ⟨Q, δ, Q_{I}, Q_{F} ⟩ we first define a set of propositions:

{q_{i}|Q_{i} ∈ Q} ⋃ {q_{i}^{⊥}|Q_{i} ∈ Q} ⋃ {a, a^{⊥}, b, b^{⊥}}

We then define the linear logic theory corresponding to the transition relation δ as the set of axioms determined as follows:

Q_{i} Increment A Q_{j} ↦ ⊢ q_{i}^{⊥}, (q_{j} ⊗ a)
Q_{i} Increment B Q_{j} ↦ ⊢ q_{i}^{⊥}, (q_{j} ⊗ b)
Q_{i} Decrement A Q_{j} ↦ ⊢ q_{i}^{⊥}, a^{⊥}, q_{j}
Q_{i} Decrement B Q_{j} ↦ ⊢ q_{i}^{⊥}, b^{⊥}, q_{j}
Q_{i} Fork Q_{j}, Q_{k} ↦ ⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k})

Using linear implication, the (Q_{i} Increment B Q_{j}) transition may be viewed as ⊢ q_{i}−∘(q_{j} ⊗ b), i.e., from state Q_{i}, move to state Q_{j} and add one to counter B. The other axioms in this translation may also be viewed in this way.

We will write C^{n} to indicate a sequence of n C’s, separated by commas, as follows:

C^{n} =^{Δ} \overbrace{C, C, ⋯, C}^{n}

Since p^{⊥} is an atomic symbol, the notation p^{⊥}^{3} will be used for (p^{⊥})^{3}, which is simply p^{⊥}, p^{⊥}, p^{⊥}.

Given a triple ⟨Q_{i}, x, y⟩ of an acm, we define the translation θ(⟨Q_{i}, x, y⟩) by:

θ(⟨Q_{i}, x, y⟩) =^{Δ} ⊢ q_{i}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F}

Thus all sequents which correspond to acm triples have exactly one positive literal, q_{F}, some number of a^{⊥}s, and b^{⊥}s, the multiplicity of which correspond to the values of the two counters of the acm in unary, and exactly one other negative literal, which corresponds to the state of the acm.

The translation of an acm ID is simply the set of translations of the elements of the ID:

θ({E_{1}, E_{2}, ⋯, E_{m}}) = {θ(E_{1}), θ(E_{2}), ⋯, θ(E_{m})}

We claim that an acm M accepts from ID s if and only if every element of θ(s) is provable in the theory corresponding to the transition function of the machine. We prove each half of this equivalence in separate lemmas.

Lemma 3.5 (Machine ⇒) An and-branching counter machine M accepts from ID s only if every sequent in θ(s) is provable in the theory derived from M.

Proof. Given a halting computation of an acm machine M from s we claim we can build a proof of every sequent in θ(s) in the theory derived from M.

M accepts from s only if there is some finite sequence of transitions from this ID to an accepting ID. We proceed by induction on the length of that sequence of transitions.

If there are no transitions in the sequence, then by the definition of accepting ID, s consists entirely of ⟨Q_{F} , 0, 0⟩. We must show that the sequent

⊢ q_{F}^{⊥}, a^{⊥}^{0}, b^{⊥}^{0}, q_{F}

is provable in linear logic. This is immediate: we have 0 A’s and 0 B’s, that is, none at all. Thus by one application of identity per sequent ⊢ q_{F}^{⊥}, q_{F}, we have our proof.

If there is at least one transition in the sequence, we have to show that θ(s) is provable. Since M accepts from ID {⋯ ⟨Q_{i}, A, B⟩ ⋯}, and there is at least one transition in the sequence, we know that there is some transition in M such that ID → ID′, and M accepts from ID′. We assume by induction that there is a linear logic proof which corresponds to the accepting computation for ID′.

We now perform case analysis on the type of transition. There are five different types of instructions: Increment A or B, Decrement A or B, and Fork. Since the two increment and two decrement instructions are nearly identical, we will concentrate only on the cases concerning the counter A.

Q_{i} Increment A Q_{j}: In this case, the first step in the halting computation has the form

{⋯ ⟨Q_{i}, A, B⟩ ⋯} → {⋯ ⟨Q_{j}, A + 1, B⟩ ⋯}

We assume by induction that we have a proof of θ(⟨Q_{j}, A+1, B⟩) = ⊢ q_{j}^{⊥}, a^{⊥}^{A+1}, b^{⊥}^{B}, q_{F}. We extend this proof into a proof of θ(⟨Q_{i}, A, B⟩) = ⊢ q_{i}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F} by adding a cut with an axiom, as follows.

\begin{matrix}\underline{\overline{⊢ q_{i}^{⊥}, (q_{j} ⊗ a)}^{T} ⋮ ; ⊢ q_{j}^{⊥}, a^{⊥}^{A+1}, b^{⊥}^{B}, q_{F} ; \overline{⊢ (q_{j}^{⊥} � a^{⊥}), a^{⊥}^{A}, b^{⊥}^{B}, q_{F}} ^{�}} & Cut \\ ⊢ q_{i}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F} \end{matrix}

Note that the axiom ⊢ q_{i}^{⊥}, (q_{j} ⊗a) is precisely the translation of the transition taken by the machine, and therefore is an axiom of the theory.

Q_{i} Increment B Q_{j}: Analogous to above.

Q_{i} Decrement A Q_{j}: Since the A counter of the machine must be positive for this instruction to apply, we know that the halting computation begins with the transition

{⋯ ⟨Q_{i}, A + 1, B⟩ ⋯} → {⋯ ⟨Q_{j}, A, B⟩ ⋯}

We assume by induction that we have a proof of ⊢ q_{j}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}. As in the Increment A case, we extend this to a proof of ⊢ q_{i}^{⊥}, a^{⊥}^{A+1}, b^{⊥}^{B}, q_{F} by adding a cut with the axiom corresponding to the transition taken by the machine.

\begin{matrix}\underline{\overline{⊢ q_{i}^{⊥}, a^{⊥}, q_{j}}^{T} ⋮ ; ⊢ q_{j}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}} & Cut \\ ⊢ q_{i}^{⊥}, a^{⊥}^{A+1}, b^{⊥}^{B}, q_{F} \end{matrix}

Q_{i} Decrement B Q_{j}: Analogous to above.

Q_{i} Fork Q_{j}, Q_{k}: Here, the halting computation begins with the step

{⋯ ⟨Q_{i}, A, B⟩ ⋯} → {⋯ ⟨Q_{j}, A, B⟩, ⟨Q_{k}, A, B⟩ ⋯}

We assume by induction that we have a proof of ⊢ q_{j}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}, and of ⊢ q_{k}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}, and we extend those proofs into a proof of ⊢ q_{i}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}.

\underline{\overline{⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k})}^{T}  \begin{matrix}\underline{⋮ ; ⊢ q_{j}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}  ⋮ ; ⊢ q_{k}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}} & & \\ ⊢ (q_{j}^{⊥}&q_{k}^{⊥}), a^{⊥}^{A}, b^{⊥}^{B}, q_{F} \end{matrix}}_{Cut} ; ⊢ q_{i}^{⊥}, a^{⊥}^{A}, b^{⊥}^{B}, q_{F}

Here ⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k}) is the axiom which corresponds to the fork instruction.

Lemma 3.6 (Machine ⇐) An and-branching counter machine M accepts from ID s if every sequent in the set θ(s) is provable in the theory derived from M.

Proof.

Given a set of proofs of the elements of θ(s) in the theory derived from M, we claim that a halting computation of the acm M from state s can be extracted from those proofs. We achieve this with the aid of the cut standardization Lemma 3.1, which in this case leaves cuts in the proof only where they correspond to applications of acm instructions. We may thus simply read the description of the computation from the standardized proof.

By Lemma 3.1, it suffices to consider standardized proofs. We show that a set of standardized proofs of θ(s) may be mimicked by the acm M to produce an accepting computation from state s.

This proof is by induction on the sum of the sizes (number of proof rules applied) of standardized proofs. Since an acm state is given by a finite set of triples, and all proofs are finite, we know that this measure is well founded. We assume that any smaller set of proofs which all end in conclusions which correspond to a triple ⟨Q_{i}, A, B⟩ can be simulated by machine M.

We consider the proof of a single element of θ(s) at a time.

If s = {⋯ ⟨Q_{i}, x, y⟩ ⋯}, then θ(s) = {⋯ ⊢ q_{i}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F} ⋯}.

We assume that we are given a proof of each element of the set θ(s), and we analyze one of the proofs, all of which end in a conclusion corresponding to a machine triple ⟨Q_{i}, x, y⟩.

⋮ ; ⊢ q_{i}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F}

Since this sequent is simply a list of atomic propositions, the only linear logic rules which can apply to any such sequent are identity, some axiom, and cut.

Identity is only applicable when both x and y are zero, and q_{i} = q_{F}. In this case, ⊢ q_{F}^{⊥}, q_{F} already corresponds to the accepting triple ⟨Q_{F} , 0, 0⟩.

The only axioms which are identical to a sequent in θ(s) are those which correspond to some δ which is a decrement instruction that ends in q_{F}. In this case, since each decrement axiom in [δ] contains exactly one occurrence of a^{⊥} or b^{⊥}, x = 1 and y = 0, or x = 0 and y = 1. In either case, the acm machine M need only perform the decrement instruction δ, and this branch of computation reaches an accepting triple.

The final possibility is cut, and by our standardization procedure, we know that one hypothesis of that cut is an axiom from the theory derived from M, and furthermore that the cut-formula in that axiom is not a negative literal.

Since there are only five types of instructions in an acm; Increment A or B, Decrement A or B, and Fork, there are only five different types of axioms in a theory derived from any acm M. We now perform case analysis on the type of axiom that was last applied in a proof.

⊢ q_{i}^{⊥}, (q_{j} ⊗ a): If the last axiom applied is of the form ⊢ q_{i}^{⊥}, (q_{j} ⊗ a), then it corresponds to an Increment A instruction, and by standardization, we know the cut-formula must be (q_{j} ⊗ a) in the axiom, and that the proof must look like

\begin{matrix}\underline{\overline{⊢ q_{i}^{⊥}, (q_{j} ⊗ a)}^{T} ⋮ ; ⊢ (q_{j}^{⊥} � a^{⊥}), a^{⊥}^{x}, b^{⊥}^{y}, q_{F}} & Cut \\ ⊢ q_{i}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F} \end{matrix}

Since each other linear logic rule besides � , cut, identity, or axiom introduces some symbol which does not occur in ⊢ (q_{j}^{⊥} � a^{⊥}), a^{⊥}^{x}, b^{⊥}^{y}, q_{F}, the derivation of this sequent must end in one of these rules. Furthermore, there are two formulas in this sequent which are not negative literals, so this sequent is not derivable using only an axiom. Identity could not lead to this sequent, since the sequent contains a non-atomic formula. By our standardization procedure, we know that each cut must involve an axiom from the theory, and the cut-formula in the axiom is not a negative literal. Inspecting the various types of axioms in the theory derived from M, we see that all axioms contain one top level negative atomic formula q_{i}^{⊥} for some i. Since q_{i}^{⊥} cannot be a directed cut-formula in a principal axiom, it must appear in the conclusion of that application of cut. However, there is no such top level q_{i} in the sequent in question. Thus this sequent may only be derived by the application of the � rule. Therefore, we know the derivation must have the form:

\begin{matrix}\underline{\overline{⊢ q_{i}^{⊥}, (q_{j} ⊗ a)}^{T} ⋮ ; ⊢ q_{j}^{⊥}, a^{⊥}^{x+1}, b^{⊥}^{y}, q_{F} ; \overline{⊢ (q_{j}^{⊥} � a^{⊥}), a^{⊥}^{x}, b^{⊥}^{y}, q_{F}} ^{�}} & Cut \\ ⊢ q_{i}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F} \end{matrix}

We know that the proof of ⊢ q_{j}^{⊥}, a^{⊥}^{x+1}, b^{⊥}^{y}, q_{F} may be simulated by the acm by induction, since it is the sequent θ(⟨Q_{j}, x + 1, y⟩), which corresponds to the triple ⟨Q_{j}, x + 1, y⟩, and has a proof in linear logic of smaller size.

Therefore the machine M may emulate this proof by performing the acm instruction corresponding to the axiom used (in this case an Increment A instruction), and then continuing as dictated by the inductive case.

⊢ q_{i}^{⊥}, (q_{j} ⊗ a): Analogous arguments apply.

⊢ q_{i}^{⊥}, a^{⊥}, q_{j}: If the last axiom applied is ⊢ q_{i}^{⊥}, a^{⊥}, q_{j}, which corresponds to a Decrement A instruction, then by standardization, we know the cut-formula must be q_{j} in the axiom, and that the proof must be of the form

\begin{matrix}\underline{\overline{⊢ q_{i}^{⊥}, a^{⊥}, q_{j}}^{T} ⋮ ; ⊢ q_{j}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F}} & Cut \\ ⊢ q_{i}^{⊥}, a^{⊥}^{x+1}, b^{⊥}^{y}, q_{F} \end{matrix}

By induction, the proof of ⊢ q_{j}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F} can be simulated, since it is the sequent θ(⟨Q_{j}, x, y⟩), which corresponds to the triple ⟨Q_{j}, x, y⟩, and has a shorter proof in linear logic.

Therefore the machine M may emulate this proof by performing the acm instruction corresponding to the axiom used (in this case a Decrement A instruction), and then continuing as dictated by the inductive case.

⊢ q_{i}^{⊥}, a^{⊥}, q_{j}: Analogous arguments apply.

⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k}): If the last axiom applied is ⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k}), which corresponds to a Fork instruction, then by standardization, we know the cut-formula must be (q_{j} ⊕ q_{k}) in the axiom, and that the proof must look like

\begin{matrix}\underline{\overline{⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k})}^{T} ⋮ ; ⊢ (q_{j}^{⊥}&q_{k}^{⊥}), a^{⊥}^{x}, b^{⊥}^{y}, q_{F}} & Cut \\ ⊢ q_{i}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F} \end{matrix}

Since each other linear logic rule besides &, cut, identity, or axiom introduces some symbol which does not occur in ⊢ (q_{j}^{⊥}&q_{k}^{⊥}), a^{⊥}^{x}, b^{⊥}^{y}, q_{F}, the derivation of this sequent must end in one of these rules. Furthermore, there are two formulas in the sequent which are not negative literals, so this sequent is not derivable using only an axiom. Identity could not lead to this sequent, since the sequent contains a nonatomic formula. By our standardization procedure, we know that each cut must involve an axiom from the theory, and the cut-formula in the axiom is not a negative literal. Inspecting the various types of axioms in the theory derived from M, we see that all axioms contain one top level negative atomic formula q_{i}^{⊥} for some i. Since q_{i}^{⊥} cannot be the cut-formula in a principal axiom of a directed cut, it must appear in the conclusion of that application of cut. However, there is no such top level q_{i} in the sequent in question. Thus this sequent may only be derived by the application of the & rule. Thus we know the derivation to be of the form:

\underline{\overline{⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k})}^{T}  \begin{matrix}\underline{⋮ ; ⊢ q_{j}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F}  ⋮ ; ⊢ q_{k}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F}} & & \\ ⊢ (q_{j}^{⊥}&q_{k}^{⊥}), a^{⊥}^{x}, b^{⊥}^{y}, q_{F} \end{matrix}}_{Cut} ; ⊢ q_{i}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F}

The proofs of ⊢ q_{j}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F} and ⊢ q_{k}^{⊥}, a^{⊥}^{x}, b^{⊥}^{y}, q_{F} can be simulated on the machine by induction, since one is a sequent which corresponds to the triple ⟨Q_{j}, x, y⟩, the other corresponds to ⟨Q_{k}, x, y⟩, and each has a proof in linear logic of smaller size.

Therefore the machine M may emulate this proof by performing the acm instruction corresponding to the axiom used (in this case a Fork instruction), and then continuing as dictated by the two inductive cases.

From Lemmas 3.4, 3.2, 3.3, 3.5, and 3.6 of this section, we easily obtain our main result:

Theorem 3.7 The provability problem for propositional linear logic is recursively unsolvable.

As mentioned earlier, linear logic, like classical logic, has an intuitionistic fragment. Briefly, the intuitionistic fragment is restricted so that there is only one positive formula in any sequent. In fact, the entire construction above was carried out in intuitionistic linear logic, and thus the undecidability result also holds for this logic.

In any theory derived from an acm M, there is only one positive formula in any theory axiom. Also, throughout a directed proof of θ(s) in such a theory, the only positive atom which appears outside a theory axiom is q_{F}. Thus any directed proof of θ(s) in a theory derived from M is in the intuitionistic fragment of linear logic, and along with a conservativity result not proven here, we have the following:

Corollary 3.8 The provability problem for propositional intuitionistic linear logic is recursively unsolvable.

In the proof of this corollary we make use of the conservativity property of full linear logic over the intuitionistic fragment for any sequents occuring in a directed proof of a translation of an acm machine configuration. This conservativity is a weaker property than full conservativity since sequents in such a directed proof have a special form. In particular, they have no constants, and the right hand side is always a single formula.

3.6 Example Computation

This section is intended to give an overview of the mechanisms we have defined above, and lend some insight into our undecidability result, stated above. We present a simple computation of an ordinary two counter machine with zero-test instruction, a corresponding acm computation, and a corresponding linear logic proof.

Repeating from the introduction, a key insight is that searching for a directed proof of a linear logic sequent in a theory is analogous to searching for an accepting acm computation. A successful search is exactly an accepting computation.

Suppose the transition relation δ of a standard two counter machine with zerotest consists of the following:

δ_{1} : : = Q_{I} Increment A Q_{2}
δ_{2} : : = Q_{3} Decrement A Q_{F}
δ_{3} : : = Q_{2} Zero-Test B Q_{3}

The machine may perform the following transitions, where an instantaneous description of a two counter machine is given by the triple consisting of Q_{j}, the current state, and the values of counters A and B.

⟨Q_{I}, 0, 0⟩ ⟶^{δ_{1}} ⟨Q_{2}, 1, 0⟩ ⟶^{δ_{3}} ⟨Q_{3}, 1, 0⟩ ⟶^{δ_{2}} ⟨Q_{F} , 0, 0⟩

This computation starts in state Q_{I}, increments the A counter and steps to state Q_{2}. Then it tests the B counter for zero, and moves to Q_{3}, where it then decrements the A counter, moves to Q_{F}, and accepts.

The transition relation δ may be transformed into a transition relation δ′ for an equivalent and-branching two counter machine without zero-test. The modified relation δ′ (shown on the left below), may then be encoded as a linear logic theory (shown on the right):

Transitions

δ′_{1} : : = Q_{I} Increment A Q_{2}
δ′_{2} : : = Q_{3} Decrement A Q_{F}
δ′_{3} : : = Q_{2} Fork Z_{B}, Q_{3}
δ′_{4} : : = Z_{B} Decrement A Z_{B}
δ′_{5} : : = Z_{B} Fork Q_{F} , Q_{F}

Theory Axioms ⊢ q_{I}^{⊥}, (q_{2} ⊗ a) ⊢ q_{3}^{⊥}, a^{⊥}, q_{F} ⊢ q_{2}^{⊥}, (z_{B} ⊕ q_{3}) ⊢ z_{B}^{⊥}, a^{⊥}, z_{B} ⊢ z_{B}^{⊥}, (q_{F} ⊕ q_{F})

Notice how the first two transitions (δ_{1} and δ_{2}) of the standard two counter machine are preserved in the translation from δ to δ′. Also, the Zero-Test instruction δ_{3} is encoded as three acm transitions — δ′_{3}, δ′_{4}, and δ′_{5}. The transition δ′_{3} is a fork to a special state Z_{B}, and one other state, Q_{3}. The two extra transitions, δ′_{4} and δ′_{5}, force the computation branch starting in state Z_{B} to verify that counter B is zero. Given the above transitions, the and-branching machine without zero-test may then perform these moves:

\begin{matrix}\{⟨Q_{I}, 0, 0⟩\} ⟶^{δ′_{1}} \{⟨Q_{2}, 1, 0⟩\} ⟶^{δ′_{3}} \{⟨Z_{B}, 1, 0⟩, ⟨Q_{3}, 1, 0⟩\} ⟶^{δ′_{4}} \{⟨Z_{B}, 0, 0⟩, ⟨Q_{3}, 1, 0⟩\} ⟶^{δ′_{5}} \\ \{⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩, ⟨Q_{3}, 1, 0⟩\} ⟶^{δ′_{2}} \{⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩\} \end{matrix}

Note that an instantaneous description of this and-branching machine is a list of triples, and the machine accepts if and only if it is able to reach ⟨Q_{F} , 0, 0⟩ in all branches of its computation. This particular computation starts in state Q_{I}, increments the A counter and steps to state Q_{2}. Then it forks into two separate computations; one which verifies that the B counter is zero, and the other which proceeds to state Q_{3}. The B counter is zero, so the proof of that branch proceeds by decrementing the A counter to zero, and jumping to the final state Q_{F}. The other branch from state Q_{3} simply decrements A and moves to Q_{F}. Thus all branches of the computation terminate in the final state with both counters at zero, resulting in an accepting computation.

The linear logic proof corresponding to this computation is displayed in Figures 3.1 and 3.2, and is explained in the following paragraphs. In these proofs, each application of a theory axiom corresponds to one step of acm computation. We represent the values of the acm counters in unary by copies of the formulas a^{⊥} and b^{⊥}. In this example the B counter is always zero, so there are no occurrences of b^{⊥}.

The proof shown in Figure 3.1 of ⊢ z_{B}^{⊥}, a^{⊥}, q_{F} in the above linear logic theory corresponds to the acm verifying that the B counter is zero. Reading the proof bottom up, it begins with a directed cut. The sequent ⊢ z_{B}^{⊥}, q_{F} is left as an intermediate step. The next step is to use another directed cut, and after application of the & rule, we have two sequents left to prove: ⊢ q_{F}^{⊥}, q_{F} and ⊢ q_{F}^{⊥}, q_{F}. Both of these correspond to the acm triple ⟨Q_{F} , 0, 0⟩ which is the accepting triple, and are provable by the identity rule. If we had attempted to prove this sequent with some occurrences of b^{⊥}, we would be unable to complete the proof.

\overline{⊢ z_{B}^{⊥}, a^{⊥}, z_{B}}^{δ4^{′}}  \underline{\overline{⊢ z_{B}^{⊥}, (q_{F} ⊕ q_{F})}^{δ5^{′}}  \underline{\overline{⊢ q_{F}^{⊥}, q_{F}}^{I} \overline{⊢ q_{F}^{⊥}, q_{F}}^{I}}_{&} ; ⊢ (q_{F}^{⊥} & q_{F}^{⊥}), q_{F}}_{Cut} ; ⊢ z_{B}^{⊥}, q_{F} Cut
⊢ z_{B}^{⊥}, a^{⊥}, q_{F}

Figure 3.1: Zero-test proof

\overline{⊢ q_{I}^{⊥}, (q_{2} ⊗ a)}^{δ1^{′}} \underline{\overline{⊢ q_{2}^{⊥}, (z_{B} ⊕ q_{3})}^{δ3^{′}}  \underline{⋮ ; ⊢ z_{B}^{⊥}, a^{⊥}, q_{F}  \underline{\overline{⊢ q_{3}^{⊥}, a^{⊥}, q_{F}}^{δ2^{′}} \overline{⊢ q_{F}^{⊥}, q_{F}}^{I}}_{Cut} ; ⊢ q_{3}^{⊥}, a^{⊥}, q_{F}}_{&} ; ⊢ (z_{B}^{⊥} & q_{3}^{⊥}), a^{⊥}, q_{F}}_{Cut} ; ⊢ q_{2}^{⊥}, a^{⊥}, q_{F} ; \overline{⊢ (q_{2}^{⊥} � a^{⊥}), q_{F}} ^{�} Cut
⊢ q_{I}^{⊥}, q_{F}

Figure 3.2: Proof corresponding to computation

The proof shown in Figure 3.2 of ⊢ q_{I}^{⊥}, q_{F} in the same theory demonstrates the remainder of the acm machinery. The lowermost introduction of a theory axiom, cut, and � together correspond to the application of the increment instruction δ′_{1}. That is, the q_{I}^{⊥} has been “traded in” for q_{2}^{⊥} along with a^{⊥}. The application of a directed cut and & correspond to the fork instruction, δ′_{3} which requires that both branches of the proof be successful in the same way that and-branching machines require all branches to reach an accepting configuration. The elided proof of ⊢ z_{B}^{⊥}, a^{⊥}, q_{F} appears in Figure 3.1, and corresponds to the verification that the B counter is zero. The application of cut and identity correspond to the final decrement instruction of the computation, and complete the proof.

Noncommutative Propositional Linear Logic

The following may be called the unrestricted exchange rule:

E \frac{⊢ Σ, Γ, A}{⊢ Σ, A, Γ}

Since sequents are treated as multisets of formulas in linear logic, the E rule is implicitly present in full linear logic. This structural rule allows sequents to be permuted arbitrarily, making linear logic a commutative logic. More specifically, ⊢ (A ⊗ B)−∘(B ⊗ A) is derivable in linear logic using exchange, as are the analogous sequents for all the other binary connectives of linear logic ( � , ⊕, & ). Since sequents are considered to be implicitly commutative, the E rule does not explicitly appear in proofs or lists of proof rules for linear logic. However, the absence of the E rule (treating sequents as lists of formulas) drasticly alters the set of provable sequents in linear logic. In fact, without the exchange rule, ⊢ (A ⊗ B)−∘(B ⊗ A) is not derivable. Thus the E rule forces ⊗ (and other connectives) to be commutative.

Noncommutative propositional linear logic is linear logic where the unrestricted exchange rule is omitted, or equivalently, where sequents are treated as being lists instead of multisets. This entire family of logics is quite speculative, ad hoc, and most formulations are original to this paper. Thus one should not take too seriously any of the results of this chapter.

The family of noncommutative linear logics may be derived from linear logic by treating sequents as lists of formulas, instead of multisets. Thus the order of formulas in a sequent becomes important. However, the immediate resulting system is unsatisfying in that the reusable formulas (those marked by ?) are exactly the ones which can be contracted and weakened in linear logic, and thus should be permitted the freedom of exchange, even in the noncommutative versions of linear logic.

There are a whole family of logics which could result from various additions of restricted exchange to noncommutative linear logic. The main point of difference within this family is the exact formulation of the rules of inference. However, most members of this family of logics have an undecidable provability problem.

In fact, the multiplicative and reuse operators are sufficient to encode undecidable problems in most of these logics. In other words, the constants and additive connectives are not necessary in order to simulate a Turing machine in noncommutative linear logic, although they appear to be necessary in (commutative) linear logic. Below we present the detailed proof of undecidability for a particular logic we will call ncl, which is actually the multiplicative and reuse fragment of a member of the noncommutative linear logic family.

David Yetter [Yet90] has also studied a variant of noncommutative linear logic. In his work, he considered a system with two new modalities, k and K, which are related to ? and !. The k modality essentially marks those formulas which are free to be permuted, despite the noncommutativity of the logic in general. The reusable formulas (marked with ?) are allowed to permute, but are also allowed the freedom of contraction and weakening, while the k and K formulas are not. We find no compelling reason for these extra connectives, except to facilitate the encoding of (commutative) linear logic in noncommutative linear logic by prefixing every subformula with k or K. Based on our results below, other encodings of linear logic into noncommutative linear logic without k and K exist. Thus we do not include any new connectives or modalities in our logics presented below, and allow only the reusable ? formulas to permute.

We now focus on one particular member of the family of noncommutative linear logics. This logic will include only the multiplicative and reuse connectives of linear logic, excluding the additives. In order to mesh smoothly with the earlier chapters we will use the proof rules as presented in Appendix B, but add two new rules, one which allows ? formulas to permute, and one which allows an entire sequent to be “rotated”. Thus one may think of a sequent as a circular list of formulas. We call this logic ncl for “circular logic”.

4.1 NCL Proof Rules

The system ncl includes the I, Cut, ⊗, � ,?W,?C,?D, and !S rules of linear logic, with each sequent treated as a circular list of formulas instead of as a multiset. The following two rules of inference are also included in ncl:

?E \frac{⊢ Γ, Σ,?A}{⊢ Γ,?A, Σ}  \frac{⊢ Γ, A}{⊢ A, Γ} R

These rules allow one to permute and exchange the reusable (?) formulas arbitrarily, and to rotate the entire sequent of reusable and non-reusable formulas. As our previous discussions of linear logic accepted exchange as “part of the system” by considering sequents to be multisets of formulas, we will now consider the exchange rules ?E and R implicitly, by regarding sequents as circular lists of linear logic formulas.

4.2 NCL is Undecidable

We will show the word problem for semi-Thue systems has a straightforward encoding in ncl. Since we have already shown that full linear logic is undecidable, the fact that full noncommutative linear logic is undecidable is not too surprising. But since ncl is a fragment of noncommutative linear logic which does not contain the additive connectives, the earlier construction of and-branching two-counter machines in full linear logic would fail in ncl. However, the and-branching used in that construction was required in order to encode zero-test in a commutative setting. In a noncommutative setting a zero test operation may be encoded easily without any sort of and-branching. This situation is analogous to that for commutative versus noncommutative semi-Thue systems, where the noncommutative version allows the encoding of a zero test leading to undecidability, whereas the commutative version is unable to simulate zero test and has been shown to be decidable [Kos82]. In fact, since ncl closely resembles semi-Thue systems, we will demonstrate undecidability of ncl by a reduction from semi-Thue systems.

Although the reduction is simple, the proof of its correctness requires some elaborate machinery. In particular the proof of cut-elimination given in Appendix A has been given in such a way that it applies to ncl as well as linear logic.

Lemma 4.1 (Cut Elimination Revisited) If there is a proof of sequent ⊢ Γ in ncl, then there is a cut-free proof of ⊢ Γ in ncl.

Proof. The cut-elimination theorem for full linear logic in Appendix A is presented in a way which gives a cut elimination procedure for ncl. The only violations of the list-ordering of rules are those which correspond to the permutation of reusable formulas, such as in the case of principal cuts of ⊗ versus !S. However, these cases are legal ncl cut proof steps, since we are assuming the ncl proof rules ?E and R are built in to the ncl system. Thus the cut-elimination procedure for full linear logic may be employed to remove cuts from ncl proofs.

Corollary 4.2 (Subformula Property Revisited) Any formula in any cut-free ncl proof of ⊢ Γ is a subformula of Γ.

Proof. Immediate.

4.3 NCL Theories

We will define theories as for the commutative case (see Section 3.2), and show that cut-standardization (see Lemma 3.1) again holds in this logic.

Formally, a ncl axiom may be any ncl sequent of the form ⊢ C, p_{i_{1}}^{⊥}, p_{i_{2}}^{⊥}, ..., p_{i_{n}}^{⊥}, where C is any ncl formula not including modal operators (? or !), and the remainder of the sequent is made up of negative literals. Any finite set of ncl axioms is a ncl theory. For any theory T, we say that a sequent ⊢ Γ is provable in T exactly when we are able to derive ⊢ Γ using the standard set of ncl proof rules and ncl axioms from T. Thus each axiom of T is treated as a reusable sequent which may occur as a leaf of a proof tree. As before we will write \overline{⊢ Γ}^{T} for a leaf sequent which is a member of the theory T.

We recall the definition of a directed cut: a directed cut is one where at least one premise is an axiom ⊢ C, p_{i_{1}}^{⊥}, p_{i_{2}}^{⊥}, ..., p_{i_{n}}^{⊥} in T, and C is the cut-formula in that axiom. We call any axiom premise of a directed cut where the cut-formula in that axiom is not a negative literal a principal axiom of that directed cut. By definition, all directed cuts have at least one principal axiom. A cut between two axioms is always directed, and if the cut-formula of such a cut is non-atomic, that cut has two principal axioms. A directed or standardized proof is a proof with all cuts directed.

Lemma 4.3 (ncl Cut Standardization) If there is a proof of ⊢ Γ in theory T in ncl, then there is a directed proof of ⊢ Γ in theory T in ncl.

Proof. The proof of cut-standardization in full linear logic (Lemma 3.1) applies to this case with little modification. In fact there are fewer cases here since the constants and additive connectives are not present in ncl.

The earlier translation from theories into pure linear logic is also a translation of ncl theories into pure ncl. For convenience, we repeat the definition here: The translation [T] of a ncl theory T with k axioms is the list of ncl formulas:

[{t_{1}, t_{2}, ⋯, t_{k}}] =?[t_{1}],?[t_{2}], ⋯,?[t_{k}]

where [t_{i}] is defined for each axiom t_{i} as follows:

[ ⊢ C, p_{a}^{⊥}, p_{b}^{⊥}, ..., p_{z}^{⊥}] =^{Δ} (C � p_{a}^{⊥} � p_{b}^{⊥} � ⋯ � p_{z}^{⊥})^{⊥} = (p_{z} ⊗ ⋯ ⊗ p_{b} ⊗ p_{a} ⊗ C^{⊥})

Note that the p_{j}^{⊥}’s are negative literals.

Lemma 4.4 (ncl Theory ⇒) For any finite set of axioms T, ⊢ Γ is provable in theory T only if ⊢ [T], Γ is provable.

Proof. The proof of Lemma 3.2 carries over to ncl without modification, since the ?E and R rules are considered implicit.

Lemma 4.5 (ncl Theory ⇐) For any finite set of axioms T, ⊢ Γ is provable in theory T if ⊢ [T], Γ is provable.

Proof. Similarly, the proof of Lemma ⇐ 3.3 given earlier applies here without modification in the system where the ?E, R rules are considered part of the ncl system.

4.3.1 Semi-Thue Systems

A semi-Thue system T over alphabet Σ is a set of pairs ⟨x → y⟩, where x and y are strings over Σ. Each pair in T is called a production, and we use them as rewrite rules. We call x the left hand side and y the right hand side of a production ⟨x → y⟩. U rewrites to V in system T with a production ⟨g → g′⟩ if U and V are words over Σ, and there exist possibly null words r and s such that U = rgs and V = rg′s. We write

U⟹V

if U rewrites to V using some production. We use the notation

U⟹^{∗}V

if there exists a (possibly empty) sequence of words U_{1}, ⋯, U_{n} such that

U⟹U_{1}⟹U_{2}⟹ ⋯ ⟹U_{n}⟹V

The word problem for a semi-Thue system T the problem of determining, for a given pair of words U and V, whether or not U⟹^{∗}V in system T . This problem is known to be undecidable [Pos47]. The problem remains undecidable if we add the condition that V be a singleton (word of length one) n such that n does not occur in U or in the right hand side of any production, and only appears as a singleton on the left hand side of productions. This restriction is analogous to requiring that a Turing machine have a unique final state without any outgoing transitions. The semi-Thue word problem also remains undecidable if there is a special end marker symbol m which is preserved by any rules which involve it except rules involving n. That is, the initial word U begins with a symbol m which does not occur anywhere else in U, and every rule in which m appears is of the form ⟨mw_{i} → mw_{j}⟩ or is of the form ⟨mw_{i} → n⟩ for some words w_{i} and w_{j} not containing m. This restriction is analogous to requiring that a Turing machine have only a one-way infinite tape.

To show that the above restrictions preserve undecidability it suffices to give a transformation from a general word problem to a word problem of the restricted class. Specifically, given a word problem from U to V, with set of productions T , we may add the production mV → n where m and n are new symbols which are added to Σ. We then ask the new word problem from mU to n (with the new and the original productions), in the alphabet Σ ∪ {m, n}. This problem is solvable if and only if the original problem is. However this new problem is of the restricted class defined above.

4.4 From Semi-Thue Systems to Noncommutative Linear Logic

We overload the definition of translation [ ] to include the case of words — the translation of a word [ab ⋯ z] is the list of ncl formulas p_{a}^{⊥}, p_{b}^{⊥}, ⋯, p_{z}^{⊥}. We also define [ab ⋯ z]^{⊥} to be the ncl formula p_{z} ⊗ ⋯ ⊗ p_{b} ⊗ p_{a}. Finally, as a notational convenience, we let γ(Γ) designate ambiguously any formula which could be derived from Γ by applications of the � rule. In other words, γ(Γ) is the result of replacing some number of commas separating formulas in Γ by � .

Given a Semi-Thue system T = {⟨a_{1} → b_{1}⟩, ⟨a_{2} → b_{2}⟩ ⋯ ⟨a_{k} → b_{k}⟩}, we define the ncl theory derived from T as the following set of sequents:

⊢ [a_{1}], [b_{1}]^{⊥} ; ⊢ [a_{2}], [b_{2}]^{⊥} ; ⋮ ; ⊢ [a_{k}], [b_{k}]^{⊥}

For a word problem P consisting of the pair U, V we define the translation τ(P) of this problem into a ncl sequent as:

⊢ [U], [V]^{⊥}

Now, we show that the word problem P is solvable within system T if and only if the translation τ(P) is provable in the theory derived from T . We state the two parts of the equivalence as Lemmas 4.6 and 4.7.

Lemma 4.6 The word problem P is solvable in the semi-Thue system T only if τ(P) is provable in the theory derived from T .

Proof. We proceed by induction on the length of the derivation of U⟹^{∗}V. If the derivation is trivial, that is U ≡ V, then we must show that the sequent

⊢ [V], [V]^{⊥}

is provable. Since we assume the word problem has the restricted form with V a singleton, this sequent actually has the form ⊢ [n], [n]^{⊥}, which by definition of notation is ⊢ p_{n}^{⊥}, p_{n}. This is provable by identity.

Suppose the derivation of U⟹^{∗}V is a nonempty sequence:

U⟹U_{1}⟹U_{2}⟹ ⋯ ⟹U_{n}⟹V.

Since U⟹U_{1}, there is some rule ⟨g → g′⟩ in T , and possibly null words r and s such that

\begin{aligned}[U] & = & [rgs] & = & p_{r_{1}}^{⊥} ⋯ p_{r_{i}}^{⊥}p_{g_{1}}^{⊥} ⋯ p_{g_{j}}^{⊥}p_{s_{1}}^{⊥} ⋯ p_{s_{k}}^{⊥} \\ [U]^{⊥} & = & [rgs]^{⊥} & = & [s]^{⊥}[g]^{⊥}[r]^{⊥} \\ [U_{1}] & = & [rg′s] & = & p_{r_{1}}^{⊥} ⋯ p_{r_{i}}^{⊥}p_{g′_{1}}^{⊥} ⋯ p_{g′_{h}}^{⊥}p_{s_{1}}^{⊥} ⋯ p_{s_{k}}^{⊥} \\ [U_{1}]^{⊥} & = & [rg′s]^{⊥} & = & [s]^{⊥}[g′]^{⊥}[r]^{⊥} \end{aligned}

By induction we assume that we have a proof of ⊢ [U_{1}], [V]^{⊥}, and construct from this a proof of the following form:

\begin{matrix}\underline{\overline{⊢ [g], [g′]^{⊥}}^{T} ⋮ ; ⊢ [r], [g′], [s], [V]^{⊥} ; \underline{\overline{⊢ [r], γ([g′]), [s], [V]^{⊥}}^{�}}_{�} ; ⋮ ; \overline{⊢ [r], γ([g′]), [s], [V]^{⊥}}^{�}} & Cut \\ ⊢ [r], [g], [s], [V]^{⊥} \end{matrix}

In this partial deduction there are as many applications of the � rule as there are separate formulas in [g′]. This is because each application of � replaces a comma by a � in the γ([g′]) formula.

The following concrete example illustrates the intended simulation. Assume that the first rule applied in the sequence of reductions is ⟨cd → xy⟩. Then g in the above schema is cd, and g′ is xy. Also, [g] is p_{c}^{⊥}, p_{d}^{⊥}, [g′] is p_{x}^{⊥}, p_{y}^{⊥}, and γ([g′]) is (p_{x}^{⊥} � p_{y}^{⊥}). Also assume that r is mab, s is ef, and [V]^{⊥} is p_{n}.

\begin{matrix}\underline{\overline{⊢ p_{c}^{⊥}, p_{d}^{⊥}, (p_{y} ⊗ p_{x})}^{T} ⋮ ; ⊢ p_{m}^{⊥}, p_{a}^{⊥}, p_{b}^{⊥}, p_{x}^{⊥}, p_{y}^{⊥}, p_{e}^{⊥}, p_{f}^{⊥}, p_{n} ; \overline{⊢ p_{m}^{⊥}, p_{a}^{⊥}, p_{b}^{⊥}, (p_{x}^{⊥} � p_{y}^{⊥}), p_{e}^{⊥}, p_{f}^{⊥}, p_{n}} ^{�}} & Cut \\ ⊢ p_{m}^{⊥}, p_{a}^{⊥}, p_{b}^{⊥}, p_{c}^{⊥}, p_{d}^{⊥}, p_{e}^{⊥}, p_{f}^{⊥}, p_{n} \end{matrix}

Thus, by induction, given a sequence of reductions which solves a word problem, we may simulate the solution in ncl.

Lemma 4.7 The word problem P is solvable with productions T if τ(P) is provable in the theory derived from T .

Proof. We remember that the target word V of the word problem is a singleton and that there is a special marker symbol m at the beginning of U which is preserved by all the productions in T .

The construction of a rewrite sequence begins with any proof of τ(P), and then produces a directed proof by cut-elimination. We may read any directed proof of τ(P) as a solution to the word problem P, since each directed cut corresponds directly to the application of one reduction in the semi-Thue system.

In more detail, given a proof which ends in a sequent ⊢ Γ where ⊢ Γ is equal to τ(P), possibly with some of the commas in τ(P) replaced with � , we apply the ncl cut-standardization Lemma 4.3, and obtain a directed proof of ⊢ Γ. We now prove by induction on the length of the directed proof that this proof may be mimicked by the corresponding semi-Thue system.

In the case that ⊢ Γ is equal to ⊢ [V], [V]^{⊥}, (for example, this proof may be a single application of the identity rule) then the solution to the word problem is trivial, i.e., no productions are required, since U ≡ V.

In the induction step, ⊢ Γ cannot be provable with the identity rule. Inspecting the other rules of ncl, we see that ⊗ and the ? and ! rules are inapplicable, since the conclusion sequent does not contain any occurrences of ⊗, ?, or !. If � is the last rule applied in the proof, then we appeal to the induction hypothesis, since then we simply have replaced fewer commas with � . The only remaining case is Cut, and by cut-standardization, we know one hypothesis is an axiom, and the cut-formula in that axiom is not a negative literal. Inspecting the axioms in the theory corresponding to the productions of a semi-Thue system, we see that the cut-formula must always be a formula [g′]^{⊥}. This formula is built up from positive literals connected by ⊗. The cut-formula in the other hypothesis then must be built from negative literals connected by � .

Since the start marker m on the initial word U is preserved by each production in T , we know that the ncl theory derived from T has a special property: the translation p_{m} of m may not be a subformula of the cut-formula of a directed cut unless it also appears in the first non-principal position following the cut-formula in the axiom. Thus the start marker participates in a directed cut if and only if it is the first symbol in the sequence of symbols replaced by the cut. It follows that the translation p_{m} of the start marker is preserved in any directed proof of any well formed word problem. This allows us to conclude that no rule is applied “around the end” of a word through some convoluted use of the rotation rule, and thus that the semi-Thue system may mimic the ncl proof by applying the corresponding production to the string. By induction, we have our result.

Theorem 4.8 The provability problem for ncl is recursively unsolvable.

Corollary 4.9 The provability problem for ncl augmented with the additive (& and ⊕) and constant (⊥, 1, and ⊤) rules is recursively unsolvable.

This corollary follows from the theorem by a conservativity result which is easily derived from the cut-elimination and subformula properties of ncl.

4.5 Other Noncommutative Logics

As mentioned previously, there is a family of logics which share a strong resemblance to ncl. All of the ones we can sensibly imagine have undecidable decision problems.

In all formulations of noncommutative linear logic the key rule is ⊗. In a sense which we make more precise later, the constants and additive connectives of linear logic are inherently commutative. Also, the � rule follows the ⊗ rule in its commutativity. Thus noncommutative linear logic is quite sensitive to the exact formulation of ⊗. However, there are some minor variations on the syntactic presentation of the other proof rules which first bear some notice.

4.5.1 Rotate Rule versus Embedding

One motivation for the particular formulation of ncl studied in the previous section (in particular, the introduction of the R rule) is so that we may make use of the same formulation of linear logic rules given in Appendix B, and refer to the previously demonstrated lemmas about linear logic with as little modification as possible. Without the R rule we would have to modify the formulation of other rules, such as the � rule, to allow its application within a sequent, instead of requiring its application at one end of a sequent. To see this, compare the original version of � on the left with the modified version on the right below:

� \frac{⊢ Σ, A, B}{⊢ Σ, (A � B)}  \frac{⊢ Σ, A, B, Γ}{⊢ Σ, (A � B), Γ} � 2

We will call the � 2 rule the embedded equivalent of the � rule. The use of � 2 in noncommutative linear logic without the R rule directly corresponds to the use of � in ncl with R rule considered part of the system. We will use encl to stand for the system derived from ncl by removing the R rule, and replacing all other rules by their embedded equivalents, and adding a symmetric identity rule.

Lemma 4.10 A sequent ⊢ Γ is provable in ncl if and only if it is provable in Encl.

This lemma follows by induction on the length of proofs, and from this lemma we obtain undecidability for this system.

Corollary 4.11 The provability problem for ncl without the R rule, and with every other rule replaced by its embedded equivalent is recursively unsolvable.

4.5.2 NCL without ?E

The earlier proof of undecidability fails in ncl without the ?E rule, since some of the requisite lemmas about theories fail. However, we may omit this rule, and replace ?C with the following ?C2 rule to restore our results, and many other properties of noncommutative linear logic.

?C \frac{⊢ Σ,?A,?A}{⊢ Σ,?A}  \frac{⊢ Σ,?A, Γ,?A}{⊢ Σ, Γ,?A} ?C2

This contraction rule essentially states that what may be proven from two not necessarily contiguous assumptions of a reusable formula, may be proven from one assumption of that reusable formula. It is the case that the ?C2 rule is derivable from the ?E and ?C rules in ncl.

Lemma 4.12 A sequent ⊢ Γ is provable in ncl if and only if it is provable in ncl without the ?E rule, and with the ?C rule replaced by ?C2.

This lemma may be proven by induction on the length of proofs. Essentially, in ncl one may contract and then exchange the reusable formula to any desired position, while in the other system one may contract the formula directly into position. On the other hand, to permute a reusable formula in ncl, one simply applies exchange, while in the other system one must contract the formula into position, and then weaken away the formula in its previous position. Using this lemma, we may obtain the following undecidability result.

Corollary 4.13 The provability problem for ncl without the ?E rule, and with the ?C rule replaced by ?C2 rule is recursively unsolvable.

4.5.3 Alternate ⊗

There are two quite reasonable versions of the ⊗ rule in noncommutative linear logic, one as used above defined in Appendix B, and the other using a different sequent order in the conclusion:

⊗ \frac{⊢ Σ, A  ⊢ B, Γ}{⊢ Σ, (A ⊗ B), Γ}  \frac{⊢ Σ, A  ⊢ Γ, B}{⊢ Σ, Γ, (A ⊗ B)} ⊗2

The two formulations are equivalent in the presence of unrestricted exchange (commutative linear logic), but are subtlely different in the context of noncommutative linear logic. In a noncommutative linear logic with ⊗ replaced by ⊗2, the definition of negation must change. In particular, the negation of the multiplicative connectives would be defined as follows:

(A ⊗ B)^{⊥} =^{Δ} A^{⊥} � B^{⊥}  (A � B)^{⊥} =^{Δ} A^{⊥} ⊗ B^{⊥}

We define the translation σ(Γ) of a sequent Γ to be the sequent Γ with all occurrences of formulas of the form A ⊗ B replaced by B ⊗ A.

Lemma 4.14 A sequent ⊢ Γ is provable in ncl if and only if σ(Γ) is provable in ncl with the ⊗ rule replaced by the ⊗2 rule

Lemma 4.15 A sequent ⊢ σ(Γ) is provable in ncl if and only if Γ is provable in ncl with the ⊗ rule replaced by the ⊗2 rule

This lemma follows by induction on the height of proofs.

Lemma 4.16 The provability problem for ncl with the ⊗ rule replaced by the ⊗2 rule and alternate definition of negation is recursively unsolvable.

This lemma follows from the above two, which simply state that by reversing the order of all tensor (⊗) formulas, we pass from ncl to this new logic, and back again. Thus a decision procedure for one implies a decision procedure for the other, and by Lemma 4.8, we know there is no decision procedure for ncl.

4.5.4 Mix and Match

The above modifications of ncl do not interfere with cut-elimination, nor with the basic undecidability result for ncl. It is also the case that even in combination the above three modifications, (R versus embedding, ?E versus ?C2, and ⊗ versus ⊗2) do not interact. That is, any combination of these modications retains the character of ncl, including the properties of being undecidable, and having a cut-elimination theorem.

4.6 Degenerate Noncommutative Linear Logics

Some variations on the ncl system are not as benign as the above. In fact, it is much easier to create nonsense than a coherent logic by altering proof rules haphazardly.

The main focus of this section is to consider plausible but degenerate variants of the rules based on interleaving the circular orders of hypotheses.

4.6.1 Intermingling ⊗

At first glance, it might seem interesting to study the systems obtained when binary rules in ncl are replaced with rules which allow intermingling of the hypotheses in the conclusion. For example,

⊗3 \frac{⊢ Σ, A  ⊢ B, Γ}{⊢ Δ, (A ⊗ B)} where Δ is some interleaving of Σ and Γ

Somewhat surprisingly, the system obtained by replacing ⊗ with ⊗3 in ncl is equivalent to a commutative version of ncl.

Lemma 4.17 A sequent ⊢ Γ is provable in the system obtained by replacing ⊗ by ⊗3 in ncl if and only if that sequent is provable in the system obtained by adding the unrestricted exchange rule to ncl.

This lemma follows by induction on the length of cut-free proofs. Formally, we need a cut-elimination procedure for both logics. The cut-elimination procedure for full linear logic suffices to eliminate cuts from ncl with unrestricted exchange. Cutelimination for ncl with ⊗ replaced by ⊗3 is possible to prove directly, although the principal ⊗3 versus � case is quite difficult. Cut-elimination in this case may be accomplished with the addition of an “intermingling cut” rule which along with the nonintermingling cut rule may be eliminated from any proof. The key reason this lemma holds is that ⊗ and � are the only binary connectives of ncl and allowing (A ⊗ B) to be equivalent to (B ⊗ A) in this context causes (A � B) to be equivalent to (B � A).

Corollary 4.18 A sequent ⊢ Γ is provable in the system obtained by replacing ⊗ by ⊗3 in ncl augmented with additives and constants if and only if that sequent is provable in the system obtained by adding the unrestricted exchange rule to ncl augmented with additives and constants.

This corollary follows from the fact that the constants and additive connectives are inherently commutative, and may be proven by induction on the length of proofs.

4.6.2 Intermingling Cut

A problem similar to that which occurs with ⊗3 arises if we allow the Cut rule to interleave its conclusion. Define Cut2:

Cut2 \frac{⊢ Σ, A  ⊢ Γ, A^{⊥}}{⊢ Δ} where Δ is some interleaving of Σ and Γ

As for the previous alteration, the system ncl with Cut replaced by Cut2 would be commutative. We can achieve the effect of the unrestricted exchange rule using the Cut2 rule:

\begin{matrix}\underline{⋮ ; ⊢ Σ, Γ, A  ⋮ ; ⊢ A, A^{⊥}} & Cut2 \\ ⊢ Σ, A, Γ \end{matrix}

Note that for any formula A, there is always a proof of ⊢ A, A^{⊥} in noncommutative (as well as commutative) linear logic. The above partial deduction shows that unrestricted exchange may be simulated in noncommutative linear logic with Cut replaced by Cut2. Somewhat more concretely, the following shows a deduction of a sequent which is not derivable in ncl:

\underline{\underline{\overline{⊢ p_{1}, p_{1}^{⊥}}^{I} \overline{⊢ p_{2}, p_{2}^{⊥}}^{I}}_{⊗} ; ⊢ p_{1}, (p_{1}^{⊥} ⊗ p_{2}^{⊥}), p_{2} \overline{⊢ p_{1}, p_{1}^{⊥}}^{I}}_{Cut2} ; ⊢ (p_{1}^{⊥} ⊗ p_{2}^{⊥}), p_{1}, p_{2}

Notice in the final conclusion that p_{1} and p_{2} have changed places, in a way impossible without the use of the Cut2 rule in ncl. Thus using Cut2 we could prove any sequent which is provable in the commutative fragment of linear logic corresponding to ncl. However, it would be impossible to prove some such sequents in ncl without Cut2, and thus cut-elimination fails in this logic.

However, since there is a proof of a sequent in this logic if and only if there is a proof of that sequent in (commutative) linear logic, we may as well use linear logic, which does have a cut-elimination theorem.

The Multiplicative Fragment

We now consider the fragment of linear logic which includes only the multiplicative connectives. In Section 5.1, we show that the decision problem for this fragment is in np, and in Section 5.2 we show that the multiplicative fragment with a rule of unrestricted weakening is np-complete.

5.1 Multiplicatives

We have two results which characterize the complexity of this fragment incompletely. The exact complexity of this fragment is one of the significant open problems. In short, we find that this fragment is in np, and if we introduce the structural rule of unrestricted weakening into this fragment, it becomes np-complete.

The pure multiplicative fragment (without additive connectives or storage operators) is the simplest fragment of linear logic that we have investigated.

Theorem 5.1 Multiplicative linear logic is in np.

Proof. The proof is straightforward: Each connective in the conclusion sequent is the principal connective in exactly one proof step in any cut-free proof, thus giving a polynomial bound on the size of cut-free proofs. Thus the entire proof may be guessed in polynomial time.

5.2 Direct Logic

We have been unable to prove the multiplicative fragment of linear logic np-complete. We now believe that this may be difficult, due to the lack of redundancy in this problem statement [GJ79]. As part of our investigation of the need to discard arbitrary resources to achieve np-completeness, we studied propositional multiplicative linear logic with unrestricted weakening, but without contraction. We will call this direct logic or dl, as it is similar to the direct logic of [KW84]. dl is also considered in considerable detail in Bellin [Bel90]. The rules for this system are the identity and cut rules, the rules for the multiplicatives, constants, and the structural rule W of unrestricted weakening.

W \frac{⊢ Σ}{⊢ A, Σ}

We first demonstrate cut-elimination for dl, yielding consistency, which will facilitate our later proof of NP-completeness.

Lemma 5.2 A sequent is provable in dl if and only if it is provable in dl without using the cut rule.

Proof. This lemma, as the cut-elimination theorem for full linear logic, is proven by giving a cut-elimination procedure. This procedure takes any proof as input, and produces a cut-free proof of the same sequent.

We modify the procedure given in Appendix A. More specifically, we modify the procedure given in Lemma A.1 to handle the extra cases brought about by the presence of weakening, and we define the formula A in the above presentation of W to be the principal formula of W.

Thus we need to present two reductions, one in the case that the cut formula is principal, and in case it is not principal.

We will follow the notation used in Appendix A, where Cut∗ is used to ambiguously refer to the Cut rule or the extra rule of inference introduced in the appendix called Cut!.

First, we consider the non-principal W case:

\underline{⋮ ; ⊢ Σ, A ; \overline{⊢ Σ, A, B}^{W} ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}
⊢ Σ, Γ, B

⟹ \underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}

(⊢ Σ, Γ) / (\overline{⊢ Σ, Γ, B}^{W})

The above reduction is very similar to the case of non-principal ?W.

In the case of principal W, we have the following reduction:

\underline{⋮ ; ⊢ Σ ; \overline{⊢ Σ, A}^{W} ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}
⊢ Σ, Γ

⟹

⋮ ; \underline{⊢ Σ}_{W} ; ⋮ ; \overline{⊢ Σ, Γ}^{W}

By combining these two reductions with the procedure given in Lemma A.1, we have a cut-reduction lemma for dl.

Fortunately, Lemma A.2 and Theorem A.3 then follow without modification. Formally, we must show that although the lemmas in Appendix A apply to full linear logic, they would not take a proof in dl into a proof outside dl. By inspection of the reductions used for the subset of the connectives of dl, we see that this holds.

Therefore, given any dl proof of sequent ⊢ Γ in theory T, we can construct a cut-free proof of ⊢ Γ in theory T.

Lemma 5.3 The provability problem for dl is in np.

Proof. The membership in np of the provability problem for dl follows from a polynomial bound on the size of cut-free dl proofs. Each subformula occurrence in the conclusion is analyzed in at most one rule application in any cut-free proof of that conclusion. Thus, given a provable sequent, it is possible to nondeterministically generate and check a cut-free proof in polynomial time.

The proof of the np-hardness of provability for dl is obtained by a transformation from the Vertex Cover problem which can be stated as: Given a graph G = (V, E) and a bound k, find a subset U of k or fewer vertices from V such that every edge in E is incident on some vertex in U. Given an instance of the Vertex Cover problem, we construct γ(V, E, k), a dl sequent which is provable exactly when (V, E) has a vertex cover of fewer than k vertices. Let deg(v, E) denote the degree of vertex v, i.e., the number of edges in E incident on v. The definition of γ is given by

γ(V, E, k) = ⊢ m^{k}, ϕ(V, E), ϵ(E)
ϕ(V, E) = � _{v∈V} (m^{⊥} ⊗ (\underbrace{x_{v}^{⊥} � … � x_{v}^{⊥}}_{deg(v,E)}))
ϵ(E) = ⊗_{(u,v)∈E}(x_{u} � x_{v})

For example, given V = {a, b, c, d} and E = {(a, b), (c, d), (b, c)}, and k = 2, the sequent γ(V, E, k) is

⊢ m, m,
m^{⊥} ⊗ x_{a}^{⊥}, m^{⊥} ⊗ (x_{b}^{⊥} � x_{b}^{⊥}), m^{⊥} ⊗ (x_{c}^{⊥} � x_{c}^{⊥}), m^{⊥} ⊗ x_{d}^{⊥},
(x_{a} � x_{b}) ⊗ (x_{c} � x_{d}) ⊗ (x_{b} � x_{c})

A vertex cover in this example is obviously {b, c}. The corresponding deduction in dl of γ(V, E, k) can be constructed in stages. In the first stage, the formula encoding vertices a and d are weakened and the formulas encoding vertices b and c are reduced as shown below.

\underline{\overline{⊢ m, m^{⊥}}^{I}  \begin{matrix}\underline{\overline{⊢ m, m^{⊥}}^{I}  ⋮ ; ⊢ x_{b}^{⊥}, x_{b}^{⊥}, x_{c}^{⊥}, x_{c}^{⊥}, ϵ(E) ; \overline{⊢ x_{b}^{⊥}, x_{b}^{⊥}, (x_{c}^{⊥} � x_{c}^{⊥}), ϵ(E)} ^{�} ; \overline{⊢ (x_{b}^{⊥} � x_{b}^{⊥}), (x_{c}^{⊥} � x_{c}^{⊥}), ϵ(E)} ^{�}} & ⊗ \\ ⊢ m, (x_{b}^{⊥} � x_{b}^{⊥}), m^{⊥} ⊗ (x_{c} � x_{c}), ϵ(E) \end{matrix}} _{⊗}

⊢ m, m, m^{⊥} ⊗ (x_{b}^{⊥} � x_{b}^{⊥}), m^{⊥} ⊗ (x_{c}^{⊥} � x_{c}^{⊥}), ϵ(E)
\overline{⊢ m, m, m^{⊥} ⊗ x_{a}^{⊥}, m^{⊥} ⊗ (x_{b}^{⊥} � x_{b}^{⊥}), m^{⊥} ⊗ (x_{c}^{⊥} � x_{c}^{⊥}), m^{⊥} ⊗ x_{d}^{⊥}, ϵ(E)} ^{W}

The remaining subgoal in the above deduction can be proved in the next stage. The vertex literals corresponding to the vertex cover can be paired off with literals in the edge encodings to demonstrate that there is at least one vertex literal for each edge.

\begin{matrix}\underline{\begin{matrix}\overline{⊢ x_{b}^{⊥}, x_{b}} & I \\ \overline{⊢ x_{b}^{⊥}, x_{a}, x_{b}} & W \\ \overline{⊢ x_{b}^{⊥}, (x_{a} � x_{b})} & � \end{matrix}  \begin{matrix}\underline{\begin{matrix}\overline{⊢ x_{c}^{⊥}, x_{c}} & I \\ \overline{⊢ x_{c}^{⊥}, x_{c}, x_{d}} & W \\ \overline{⊢ x_{c}^{⊥}(x_{c} � x_{d})} & � \end{matrix}  \begin{matrix}\overline{⊢ x_{b}^{⊥}, x_{b}} & I \\ \overline{⊢ x_{b}^{⊥}, x_{c}^{⊥}, x_{b}, x_{c}} & W \\ \overline{⊢ x_{b}^{⊥}, x_{c}^{⊥}, (x_{b} � x_{c})} & � \end{matrix}} & ⊗ \\ ⊢ x_{b}^{⊥}, x_{c}^{⊥}, x_{c}^{⊥}, (x_{c} � x_{d}) ⊗ (x_{b} � x_{c}) \end{matrix}} & ⊗ \\ ⊢ x_{b}^{⊥}, x_{b}^{⊥}, x_{c}^{⊥}, x_{c}^{⊥}, (x_{a} � x_{b}) ⊗ (x_{c} � x_{d}) ⊗ (x_{b} � x_{c}) \end{matrix}

The next three lemmas are stated without proof. They are used in the proof of Lemma 5.7 to establish that when a vertex cover for V,E, and k exists, then γ(V, E, k) is provable.

Lemma 5.4 If l ≤ k, then there exists a deduction of ⊢ m^{k}, Γ from ⊢ m^{l}, Γ.

Lemma 5.5 Given V, E, and U ⊆ V, let Γ be the multiset containing deg(u, E) occurrences of x_{u}^{⊥} for each u in U, and let l be |U|. There is a deduction of ⊢ m^{l}, ϕ(V, E), Δ from ⊢ Γ, Δ.

Lemma 5.6 If Γ is a multiset of literals such that for each (u, v) in E, there is a distinct occurrence of either x_{u}^{⊥} or x_{v}^{⊥} in Γ, then ⊢ Γ, ϵ(E) is provable.

Lemma 5.7 If G = (V, E) has a vertex cover U of k or fewer vertices, then γ(V, E, k) has a dl proof.

Proof. Let l = |U| be the cardinality of U. By Lemma 5.4 and the definition of γ, the required conclusion, ⊢ m^{k}, ϕ(V, E), ϵ(E), can be deduced from ⊢ m^{l}, ϕ(V, E), ϵ(E). Let Γ be the multiset of literals containing deg(u, E) occurrences of x_{u}^{⊥} for each u in U. By Lemma 5.5, there is a deduction of ⊢ m^{l}, ϕ(V, E), ϵ(E) from ⊢ Γ, ϵ(E). Since deg(u, E) is the number of occurrences of x_{u} in ϵ(E), the sequent ⊢ Γ, ϵ(E) is provable by Lemma 5.6.

Lemma 5.8 states some straightforward properties about weakening, and is given below without proof (see [Bel90], page 138). A formula occurrence is said to be weakened in a proof if it is the principal formula of an application of the weakening rule. The lemma essentially captures the idea that if all subformulas of a formula occurrence are weakened, then the formula itself can be weakened instead; and if even a single conjunct in a conjunction is weakened, then the entire conjunction can be weakened instead. Lemma 5.8 is used repeatedly in the proof of Theorem 5.9 to maximize the size of any formulas that are weakened in a proof.

Lemma 5.8 For any proof π in dl of a sequent ⊢ Γ, one can obtain a proof θ of ⊢ Γ such that

1. for any formula occurrence (A ⊗ B), neither A nor B is weakened in θ

2. for any formula occurrence (A � B), A and B are not both weakened in θ, and

3. any weakening of formula occurrences in Γ occurs below any application of non-weakening rules in θ.

Lemma 5.9 Given a graph G = (V, E) and a bound k, if γ(V, E, k) is provable in dl then G has a vertex cover of size less than k.

Proof. Given a proof of γ(V, E, k), first take the set U of vertices u such that ⊢ x_{u}, x_{u}^{⊥} is an axiom in the proof of γ(V, E, k). There are two possible ways in which U might not be a vertex cover. One way is if for some edge encoded by (x_{v} � x_{w}), neither x_{v} nor x_{w} appears in an axiom. Then the literals x_{u} and x_{v} must have been subformulas of some weakened formulas. By Lemma 5.8 the given proof can be transformed to one in which both x_{u} and x_{v} are not weakened, and neither is (x_{u} � x_{v}) since it is a conjunct. Therefore the entire edge encoding ϵ(E) would have to be weakened below any non-weakening rules, and as a result ⊢ m^{k}, ϕ(V, E) would have to be provable. Since ⊢ m^{k}, ϕ(V, E) contains no positive occurrences of literals x_{v} for v in V, a proof of ⊢ m^{k}, ϕ(V, E) cannot contain axioms of the form ⊢ x_{v}, x_{v}^{⊥}. Again, by Lemma 5.8, each formula in ϕ(V, E) must be weakened below any application of logical rules. Such a proof would contain a deduction of ⊢ m^{k}. However, ⊢ m^{k} is unprovable for any k, contradicting the assumption that ⊢ γ(V, E, k) is provable.

The only remaining way in which the set U with l = |U| might fail to be a vertex cover is if l > k. The negative literals x_{v}^{⊥} in axioms ⊢ x_{v}, x_{v}^{⊥} only occur in the formulas in ϕ(V, E). By Lemma 5.8, the given proof can be transformed to a proof θ in which l of the formulas in ϕ(V, E) are not weakened, because each formula in ϕ(V, E) contributes at most one vertex to the set U. Since each unweakened formula in ϕ(V, E) is of the form m^{⊥} ⊗ A for some A, Lemma 5.8 implies that θ contains at least l axioms of the form ⊢ m, m^{⊥}. However, there are only k positive occurrences of the literal m in the conclusion sequent ⊢ γ(V, E, k), and each occurrence can appear in at most one axiom of the form ⊢ m, m^{⊥}, thus contradicting the claim that l > k.

Therefore, the construction of U from a dl proof of ⊢ γ(V, E, k) does yield a vertex cover for G = (V, E) of size bounded by k.

The encoding γ transforming an instance of the Vertex Cover problem to the provability of a dl sequent is clearly of polynomial complexity. Together, Lemmas 5.7 and 5.9 yield the following result.

Theorem 5.10 Multiplicative linear logic with unrestricted weakening is np-complete.

In this reduction, weakening appears essential since an edge may be covered by selecting one endpoint or both, and weakening allows both cases to succeed. Only with additives would it be possible to encode such behavior in linear logic, and including the additives would take dl out of np. In fact, dl with additive connectives becomes pspace-complete.

Conclusion

We have investigated the complexity of the provability problem for several fragments of propositional linear logic. Our most significant results are that provability for full propositional linear logic is undecidable, but that provability becomes pspace-complete when the modal storage operator is removed. One may view these results in terms of the non-modal multiplicative-additive linear logic as the facts that provability in this logic without non-logical axioms is pspace-complete, and with non-logical axioms provability becomes undecidable. In fact, even if the nonlogical axioms are of an extremely restricted class, the provability problem remains undecidable.

These results point out the greater complexity inherent in linear logic, when compared with classical or intuitionistic logic. This extra complexity is the price one should expect to pay in a logic as detailed, or as specific, as linear logic. In fact, we show that linear logic is a computational logic. That is, linear logic can exactly represent computations, to the point where not only is there a correspondence between derivable conclusions and machine configurations that eventually reach an accepting state, but there is an exact correspondence between (standardized) proofs and accepting computations.

We have also shown that provability for the non-commutative fragment of linear logic (even without additive connectives) is also undecidable. Finally, we show that the decision problem for the multiplicative fragment is in np, and becomes np-complete in the presence of unrestricted weakening.

Although we have gained some insight into the expressive power and combinatorial properties of propositional linear logic, some open problems remain. We have been unable to establish tight bounds for the multiplicative fragment or settle the decidability of the multiplicatives with the ! operator. This seems particularly difficult, since a positive solution would involve an extension of the reachability algorithm for Petri nets. The other open problem of interest to us is the decidability of various fragments of linear logic without the modal operators ? and !, and without non-logical axioms, extended with propositional quantifiers.

Acknowledgements

We would like to thank the Stanford Center for Study of Language and Information, and the SRI Computer Science Laboratory for supportive working environments. Thanks also to Jean-Yves Girard, Alasdair Urquhart, Gian Luigi Bellin, and Grigori Mints for stimulating discussion and correspondence. Tim Winkler of the SRI Computer Science Laboratory helped with the typesetting of the � connective. David Israel, Peter Neumann, and Narciso Martí-Oliet carefully read drafts of the report and provided several constructive comments.

Patrick Lincoln is supported by an AT&T Bell Laboratories graduate fellowship and by the SRI Computer Science Laboratory (summers of 1989 and 1990). John Mitchell is supported by an NSF PYI Award, matching funds from Digital Equipment Corporation, Powell Foundation, Xerox Corporation; NSF grant CCR-8814921, and Wallace F. and Lucille M. Davis Faculty Scholarship. Andre Scedrov is partially supported by NSF Grant CCR-87-05596, by ONR Grant NOOO14-88-K-0635 and by the 1987 Young Scientist Award from the Natural Sciences Association of the University of Pennsylvania. During his 1989-90 sabbatical at Stanford, Scedrov was also partially supported by Mitchell’s PYI-related funds. Natarajan Shankar is supported by the SRI Computer Science Laboratory.

Bibliography

[AFG90] A. Asperti, G.-L. Ferrari, and R. Gorrieri. Implicative formulae in the ‘proofs as computations’ analogy. In Proc. 17-th ACM Symp. on Principles of Programming Languages, San Francisco, pages 59–71, January 1990.

[AP90] J.-M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. In Proc. 7-th International Conference on Logic Programming, Jerusalem, May 1990.

[Asp87] A. Asperti. A logic for concurrency. Technical report, Dipartimento di Informatica, Universitá di Pisa, 1987.

[AV90] S. Abramsky and S. Vickers. Quantales, observational logic, and process semantics. Preprint, January 1990.

[Avr88] A. Avron. The semantics and proof theory of linear logic. Theoretical Computer Science, 57:161–184, 1988.

[Baw86] A. Bawden. Connection graphs. In Proc. ACM Symp. on Lisp and Functional Programming, pages 258–265, 1986.

[Bel90] G. Bellin. Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information. PhD thesis, Stanford University, 1990.

[Cer90] S. Cerrito. A linear semantics for allowed logic programs. In Proc. 5th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[CKS81] A.K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, 1981.

[Clo86] P. Clote. On the finite containment problem for Petri nets. Theoretical Computer Science, 43:99–105, 1986.

[DR89] V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.

[Gen69] G. Gentzen. Collected Works. Edited by M.E. Szabo. North-Holland, Amsterdam, 1969.

[GG89] C.A. Gunter and V. Gehlot. Nets as tensor theories. In G. De Michelis, editor, Proc. 10-th International Conference on Application and Theory of Petri Nets, Bonn, pages 174–191, 1989.

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

[GH90] J.C. Guzman and P. Hudak. Single-threaded polymorphic lambda calculus. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

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

[Gir87b] J.-Y. Girard. Multiplicatives. Rendiconti del Seminario Matematico dell’ Universitá e Politecnico Torino, Special Issue on Logic and Computer Science, pages 11–33, 1987.

[Gir89] J.-Y. Girard. Towards a geometry of interaction. In: Contemporary Math. 92, Amer. Math. Soc., 1989. 69-108.

[Gir90] J.-Y. Girard. La logique linéaire. Pour La Science, Édition Francaise de Scientific American, 150:74–85, April 1990.

[GJ79] M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., 1979.

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

[GSS90] J.-Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic: A modular approach to polynomial time computability. In Proc. Math. Sci. Institute Workshop on Feasible Mathematics, Cornell University, June, 1988. Birkhauser, 1990.

[HS86] J.R. Hindley and J.P. Seldin. Introduction to Combinators and Lambda Calculus. London Mathematical Society Student Texts, Cambridge University Press, 1986.

[HU79] J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley Publishing Company, 1979.

[Kos82] S.R. Kosaraju. Decidability of reachability in vector addition systems. In Proc. 14-th ACM Symp. on Theory of Computing, pages 267–281, 1982.

[KW84] J. Ketonen and R. Weyhrauch. A decidable fragment of predicate calculus. Theoretical Computer Science, 32, 1984.

[Laf88] Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.

[Laf90] Y. Lafont. Interaction nets. In Proc. 17-th ACM Symp. on Principles of Programming Languages, San Francisco, pages 95–108, January 1990.

[Lam58] J. Lambek. The mathematics of sentence structure. Amer. Math. Monthly, 65:154–169, 1958.

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

[Lip76] R. Lipton. The reachability problem is exponential-space hard. Technical Report 62, Department of Computer Science, Yale University, January 1976.

[LMSS90] P. Lincoln, J.C. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. In Proc. 31st IEEE Symp. on Foundations of Computer Science, pages 662–671, 1990.

[May81] E.W. Mayr. An algorithm for the general Petri net reachability problem. In Proc. 13-th ACM Symp. on Theory of Computing, Milwaukee, pages 238–246, 1981.

[McA84] K. McAloon. Petri nets and large sets. Theoretical Computer Science, 32:173–183, 1984.

[Mey66] R.K. Meyer. Topics in Modal and Many-Valued Logic. PhD thesis, University of Pittsburgh, 1966.

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

[MM82] E. Mayr and A. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46:305–329, 1982.

[MOM89] N. Martí-Oliet and J. Meseguer. From Petri nets to linear logic. In: Springer LNCS 389, ed. by D.H. Pitt et al., 1989. 313-340.

[Pos47] E.L. Post. Recursive unsolvability of a problem of Thue. Journal of Symbolic Logic, 12:1–11, 1947.

[Sce90] A. Scedrov. A brief guide to linear logic. Bulletin of the European Assoc. for Theoretical Computer Science, 41:154–165, June 1990.

[Urq84] A. Urquhart. The undecidability of entailment and relevant implication. Journal of Symbolic Logic, 49:1059–1073, 1984.

[Yet90] D.N. Yetter. Quantales and (noncommutative) linear logic. Journal of Symbolic Logic, 55:41–64, 1990.

Appendix A

Cut Elimination

The cut-elimination theorem, in general, states that whatever can be proven in the full version of a logic may also be proven without the use of the cut rule. This theorem is fundamental to linear logic, and was proven by Girard shortly after the introduction of the logic by presenting a cut-elimination procedure for proof nets [Gir87a]. In our proof of undecidability, we make use of the syntax, or exact form of a cut-elimination procedure for the sequent calculus formulation of linear logic. Since Girard demonstrated the correspondence between proof nets and the sequent calculus presentation of linear logic, we could have relied on Girard’s proof of cut-elimination. However, for the purposes of our undecidability proof, and other results, it is much more clear to present a cut-elimination procedure native to the sequent calculus.

The following demonstration of the cut-elimination theorem consists of a linear logic proof normalization procedure which slowly eliminates cuts from any linear logic proof. The procedure may greatly increase the size of the proof, although of course it will still be a proof of the same sequent. For technical reasons, we add a derived rule of inference, Cut!, which simplifies the proof of termination. We then give a set of reductions which apply to proofs which end in Cut or Cut!, and using these we eliminate all uses of Cut and Cut! from a proof.

The proof structure is very close to the well known proofs of cut-elimination in classical logic [GLT89], but is complicated by the extra information which must be preserved in a linear proof. The Cut! rule defined below is reminiscent of Gentzen’s MIX rule [Gen69], and serves the same purpose, which is to package together inference rules. As in Gentzen’s work, we add this extra rule, and then show that it (along with Cut) may be eliminated entirely from any proof. Thus we show that this new rule and Cut are redundant in linear logic.

Let us begin with some definitions. First, we define the following new rule of inference,

Cut! \frac{⊢ Σ, (?A)^{n}  ⊢ Δ,!A^{⊥}}{⊢ Σ, Δ} n ≥ 1

(?A)^{n} is meant to denote a multiset of formulas. For example, (?A)^{3} =?A,?A,?A. As stated in the side condition, the Cut! rule is only applicable when n is at least 1. This rule of inference is derivable; that is, it may be simulated by several applications of contraction (?C) on the left hypothesis and then one application of the standard Cut rule. The original Cut rule and Cut! coincide when n = 1. Adding this extra derived rule of inference simplifies the termination argument substantially by packaging together some number of contractions with the cut that eliminates the contracted formula. This package is only opened when the contracted formulas are actually used with the application of the ?D rule, thrown away by the ?W rule, or split into two packages by the ⊗ and Cut∗ rules. We will use the symbol “Cut∗” as a general term for the original Cut rule and the new Cut! rule ambiguously.

We will call a formula which appears in a hypothesis of an application of Cut or Cut!, but which does not occur in the conclusion a cut-formula. In the list of linear logic rules in Appendix B the cut-formulas in the Cut rule are the formulas named A and A^{⊥}, and in the Cut! rule above, the cut-formulas are ?A and !A^{⊥}.

We also define the degree of a Cut or Cut! to be the number of symbols in its cut-formulas. For concreteness, we define here what is meant by number of symbols. We will consider each propositional symbol p_{i} to be a single symbol. We also consider the negation of each propositional symbol p_{i}^{⊥} to be a single symbol. Finally, we count each connective and constant, ⊗, � , ⊕, &,?,!, 1, ⊥, 0, ⊤, as a single symbol, but do not count parentheses. It is important to note that negation is defined, and therefore is not a connective. This method of accounting has the pleasant property that any linear logic formula A and its negation A^{⊥} have exactly the same number of symbols. (One may prove this by simple induction on the structure of the formula A). Thus it does not matter which cut-formula we count when determining the degree of a cut. We also define the degree of a proof to be the maximum degree of any cut in the proof, or zero if there are no cuts.

The principal formula of an application of an inference rule is usually defined to be any formula which is introduced by that rule. For example, the formula (A⊗B) is the principal formula of the ⊗ rule, since that is the formula which is introduced by that rule. We follow the standard convention of considering the contracted formula in an application of ?C principal, even though it is not introduced by the rule. For convenience, we extend the notion of principal formula in the following nonstandard ways. We will consider any formula beginning with ? appearing in the conclusion of the !S, ⊗, Cut, or Cut! rules to be principal. By this definition all formulas in the conclusion of !S are principal, and the only rule in which a formula beginning with ! may be principal is !S. This definition of principal formula simplifies the structure of the following proof somewhat.

Operationally, the cut-elimination procedure defined below first finds one of the “highest” cuts of maximal degree in the proof. That is, an application of Cut∗ (Cut or Cut!) for which all applications of Cut∗ in the derivation of either hypothesis is of smaller degree. Then a reduction is applied to that occurrence of Cut∗, which simplifies or eliminates it, although it may replicate some other portions of the original proof. We iterate this procedure to remove all cuts of some degree, and then iterate the entire procedure to eliminate all cuts. In this way, any linear logic proof may be normalized into one without any uses of the Cut or Cut! rules, at the possible expense of an (worse than) exponential blowup in the size of the resulting proof tree.

Technically, we begin with a lemma which constitutes the heart of the proof of cut-elimination. Although the proof of this lemma is rather lengthy, the reasoning is straightforward, and the remainder of the proof of cut-elimination is quite simple.

Lemma A.1 (Reduce One Cut) Given a proof of the sequent ⊢ Γ in linear logic which ends in an application of Cut∗ of degree d > 0, and where the degree of the proofs of both hypothesis is less than d, we may construct a proof of ⊢ Γ in linear logic of degree less than d.

Proof. By induction on the number of proof rules applied in the derivation of ⊢ Γ.

Given a derivation which ends in a Cut∗, we perform case analysis on the rules which were applied immediately above the Cut∗. One of the following cases must apply to any such derivation:

1. The cut-formula is not principal in one or both hypotheses.

2. The cut-formula is principal in both hypotheses.

In each case we will provide a reduction, which may eliminate the cut entirely, or replace it with one or two smaller cuts. Since this is a proof by induction on the size of a derivation, one may view this proof as a procedure which pushes applications of Cut∗ of large degree up a derivation. Informally, this procedure pushes applications of Cut∗ up through proof rules where the cut-formula is non-principal, until the critical point is reached where the cut-formula is principal in both hypotheses. In Girard’s proof of cut-elimination for linear logic using proof nets, the non-principal cases are circumvented by following proof links. In both approaches, however, the principal cases require significant detailed analysis.

A.1 Cut of non-principal formulas

If the derivation of a hypothesis ends in a rule yielding a non-principal cut-formula, then the rule must be one of the following: ⊗, � , ⊕, &, ?W, ?C, ?D, ⊥, ⊤, or Cut∗. The rules I, !S, and 1 are absent since those rules have no non-principal formulas in their conclusions. The later analysis of principal formula cuts considers these three cases.

A.1.1 ⊗

If the last rule applied in one hypothesis is ⊗, the cut-formula is not the main formula introduced by that application of ⊗, and the cut-formula does not begin with ?, then we may propagate the Cut∗ upward, through the application of ⊗:

\underline{\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ B, Δ, C} & ⊗ \\ ⊢ Σ, (A ⊗ B), Δ, C \end{matrix} ⋮ ; ⊢ Γ, C^{⊥}} _{Cut}
⊢ Σ, (A ⊗ B), Δ, Γ

⟹ ⋮ ; ⊢ Σ, A  \begin{matrix}\underline{⋮ ; ⊢ B, Δ, C  ⋮ ; ⊢ Γ, C^{⊥}} & Cut \\ ⊢ B, Δ, Γ \end{matrix} ⊗

⊢ Σ, (A ⊗ B), Δ, Γ

For the rules such as ⊗ with two hypotheses, we give the reduction for the case where the non-principal cut-formula appears in the right hand hypothesis of the ⊗ rule, and appears in one specific position in that sequent. The symmetric case of the cutformula appearing in the left hand hypothesis is very similar, and is always omitted. Since some notion of exchange is built-in to the system, sequents are considered multisets. Thus the exact position of formulas in sequents is unimportant. (Note that in noncommutative linear logic the relative position becomes vitally important.)

The proof ending in Cut after this transformation is smaller than the original proof, since the entire proof of ⊢ Σ, A, and the last application of ⊗ are no longer above the Cut. Thus by induction on the size of proofs, we can construct the desired proof of degree less than d.

Note that the Cut! rule only applies to formulas which begin with ?, and thus this reduction, which is only used if the cut-formula does not begin with ?, applies only to Cut and not to Cut!. Thus, we have disambiguated this case, and write only of Cut, where we present tranformations later in terms of Cut∗, in order to cover both possibilities simultaneously. The reduction given later (in Section A.2.9) handles the case of Cut!.

A.1.2 �

If the last rule applied in one hypothesis is � , and the cut-formula is not the main formula introduced by that application of � , then we may propagate the Cut∗ upward, through the application of � :

\underline{⋮ ; ⊢ Σ, A, B, C ; \overline{⊢ Σ, (A � B), C} ^{�}  ⋮ ; ⊢ Γ, C^{⊥}} _{Cut∗}
⊢ Σ, (A � B), Γ

⟹ \underline{⋮ ; ⊢ Σ, A, B, C  ⋮ ; ⊢ Γ, C^{⊥}} _{Cut∗}

⊢ Σ, A, B, Γ
\overline{⊢ Σ, (A � B), Γ} ^{�}

Again, the proof above the Cut∗ is smaller after this transformation, and thus by induction we have our result.

A.1.3 ⊕

Applications of Cut∗ involving the two symmetric ⊕ rules (where the cut-formula is not principle, that is, not introduced by this application of ⊕) may be eliminated in similar ways:

\underline{⋮ ; ⊢ Σ, A, C ; \overline{⊢ Σ, (A ⊕ B), C}^{⊕}  ⋮ ; ⊢ Γ, C^{⊥}} _{Cut∗}
⊢ Σ, (A ⊕ B), Γ

⟹ \underline{⋮ ; ⊢ Σ, A, C  ⋮ ; ⊢ Γ, C^{⊥}} _{Cut∗}

⊢ Σ, A, Γ
\overline{⊢ Σ, (A ⊕ B), Γ}^{⊕}

The second case of this rule is the same except the conclusion would contain the formula (B ⊕ A), instead of the formula (A ⊕ B) seen above.

A.1.4 &

It is the elimination of this type of cut (among others) which may lead to an exponential blowup in the size of cut-free proofs. The only other cut-elimination steps which may lead to a proof expansion are those involving !S.

\underline{\begin{matrix}\underline{⋮ ; ⊢ Σ, A, C ⋮ ; ⊢ Σ, B, C} & & \\ ⊢ Σ, (A&B), C \end{matrix} ⋮ ; ⊢ Γ, C^{⊥}} _{Cut∗}
⊢ Σ, (A&B), Γ
⇓

\begin{matrix}\underline{⋮ ; ⊢ Σ, A, C ⋮ ; ⊢ Γ, C^{⊥}} & Cut∗ \\ ⊢ Σ, A, Γ \end{matrix} \begin{matrix}\underline{⋮ ; ⊢ Σ, B, C ⋮ ; ⊢ Γ, C^{⊥}} & Cut∗ \\ ⊢ Σ, B, Γ \end{matrix} &
⊢ Σ, (A&B), Γ

The increase in proof size comes from replicating the entire proof tree above ⊢ Γ, C^{⊥}. Note that even though there are now two cuts instead of one, we may assume that both may be reduced in degree to less than d by induction on the size of the derivations. That is, there are fewer proof rules applied above each Cut∗ than there were above the single application of Cut∗ originally.

A.1.5 ?W

For this and the remaining cases, we omit discussion and simply indicate the reduction:

\underline{⋮ ; ⊢ Σ, A ; \overline{⊢ Σ, A,?B}^{?W} ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}
⊢ Σ, Γ,?B

⟹ \underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}

⊢ Σ, Γ
\overline{⊢ Σ, Γ,?B}^{?W}

A.1.6 ?C

\underline{⋮ ; \underline{⊢ Σ, A,?B,?B}_{?C} ; ⊢ Σ, A,?B ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}
⊢ Σ, Γ,?B

⟹ \underline{⋮ ; ⊢ Σ, A,?B,?B  ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}

\underline{⊢ Σ, Γ,?B,?B}_{?C}
⊢ Σ, Γ,?B

A.1.7 ?D

\underline{⋮ ; ⊢ Σ, A, B ; \overline{⊢ Σ, A,?B}^{?D} ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}
⊢ Σ, Γ,?B

⟹ \underline{⋮ ; ⊢ Σ, A, B  ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}

⊢ Σ, Γ, B
\overline{⊢ Σ, Γ,?B}^{?D}

A.1.8 ⊥

\underline{⋮ ; ⊢ Σ, A ; \overline{⊢ Σ, A, ⊥}^{⊥}  ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}
⊢ Σ, Γ, ⊥

⟹ \underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ Γ, A^{⊥}} _{Cut∗}

(⊢ Σ, Γ) / (\overline{⊢ Σ, Γ, ⊥}^{⊥})

A.1.9 ⊤

\begin{matrix}\underline{\overline{⊢ Σ, A, ⊤}^{⊤} ⋮ ; ⊢ Γ, A^{⊥}} & Cut∗ \\ ⊢ Σ, Γ, ⊤ \end{matrix}⟹ \overline{⊢ Σ, Γ, ⊤}^{⊤}

A.1.10 Cut

If the proof of one hypothesis ends in Cut∗, then we know that it has degree less than d. If the cut-formula of the lower degree d application of Cut∗ begins with ?, then it is considered principal (by definition) in the upper application of Cut∗, and will be handled in Section A.2.8. Otherwise, we know the formula does not begin with ?, and thus the lower Cut∗ must actually be Cut.

\begin{matrix}\underline{⋮ ; ⊢ Σ, A, C ⋮ ; ⊢ Γ, C^{⊥}} & Cut∗ \\ ⊢ Σ, A, Γ \end{matrix} ⋮ ; ⊢ Δ, A^{⊥} Cut
⊢ Σ, Δ, Γ

⟹

\begin{matrix}\underline{⋮ ; ⊢ Σ, A, C ⋮ ; ⊢ Δ, A^{⊥}} & Cut \\ ⊢ Σ, Δ, C \end{matrix} ⋮ ; ⊢ Γ, C^{⊥} Cut∗
⊢ Σ, Δ, Γ

Here we know that the number of symbols in the formula A is d, and the number of symbols in the formula C is less than d. Thus by induction we know that we can construct a proof of degree less than d of ⊢ Σ, Δ, C, and from that we can construct our desired proof of ⊢ Σ, Δ, Γ.

A.2 Cut of principal formulas

If the proof of each hypothesis ends in a rule with the cut formula as its principal formula, then the two last rules above the cut must be one of these combinations: I versus any, ⊗ versus � , ⊕ versus &, ?W versus !S, ?C versus !S, ?D versus !S, !S versus !S, Cut∗ versus !S, ⊗ versus !S, or ⊥ versus 1. Note that since there is no introduction rule for 0, the ⊤ rule cannot participate in a cut of principal formulas. Since all formulas in the conclusion of !S are considered principal, the analysis of !S at this stage of the proof is rather complex.

In many of these cases, we know that the Cut! rule is inapplicable, since the cut-formula has just been introduced, and it does not begin with a ?. When we know this, we will disambiguate the reduction, and show the applications of Cut and Cut! separately.

A.2.1 I versus any

If the last rule applied in either hypothesis is I (identity), then regardless of the rule applied in the other hypothesis we may remove the cut, and the application of identity:

\begin{matrix}\underline{\overline{⊢ p_{i}, p_{i}^{⊥}}^{I}  ⋮ ; ⊢ p_{i}, Γ} & Cut \\ ⊢ p_{i}, Γ \end{matrix}⟹ ⋮ ; ⊢ p_{i}, Γ

Note that the identity axiom only applies to atomic propositions, and thus we know that Cut! is inapplicable.

A.2.2 ⊗ versus �

\underline{\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ B, Δ} & ⊗ \\ ⊢ Σ, (A ⊗ B), Δ \end{matrix} ⋮ ; ⊢ Γ, B^{⊥}, A^{⊥} ; \overline{⊢ Γ, (B^{⊥} � A^{⊥})} ^{�}}_{Cut}
⊢ Σ, Γ, Δ
⇓

⋮ ; ⊢ Σ, A  \begin{matrix}\underline{⋮ ; ⊢ B, Δ  ⋮ ; ⊢ Γ, B^{⊥}, A^{⊥}} & Cut \\ ⊢ Γ, Δ, A^{⊥} \end{matrix} Cut
⊢ Γ, Δ, Σ

In this case, as in most of the principal formula cut-elimination steps, we need not appeal to the induction hypothesis of this lemma. We have eliminated the Cut of degree d, and replaced it with two applications of Cut of degree smaller than d.

A.2.3 & versus ⊕

\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ Σ, B} & & \\ ⊢ Σ, (A&B) \end{matrix} ⋮ ; ⊢ Γ, A^{⊥} ; \overline{⊢ Γ, (A^{⊥} ⊕ B^{⊥})}^{⊕} Cut
⊢ Σ, Γ

⟹ \begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ Γ, A^{⊥}} & Cut \\ ⊢ Σ, Γ \end{matrix}

The symmetric case of ⊕ is similar. Again, we need not appeal to the induction hypothesis, and the cut-formula does not begin with ?, and thus we know that Cut! does not apply.

A.2.4 ?W versus !S

For this and subsequent cases involving !S, ‘packaging’ is a useful analogy. We build packages containing a number of contractions and a single Cut! when we reduce principal cases involving ?C versus !S. We shrink the package in cases of ?W versus !S, and we actually use the contents of the package as cases of ?D versus !S. We let packages pass by each other at cases of !S versus !S, and at cases of Cut! versus !S and of ⊗ versus !S we break one package into two.

For this case, ?W versus !S, there are two possibilities, depending on whether the cut in question eliminates more than one occurrence of the cut-formula from the weakened sequent. Informally, the possibilities turn on whether there is only one thing in the package. If so, we don’t need the package. If there are more things in the package, we shrink the package.

In the first possibility, the cut eliminates the one occurrence of the cut-formula introduced by the ?W rule, and thus this application of cut may be eliminated entirely:

⋮ ; ⊢ Σ ; \overline{⊢ Σ,?A}^{?W} ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S} Cut∗
⊢ Σ,?Γ

⟹

⋮ ; \underline{⊢ Σ}_{?W} ; ⋮ ; \overline{⊢ Σ,?Γ}^{?W}

However, the second possibility, where the Cut∗ is actually a Cut! and eliminates more than one occurrence of the cut-formula from the weakened sequent, we perform the following reduction:

⋮ ; \underline{⊢ Σ, (?A)^{n−1}}_{?W} ; ⊢ Σ, (?A)^{n} ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S} Cut!
⊢ Σ,?Γ

⟹

\underline{⋮ ; ⊢ Σ, (?A)^{n−1} ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S}}_{Cut!}

⊢ Σ,?Γ

In the first possibility we have our result immediately, since the Cut∗ has been eliminated. In the second possibility, we appeal to the induction hypothesis.

A.2.5 ?C versus !S

In this case we make critical use of the Cut! rule. Without this extra rule of inference this reduction is especially difficult to formulate correctly, and the induction required is complicated.

⋮ ; \underline{⊢ Σ,?A,?A}_{?C} ; ⊢ Σ,?A ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S} Cut∗
⊢ Σ,?Γ

⟹

\underline{⋮ ; ⊢ Σ,?A,?A ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S}}_{Cut!}

⊢ Σ,?Γ

Here we know that the cut-formula begins with a ?, and thus Cut! may apply to it. We thus produce a Cut! regardless of whether the original Cut∗ was a Cut or a Cut!.

A.2.6 ?D versus !S

As for the previous ?W versus !S case, here we have two cases, depending on whether the Cut∗ in question eliminates more than one occurrence of the cut-formula from the derelicted sequent. Again, informally, the two cases turn on the size of the package. If there is only one thing in the package, we simple make use of it, and throw away the wrapping. If there are more thing in the package, we take one out, and move the smaller package along its way.

In the first case, the cut eliminates the one occurrence of the cut-formula introduced by the ?D rule, and thus the following reduction applies:

⋮ ; ⊢ Σ, A ; \overline{⊢ Σ,?A}^{?D} ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S} Cut∗
⊢ Σ,?Γ
⇓
\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢?Γ, A^{⊥}} & Cut \\ ⊢ Σ,?Γ \end{matrix}

However, in the second case, where the cut is actually a Cut! and eliminates more than one occurrence of the cut-formula from the derelicted sequent, we perform the following reduction:

⋮ ; \underline{⊢ Σ,?A^{n−1}, A}_{?D} ; ⊢ Σ,?A^{n} ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S} Cut!
⊢ Σ,?Γ

⟹

\underline{⋮ ; ⊢ Σ,?A^{n−1}, A  ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S}}_{Cut!}
⊢ Σ,?Γ, A

⋮ ⊢?Γ, A^{⊥}

Cut

\underline{⊢ Σ,?Γ,?Γ}_{?C}
⋮
\overline{⊢ Σ,?Γ}^{?C}

Note that the second case requires the duplication of the proof above the application of !S. Since A has fewer symbols than ?A, the lower Cut in the second case is of degree smaller than d. By induction, we may assume that the upper application of Cut! is reducible in degree.

A.2.7 !S versus !S

⋮ ; ⊢?Σ,?A, B ; \overline{⊢?Σ,?A,!B}^{!S}  ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S} Cut∗
⊢?Σ,?Γ,!B

⟹ \underline{⋮ ; ⊢?Σ,?A, B ⋮ ; ⊢?Γ, A^{⊥} ; \overline{⊢?Γ,!A^{⊥}}^{!S}}_{Cut∗}

(⊢?Σ,?Γ, B) / (\overline{⊢?Σ,?Γ,!B}^{!S})

Here we appeal to the induction hypothesis to produce a proof degree less than d of ⊢?Σ,?Γ, B, and then construct the desired proof from that.

A.2.8 Cut∗ versus !S

There are two possibilities here, which correspond to whether it is necessary to split a package into two pieces. The case where the package needs to be split is one of the most tricky aspects of the entire cut-elimination procedure.

If the lower application of Cut∗ is applied to formulas which may all be found in one hypothesis of the upper application of Cut∗, then we apply the same reduction as in the non-principal Cut case (Section A.1.10):

\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ Δ, (?C)^{n}, A^{⊥}} & Cut∗ \\ ⊢ Σ, Δ, (?C)^{n} \end{matrix} ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S} Cut∗
⊢ Σ, Δ,?Γ
⇓

⋮ ⊢ Σ, A \underline{⋮ ; ⊢ Δ, (?C)^{n}, A^{⊥} ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S}}_{Cut∗}

⊢ Δ,?Γ, A^{⊥} Cut∗

⊢ Σ, Δ,?Γ

In the more complex case, when the cut-formulas descend from both hypotheses of the upper Cut∗,we use the following reduction:

\begin{matrix}\underline{⋮ ; ⊢ Σ,?C^{m}, A  ⋮ ; ⊢ Δ,?C^{n}, A^{⊥}} & Cut∗ \\ ⊢ Σ, Δ,?C^{n+m} \end{matrix}  ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S} Cut!
⊢ Σ, Δ,?Γ
⇓

\underline{⋮ ; ⊢ Σ,?C^{m}, A  ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S}}_{Cut!}
⊢ Σ,?Γ, A

\underline{⋮ ; ⊢ Δ,?C^{n}, A^{⊥}  ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S}}_{Cut!}

⊢ Δ,?Γ, A^{⊥} Cut∗

\underline{⊢ Σ,?Γ, Δ,?Γ,}_{?C}
⋮
\overline{⊢ Σ, Δ,?Γ,}^{?C}

A.2.9 ⊗ versus !S

There are two possibilities here, which correspond to whether it is necessary to split a package into two pieces. The case where the package needs to be split is again one of the most tricky aspects of the entire cut-elimination procedure.

If Cut∗ is applied to formulas which may all be found in one hypothesis of ⊗, then we apply the same reduction as in the non-principal ⊗ case (Section A.1.1):

\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ B, Δ, (?C)^{n}} & ⊗ \\ ⊢ Σ, (A ⊗ B), Δ, (?C)^{n} \end{matrix}  ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S} Cut∗
⊢ Σ, (A ⊗ B), Δ,?Γ
⇓

⋮ ⊢ Σ, A \underline{⋮ ; ⊢ B, Δ, (?C)^{n} ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S}}_{Cut∗}

⊢ B, Δ,?Γ ⊗

⊢ Σ, (A ⊗ B), Δ,?Γ

In the more complex case, when the cut-formulas descend from both hypotheses of ⊗, we use the following reduction to push the cut above the ⊗ rule.

\begin{matrix}\underline{⋮ ; ⊢ Σ,?C^{m}, A ⋮ ; ⊢ B, Δ,?C^{n}} & ⊗ \\ ⊢ Σ, (A ⊗ B), Δ,?C^{n+m} \end{matrix} ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S} Cut!
⊢ Σ, (A ⊗ B), Δ,?Γ
⇓

\underline{⋮ ; ⊢ Σ,?C^{m}, A ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S}}_{Cut!}
⊢ Σ,?Γ, A

\underline{⋮ ; ⊢ B, Δ,?C^{n}  ⋮ ; ⊢?Γ, C^{⊥} ; \overline{⊢?Γ,!C^{⊥}}^{!S}}_{Cut!}

⊢ B, Δ,?Γ ⊗

\underline{⊢ Σ,?Γ, (A ⊗ B), Δ,?Γ}_{?C}
⋮
\overline{⊢ Σ, (A ⊗ B), Δ,?Γ}^{?C}

A.2.10 ⊥ versus 1

\underline{\overline{⊢ 1}^{1} ⋮ ; ⊢ Γ ; \overline{⊢ ⊥, Γ}^{⊥}}_{Cut} ; ⊢ Γ⟹ ⋮ ; ⊢ Γ

Again, we know that the Cut∗ involved here is Cut, since the formula 1 was just introduced.

This exhausts all the cases.

Thus, we have a procedure which given a proof which ends in Cut∗ of degree d, and which has no applications of Cut∗ in the proof of either hypothesis of degree greater than or equal to d, produces a proof of degree less than d.

Lemma A.2 (Lower-Degree-Cuts) If a sequent is provable in linear logic with a proof of degree d > 0, then it is provable in linear logic with a proof of degree less than d.

Proof. By induction on the height of the derivation tree of the conclusion, we show that given any proof of degree d of ⊢ Γ in propositional linear logic, we may find a (possibly much larger) proof of ⊢ Γ in linear logic of degree less than d.

We examine the proof of ⊢ Γ. Since the degree of this proof is greater than zero, there must be some Cut∗ in the proof. If the last rule is not Cut∗, then by induction we may form proofs of its hypotheses of degree less than d. Applying the same rule to the resulting reduced degree hypotheses produces the desired proof of degree less than d.

In the case that the last rule is Cut∗, we have the following situation for some Σ and Δ which together (in multiset union) make up Γ:

\begin{matrix}\underline{⋮ ; ⊢ Σ, A  ⋮ ; ⊢ Δ, A^{⊥}} & Cut∗ \\ ⊢ Γ \end{matrix} where Σ ∪ Δ = Γ

By induction, we can produce proofs of ⊢ Σ, A and ⊢ Δ, A^{⊥} of degree less than d. By a single application of Lemma A.1 to the resulting proof constructed from the modified hypotheses, we obtain a proof of ⊢ Γ of degree less than d.

Theorem A.3 (Cut-Elimination) If a sequent is provable in linear logic, then it is provable in linear logic without using the Cut rule.

Proof. By induction on the degree of the assumed proof. We may apply Lemma A.2 at each inductive step, and at the base case the degree of the proof is zero, so therefore by definition of proof degree there are no cuts, and we have our desired cut-free proof.

Note that the proof can explode hyperexponentially in size during the cutelimination process.

A.3 Subformula Property

Above we have demonstrated that all cuts may be eliminated from a proof, at the possible expense of increasing the size of the proof hyperexponentially. This normalization is worthwhile, however, since it grants one various kinds of control over the form of proofs of given sequents. One of the finest forms of control, and historically the most important, is the subformula property.

The class of subformulas of a given formula or sequent is defined by the following: A is a subformula of A. If A is a subformula of B, then A is also a subformula of the following formulas: ?B, !B, B ⊗ C, C ⊗ B, B � C, C � B, B−∘C, and C−∘B. If A is a subformula of B, then A is also a subformula of the sequent ⊢ Γ_{1}, B, Γ_{2}.

Corollary A.4 (Subformula Property) Any formula in any cut-free proof of ⊢ Γ is a subformula of Γ.

Proof. Each rule of linear logic except Cut has the property that every subformula of the hypotheses is also a subformula of the conclusion. For example, in the ⊗ rule, any subformula of either hypothesis is either a subformula of Σ_{1}, A, B, or Σ_{2}. However, any such subformula is also a subformula of the conclusion. In fact, we may have “added” a subformula: (A ⊗ B) is a subformula of the conclusion, but might not be a subformula of the hypotheses.

Therefore, by induction on the size of proofs, we have that any subformula of any step of a cut-free proof of a sequent is a subformula of the original sequent.

It is easy to see that the subformula property is not true of proofs with cut: the subformulas A and A^{⊥} in the hypotheses of cut might not appear in the conclusion.

Appendix B

Propositional Linear Logic Proof Rules

A linear logic sequent is a ⊢ followed by a multiset of linear logic formulas. Note that in standard presentations of sequent calculi, sequents are often built from sets of formulas, where we use multisets here. This difference is crucial. We assume a set of propositions p_{i} given, along with their associated negations, p_{i}^{⊥}. Below we give the inference rules for the linear sequent calculus, along with the definition of negation and implication. The reader should note that negation is a defined concept, not an operator.

The following notational conventions are followed throughout this paper:

p_{i}  Positive propositional literal
p_{i}^{⊥}  Negative propositional literal
A, B, C  Arbitrary formulas
Σ, Γ, Δ  Arbitrary multisets of formulas

Thus the identity rule (I below) is restricted to atomic formulas, although in fact the identity rule for arbitrary formulas (⊢ A, A^{⊥}) is derivable in this system. For notational convenience, it is usually assumed that −∘ and ⊗ associate to the right, and that ⊗ has higher precedence than −∘. The notation ?Σ is used to denote a multiset of formulas which all begin with ?. The English names for the rules given below are identity, cut, tensor, par, plus, with, weakening, contraction, dereliction, storage, bottom, one, and top, respectively. Note that there is no rule for the 0 constant.

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

Cut  \frac{⊢ Σ, A  ⊢ Γ, A^{⊥}}{⊢ Σ, Γ}

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

�  \frac{⊢ Σ, A, B}{⊢ Σ, (A � B)}

⊕ \begin{aligned}⊢ Σ, A & ⊢ Σ, B \\ ⊢ Σ, (A ⊕ B) & ⊢ Σ, (A ⊕ B) \end{aligned}

&  \frac{⊢ Σ, A  ⊢ Σ, B}{⊢ Σ, (A & B)}

?W  \frac{⊢ Σ}{⊢ Σ,?A}

?C  \frac{⊢ Σ,?A,?A}{⊢ Σ,?A}

?D  \frac{⊢ Σ, A}{⊢ Σ,?A}

!S  \frac{⊢?Σ, A}{⊢?Σ,!A}

⊥  \frac{⊢ Σ}{⊢ Σ, ⊥}
1  \overline{⊢ 1}
⊤  \overline{⊢ Σ, ⊤}

Proof Rules 87 Linear negation is defined as follows:

(p_{i})^{⊥} =^{Δ} p_{i}^{⊥}
(p_{i}^{⊥})^{⊥} =^{Δ} p_{i}
(A ⊗ B)^{⊥} =^{Δ} B^{⊥} � A^{⊥}
(A � B)^{⊥} =^{Δ} B^{⊥} ⊗ A^{⊥}
(A ⊕ B)^{⊥} =^{Δ} A^{⊥} & B^{⊥}
(A & B)^{⊥} =^{Δ} A^{⊥} ⊕ B^{⊥}
(!A)^{⊥} =^{Δ} ?A^{⊥}
(?A)^{⊥} =^{Δ} !A^{⊥}
(1)^{⊥} =^{Δ} ⊥
(⊥)^{⊥} =^{Δ} 1
(0)^{⊥} =^{Δ} ⊤
(⊤)^{⊥} =^{Δ} 0

Linear implication, −∘, is defined as follows:

A−∘B =^{Δ} A^{⊥} � B