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. Since cut elimination implies the subformula property, all of the fundamental equivalences provable in full linear logic remain valid within such fragments, as soon as the formulas concerned belong to the fragment itself.

Conventionally, if $L L$ denotes full linear logic, its fragments are denoted by prefixing $L L$ 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, of 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 quantifiers, of whatever order (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 propositional linear logic (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 fragments

Multiplicative linear logic ( $M L L$ ) 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 $M L L$ 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 $M L L$ 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 $M L L$ is $\mathbf{NP}$ -complete, and it remains so even in presence of first order quantifiers.

Another multiplicative fragment, less considered in the literature, can be defined by using the units $\one$ and $\bot$ instead of the propositional atoms. In this fragment, denoted by $M L L u$ , one can also eliminate the $\rulename{axiom}$ rule from sequent calculus, since it is redundant. $M L L u$ is even simpler than $M L L$ : 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 $M L L$ and $M L L u$ is the full propositional multiplicative fragment of linear logic, and is denoted by $M L L 0$ . It has the same properties as $M L L$ , 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 $M L L$ (resp. $M L L u$ ), we obtain a system denoted by $M L L 2$ (resp. $M L L 02$ ). In $M L L 02$ 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, $M L L 2$ is as expressive as $M L L 02$ . In these second order fragments, provability is undecidable, while cut elimination is still $\mathbf P$ -complete.

Additive fragments

The most studied additive fragments of linear logic are defined by taking $M L L$ or $M L L 0$ and by enriching their language with the additive connectives, with or without units. The same can be done in presence of quantifiers. We thus obtain:

$M A L L$ : formulas built from propositional atoms using $\tens,\parr,\with,\plus$ ;
$M A L L 0$ : formulas built from propositional atoms and $\one,\bot,\top,\zero$ , using $\tens,\parr,\with,\plus$ ;
$M A L L n$ : $M A L L$ with quantifiers of order $n$ ;
$M A L L 0 n$ : $M A L L 0$ with quantifiers of order $n$ .

As for the multiplicative connectives, the additive connectives are also defined by their rules: adding a pair of dual connectives $\with',\plus'$ to $M A L L$ , and giving them the same rules as $\with,\plus$ , makes the new connectives provably equivalent to the old ones.

In $M A L L 02$ , the additive units $\top$ and $\zero$ are provably equivalent to $\exists X.X\orth$ and $\forall X.X$ , respectively. Since multiplicative units are also definable in terms of second order quantification, we obtain that $M A L L 2$ is as expressive as $M A L L 02$ .

The cut elimination problem is $\mathbf{coNP}$ -complete for all of the fragments defined above (Mairson-Terui).

Provability is undecidable in any additive fragment as soon as second order quantification is considered. It is decidable, although quite complex, in the propositional and first order case: it is $\mathbf{PSPACE}$ -complete in $M A L L 0$ , and $\mathbf{NEXP}$ -complete in $M A L L 01$ . This latter result is indicative of the fact that the undecidability of predicate calculus is not ascribable to existential quantification alone, but rather to the simultaneous presence of existential quantification and contraction.

Exponential fragments

The most common proper fragments of linear logic containing the exponential connectives are defined as in the case of the additive fragments, i.e., by adding the modalities on top of $M L L$ and its variants:

$M E L L$ : formulas built from propositional atoms using $\tens,\parr,\oc,\wn$ ;
$M E L L 0$ : formulas built from propositional atoms and $\one,\bot$ , using $\tens,\parr,\oc,\wn$ ;
$M E L L n$ : $M E L L$ with quantifiers of order $n$ ;
$M E L L 0 n$ : $M E L L 0$ with quantifiers of order $n$ .

If, instead of taking $M L L$ , we add the modalities to $M A L L$ , we obtain of course various versions of full linear logic:

$L L$ : full linear logic, without units;
$L L 0$ : full linear logic, with units;
$L L n$ : $L L$ with quantifiers of order $n$ ;
$L L 0 n$ : $L L 0$ with quantifiers of order $n$ .

In $L L 02$ the formulas $A\with B$ and $A\plus B$ are provably equivalent to $\exists X.(\oc{(X\orth\parr A)}\tens\oc{(X\orth\parr B)}\tens X)$ and $\forall X.(\wn{(X\orth\tens A)}\parr\wn{(X\orth \tens B)}\parr X)$ , respectively, for all $A, B$ . Thanks to the second-order definability of units discussed above, we obtain that $M E L L 2$ is as expressive as $L L 02$ , i.e., full propositional second order linear logic embeds in its second order multiplicative exponential fragment without units.

Girard showed how cut elimination for $L L 02$ without the contraction rule can be proved by a simple induction up to $ω$ , i.e., in first order Peano arithmetic. This gives a huge gap between the logical complexity of full linear logic and its contraction-free subsystem: in fact, still by Girard's results, we know that cut elimination in $M E L L 2$ is equivalent to the consistency of second order Peano arithmetic, for which no ordinal analysis exists. There are nevertheless subsystems of $M E L L 2$ , the so-called light subsystems of linear logic, in which the exponential connectives are weakened, whose cut elimination can be proved in seconder order Peano arithmetic even in presence of contraction.

The cut elimination problem is never elementary recursive in presence of exponential connectives: the simply typed $λ$ -calculus with arrow types only can be encoded in $M E L L$ , and this is enough for Statman's lower bound to apply. However, it becomes elementary recursive in the above mentioned light logics.

Albeit perhaps surprisingly, provability in $L L$ is already undecidable. This result, obtained by coding Minsky machines with linear logic formulas, contrasts with the situation in classical logic, whose propositional fragment is notoriously decidable. It is indicative of the fact that modalities are themselves a form of quantification, although this claim is far from being clear: as a matter of fact, the decidability of propositional provability in the absence of additives, i.e., in $M E L L$ alone, is still an open problem. It is known that adding first order quantification to $M E L L$ makes it undecidable.

About exponential rules

In this section, provability is assumed to be in $L L 02$ , i.e., full propositional second order linear logic.

In contrast with multiplicative and additive connectives, the modalities of linear logic are not defined by their rules: one may introduce a pair of dual modalities $\oc',\wn'$ , each with the same rules as $\oc,\wn$ , without $\oc'A$ (resp. $\wn'A$ ) being in general provably equivalent to $\oc A$ (resp. $\wn A$ ).

The promotion rule is derivable from the following two rules, called functorial promotion and digging, respectively:

$\AxRule{\vdash\Gamma,A} \LabelRule{f\oc} \UnaRule{\vdash\wn\Gamma,\oc A} \DisplayProof \qquad\qquad\qquad \AxRule{\vdash\Gamma,\wn{\wn A}} \LabelRule{dig} \UnaRule{\vdash\Gamma,\wn A} \DisplayProof$

Functorial promotion is itself derivable from dereliction and promotion; the digging rule is also derivable, but only using the $\rulename{cut}$ rule (in fact, digging does not enjoy the subformula property). It may be convenient to consider this pair of rules instead of the standard promotion rule in the context of categorical semantics of linear logic.

In presence of the digging rule, dereliction, weakening, and contraction can be derived from the following rule, called multiplexing, in which $A (n)$ stands for the sequence $A,\ldots,A$ containing $n$ occurrences of $A$ :

$\AxRule{\vdash\Gamma,A^{(n)}} \LabelRule{mux} \UnaRule{\vdash\Gamma,\wn A} \DisplayProof$

Of course, multiplexing is itself derivable from dereliction, weakening, and contraction. Hence, there are several alternative but equivalent presentations of the exponential fragment of linear logic, such as

remove promotion, and replace it with functorial promotion and digging;
remove promotion, dereliction, weakening, and contraction, and replace them with functorial promotion, digging, and multiplexing.

Apart from their usefulness in categorical semantics, these alternative formulations are of interest in the context of the so-called light linear logics mentioned above. For example, elementary linear logic is obtained by removing dereliction and digging from formulation 1, and soft linear logic is obtained by removing digging from formulation 2.

Multiplexing is invertible in certain circumstances. A sequent $\vdash\Gamma,\wn A$ containing no occurrence of $\with$ , $\oc$ , or second order $\exists$ is provable iff $\vdash\Gamma,A^{(n)}$ is provable for some $n$ (this is easily checked by induction on cut-free proofs). To see that this does not hold in general, take for instance $A=X\orth$ and $\Gamma=X\with\one$ , or $\Gamma=\oc X$ . The restriction on the presence of additive conjunction can be removed by slightly changing the statement: a sequent $\vdash\Gamma,\wn A$ containing no occurrence of $\oc$ or second order $\exists$ is provable iff $\vdash\Gamma,(A\plus\bot)^{(n)}$ is provable for some $n$ .

The latter result can be generalized as follows. If $A$ is a formula, $\oc_nA$ stands for the formula $(A\with\one)\tens\cdots\tens(A\with\one)$ ( $n$ times) and $\wn_nA$ for the formula $(A\plus\bot)\parr\cdots\parr(A\plus\bot)$ ( $n$ times). Then, we have

Theorem (Approximation Theorem)

Let $\vdash\Gamma$ be a provable sequent containing $p$ occurrences of $\oc$ , $q$ occurrences of $\wn$ , and no occurrence of second order $\exists$ . Then, for all $m_1,\ldots,m_p\in\mathbb N$ , there are $n_1,\ldots,n_q\in\mathbb N$ such that the sequent obtained from $\vdash\Gamma$ by replacing the $p$ occurrences of $\oc$ with $\oc_{m_1},\ldots,\oc_{m_p}$ and the $q$ occurrences of $\wn$ with $\wn_{n_1},\ldots,\wn_{n_q}$ is provable.

A structural formula is a formula $C$ such that $C\limp C\tens C$ and $C\limp\one$ are provable. Obviously, any formula of the form $\wn B$ is structural. However, the promotion rule cannot be extended to arbitrary structural formulas, i.e., the following rule is not admissible:

$\AxRule{C\vdash A} \AxRule{C\vdash C\tens C} \AxRule{C\vdash\one} \TriRule{C\vdash\oc A} \DisplayProof$

For instance, if $A=C=\alpha\tens\oc{(\alpha\limp\alpha\tens\alpha)}\tens\oc{(\alpha\limp\one)}$ , the three premises are provable but not the conclusion.

The following rule, called absorption, is derivable in the standard sequent calculus:

$\AxRule{\vdash\Gamma,\wn A,A} \UnaRule{\vdash\Gamma,\wn A} \DisplayProof$

The absorption rule is useful in the context of proof search in linear logic.

The provability problem

It is well known that the decidability of the provability problem is connected to the finite model property: if a fragment of a logic with a truth semantics enjoys the finite model property, then the provability in that fragment is decidable. Note of course that the converse may fail.

In this section, we summarize the known results about the validity of the final model property and the decidability of provability, with its complexity, for the various fragments of linear logic introduced above. Question marks in the tables below denote open problems. For brevity, all fragments are assumed to have units and propositional atoms, e.g., $M L L$ actually denotes what we called $M L L 0$ above.

The finite model property

$M L L$	$M A L L$	$M E L L$	$L L$
yes	yes	no	no

Provability

	$M L L$	$M A L L$	$M E L L$	$L L$
propositional case	$\mathbf{NP}$ -complete	$\mathbf{PSPACE}$ -complete	?	undecidable
first order case	$\mathbf{NP}$ -complete	$\mathbf{NEXP}$ -complete	undecidable	undecidable
second order case	undecidable	undecidable	undecidable	undecidable

The cut elimination problem

In this section, we summarize the known results about the complexity of the cut elimination problem for the various fragments of linear logic introduced above, plus some light linear logics. All fragments are assumed to be propositional; the results do not change in presence of quantification of any order.

$M L L u$	$M L L$	$M A L L$	$M S L L$	$M L L L$	$M E L L$
$\mathbf L$	$\mathbf{P}$ -complete	$\mathbf{coNP}$ -complete	$\mathbf{EXP}$ -complete	$\mathbf{2EXP}$ -complete	not elementary recursive

Notations used in the above table:

$M S L L$ : multiplicative soft linear logic;
$M L L L$ : multiplicative light linear logic.

Fragment

Contents

Motivations

Multiplicative fragments

Additive fragments

Exponential fragments

About exponential rules

The provability problem

The finite model property

Provability

The cut elimination problem

Views

Personal tools

Navigation

Search

Tools