Linear logic is a substructural logic proposed by French logician Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics (because linear logic can be seen as the logic of quantum information theory), as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.

Linear logic lends itself to many different presentations, explanations, and intuitions.

Proof-theoretically, it derives from an analysis of classical sequent calculus in which uses of (the structural rules) contraction and weakening are carefully controlled. Operationally, this means that logical deduction is no longer merely about an ever-expanding collection of persistent "truths", but also a way of manipulating resources that cannot always be duplicated or thrown away at will. In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian (closed) categories by symmetric monoidal (closed) categories, or the interpretation of classical logic by replacing Boolean algebras by C*-algebras.

Notation comparison

This article follows Girard's notation. For readers who are familiar with different notations, the following table, compiled by Paoli 2002, compares the notations for linear-logic connectives and constants across several sources.

{| class="wikitable" style="text-align:center; margin:auto;"

|-

! Girard 1987

! Restall 2000

! Paoli 2002

The main semantic approaches include:

; Phase semantics: An early model focusing on provability.

; Categorical semantics: An algebraic framework that models proofs as morphisms. The appropriate category is a subcategory of complete, separated, bornological vector space with continuous linear maps.

; Game semantics: An interactive model that interprets formulas as games and proofs as strategies.

; Denotational semantics: A model that interprets proofs as mathematical objects.

The algebraic semantics of linear logic is that of quantales.

In linguistics, linear logic models grammatical parsing as deduction. In that circumstance, a valid parse tree corresponds to proving the existence of a sentence using implication rules encoding the grammar.

The resource interpretation

Lafont (1993) first showed how intuitionistic linear logic can be explained as a logic of resources, so providing the logical language with access to formalisms that can be used for reasoning about resources within the logic itself, rather than, as in classical logic, by means of non-logical predicates and relations. Tony Hoare (1985) used purchases at a vending machine to illustrate the logic, and culinary transactions have become the traditional example to describe use of the connectives.

In particular, a prix fixe menu corresponds to a linear implication from the price to the meal; either

:(Cash) ⊸ (Meal)

or equivalently

:(Cash)<sup>⊥</sup> ⅋ (Meal)

depending on if implication or par is taken to be the primitive connective. Different courses are then conjoined using tensor, as a purchased meal is guaranteed to consist of both. For example, one might define (Meal) as

:(Meal) := (Appetizer) ⊗ (Main) ⊗ (Dessert) ⊗ (Drink)

The customer's choice is conjoined using &amp;:

:(Appetizer) := (Soup) &amp; (Salad)

indicating that the customer must choose either a soup or a salad. Contrariwise, the restaurant's choice is disjoined using ⊕: if the dessert is seasonal fruits, then it might be well-modeled as

:(Dessert) := (Summer berries) ⊕ (Apple slices) ⊕ (Winter pineapple) ⊕ (Cherries)

Finally, an all-you-can-eat/drink item is modeled with !:

:(Drink) := (Coffee) &amp; (Tea) &amp; !(Tap water)

In the resource interpretation, the constant 1 denotes the absence of any resource, and so functions as the unit of ⊗ (any formula is equivalent to ). ⊤ is the unit for &amp; and consumes any unneeded resources; 0 represents a product that cannot be made, and thus serves as the unit of ⊕ (a machine that might produce or is as good as a machine that always produces , because it will never succeed in producing a 0); and ⊥ denotes unconsumable resources.

Decidability/complexity of entailment

The entailment relation in full CLL is undecidable. When considering fragments of

CLL, the decision problem has varying complexity:

  • Multiplicative linear logic (MLL): only the multiplicative connectives. MLL entailment is NP-complete, even restricting to Horn clauses in the purely implicative fragment, or to atom-free formulas.
  • Multiplicative-additive linear logic (MALL): only multiplicatives and additives (i.e., exponential-free). MALL entailment is PSPACE-complete.