Fragment

In general, a fragment of a logical system S is a logical system obtained by restricting the language of S, and by restricting the rules of S accordingly. In linear logic, the most well known fragments are obtained by combining/removing in different ways the classes of connectives present in the language of linear logic itself:

• Multiplicative connectives: the conjunction $\tens$ (tensor) and the disjunction $\parr$ (par), with their respective units $\one$ (one) and $\bot$ (bottom); these connectives are the combinatorial base of linear logic (permutations, circuits, etc.).
• Additive connectives: the conjunction $\with$ (with) and the disjunction $\plus$ (plus), with their respective units $\top$ (top) and $\zero$ (zero); the computational content of these connectives, which behave more closely to their intuitionistic counterparts (e.g., $A\with B\limp A$ and $A\with B\limp B$ are provable), is strongly related to choice (if...then...else, product and sum types, etc.).
• Exponential connectives: the modalities $\oc$ (of course) and $\wn$ (why not) handle the structural rules in linear logic, and are necessary to recover the expressive power of intuitionistic or classical logic.
• Quantifiers: just as in classical logic, quantifiers may be added to propositional linear logic, at any order. The most frequently considered are the second order ones (in analogy with System F).

The additive and exponential connectives, if taken alone, yield fragments of limited interest, so one usually considers only fragments containing at least the multiplicative connectives (perhaps without units). It is important to observe that the cut-elimination rules of linear logic do not introduce connectives belonging to a different class than that of the pair of dual formulas whose cut is being reduced. Hence, any fragment defined by combining the above classes will enjoy cut-elimination.

Conventionally, if LL denotes full linear logic, its fragments are denoted by prefixing LL with letters corresponding to the classes of connectives being considered: M for multiplicative connectives, A for additive connectives, and E for exponential connectives. Additional subscripts may specify whether units and/or quantifiers are present or not, and, for quantifiers, at what order (see the article on notations).

Motivations

The main interest of studying fragments of linear logic is that these are usually simpler than the whole system, so that certain properties may be first analyzed on fragments, and then extended or adapted to increasingly larger fragments. It may also be interesting to see, given a property that does not hold for full linear logic, whether it holds for a fragment, and where the "breaking point" is situated. Examples of such questions include:

• logical complexity: proving cut-elimination for full linear logic with second order quantification is equivalent to proving the consistency of second order Peano arithmetic (Girard, via translations of System F in linear logic). One may expect that smaller fragments have lower logical complexity.
• provability: the provability problem for a logical system S is defined as follows: given a formula A in the language of S, is A provable in S? This problem is undecidable in full linear logic with first order quantifiers (again, because classical logic can be translated in linear logic). On what fragments does it become decidable? And if it does, what is its computational complexity?
• computational complexity of cut-elimination: the cut-elimination problem (Mairson-Terui) for a logical system S is defined as follows: given two proofs of A in S, do they reduce to the same cut-free proof? Although decidable (thanks to strong normalization), this problem is not elementary recursive in full linear logic with first order quantification (Statman, again via the above-mentioned translations). Does the problem fall into any interesting complexity class when applied to fragments?
• proof nets: the definition of proof nets, and in particular the formulation of correctness criteria and the study of their complexity, is a good example of how a methodology can be applied to a small fragment of linear logic and later adapted (more or less successfully) to wider fragments.

Multiplicative linear logic

Multiplicative linear logic (MLL) is the simplest of the well known fragments of linear logic. Its formulas are obtained by combining propositional atoms with the connectives tensor and par only. As a consequence, the sequent calculus of MLL is limited to the rules $\rulename{axiom}$, $\rulename{cut}$, $\tens$, and $\parr$. These rules actually determine the multiplicative connectives: if a dual pair of connectives $\tens'$ and $\parr'$ is introduced, with the same rules as $\tens$ and $\parr$, respectively, then one can show $A\tens' B$ to be provably equivalent to $A\tens B$ (and, dually, $A\parr'B$ to be provably equivalent to $A\parr B$).

The cut-elimination problem for MLL is $\mathbf P$-complete (Mairson-Terui), even though there exists a deterministic algorithm solving the problem in logarithmic space if one considers only eta-expanded proofs (Mairson-Terui). On the other hand, provability for MLL is $\mathbf{NP}$-complete.

Another multiplicative fragment, less considered in the literarure, can be defined by using the units $\one$ and $\bot$ instead of the propositional atoms. In this fragment, denoted by MLL_u, one can also eliminate the $\rulename{axiom}$ rule from sequent calculus, since it is redundant. MLL_u is even simpler than MLL: its provability problem is in $\mathbf P$, and, since all proofs are eta-expandend, its cut-elimination problem is in $\mathbf L$.

The union of MLL and MLL_u is the full propositional multiplicative fragment of linear logic, and is denoted by MLL₀. It has the same properties as MLL, which shows that the presence/absence of propositional atoms (and of the $\rulename{axiom}$ rule) has a non-trivial effect on the complexity of provability and cut-elimination, i.e., the complexity is not altered iff $\mathbf P\subsetneq\mathbf{NP}$ and $\mathbf L\subsetneq\mathbf P$, respectively.

If we add second order quantifiers to MLL (resp. MLL_u), we obtain a system denoted by MLL₂ (resp. MLL₀₂). In MLL₀₂ one can show that $\one$ and $\bot$ are provably equivalent to $\forall X.(X\orth\parr X)$ and $\exists X.(X\orth\tens X)$, respectively. Hence, MLL₂ is as expressive as MLL₀₂.