{"history":[],"article":{"id":"35f8177b-f03d-468a-82e5-5a2682717eb8","title":"Linear logic","slug":"linear-logic","content":":::summary\n:::\n\n# \n**Linear logic** is a [substructural logic](https://bliptext.com/articles/substructural-logic) proposed by French [logician](https://bliptext.com/articles/logician) [Jean-Yves Girard](https://bliptext.com/articles/jean-yves-girard) as a refinement of [classical](https://bliptext.com/articles/classical-logic) and [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic), joining the [dualities](https://bliptext.com/articles/duality-mathematics) of the former with many of the [constructive](https://bliptext.com/articles/constructivism-mathematics) properties of the latter.\nAlthough 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](https://bliptext.com/articles/programming-languages), [game semantics](https://bliptext.com/articles/game-semantics), and [quantum physics](https://bliptext.com/articles/quantum-physics) (because linear logic can be seen as the logic of [quantum information theory](https://bliptext.com/articles/quantum-information-theory)), as well as [linguistics](https://bliptext.com/articles/linguistics), particularly because of its emphasis on resource-boundedness, duality, and interaction.\nLinear logic lends itself to many different presentations, explanations, and intuitions.\n[Proof-theoretically](https://bliptext.com/articles/proof-theory), it derives from an analysis of classical [sequent calculus](https://bliptext.com/articles/sequent-calculus) in which uses of (the [structural rules](https://bliptext.com/articles/structural-rule)) [contraction](https://bliptext.com/articles/idempotency-of-entailment) and [weakening](https://bliptext.com/articles/monotonicity-of-entailment) are carefully controlled.\nOperationally, 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.\nIn terms of simple [denotational models](https://bliptext.com/articles/denotational-semantics), linear logic may be seen as refining the interpretation of intuitionistic logic by replacing [cartesian (closed) categories](https://bliptext.com/articles/cartesian-closed-categories) by [symmetric monoidal (closed) categories](https://bliptext.com/articles/symmetric-monoidal-categories), or the interpretation of classical logic by replacing [Boolean algebras](https://bliptext.com/articles/boolean-algebras) by [C*-algebras](https://bliptext.com/articles/c-algebras).\n\n# Connectives, duality, and polarity\n\n## Syntax\nThe language of classical linear logic (CLL) is defined inductively by the [BNF notation](https://bliptext.com/articles/backus-naur-form)\nHere\np\nand\np⊥\nrange over [logical atoms](https://bliptext.com/articles/atomic-formula).\nFor reasons to be explained below, the [connectives](https://bliptext.com/articles/logical-connective) ⊗, ⅋, 1, and ⊥ are called multiplicatives, the [connectives](https://bliptext.com/articles/logical-connective) &, ⊕, ⊤, and 0 are called additives, and the [connectives](https://bliptext.com/articles/logical-connective) !\nand ?\nare called exponentials.\nWe can further employ the following terminology:\nBinary connectives ⊗, ⊕, & and ⅋ are associative and commutative; 1 is the unit for ⊗, 0 is the unit for ⊕, ⊥ is the unit for ⅋ and ⊤ is the unit for &.\nEvery proposition\nA\nin CLL has a **dual**\nA⊥\n, defined as follows:\nObserve that\n(-)⊥\nis an [involution](https://bliptext.com/articles/involution-mathematics), i.e.,\nA⊥⊥ = A\nfor all propositions.\nA⊥\nis also called the linear negation of\nA\n.\n****T****h****e**** ****c****o****l****u****m****n****s**** ****o****f**** ****t****h****e**** ****t****a****b****l****e**** ****s****u****g****g****e****s****t**** ****a****n****o****t****h****e****r**** ****w****a****y**** ****o****f**** ****c****l****a****s****s****i****f****y****i****n****g**** ****t****h****e**** ****c****o****n****n****e****c****t****i****v****e****s**** ****o****f**** ****l****i****n****e****a****r**** ****l****o****g****i****c****,**** ****t****e****r****m****e****d**** ****:**** ****t****h****e**** ****c****o****n****n****e****c****t****i****v****e****s**** ****n****e****g****a****t****e****d**** ****i****n**** ****t****h****e**** ****l****e****f****t**** ****c****o****l****u****m****n**** ****(****⊗****,**** ****⊕****,**** ****1****,**** ****0****,**** ****!****)**** ****a****r****e**** ****c****a****l****l****e****d**** ****p****o****s****i****t****i****v****e****,**** ****w****h****i****l****e**** ****t****h****e****i****r**** ****d****u****a****l****s**** ****o****n**** ****t****h****e**** ****r****i****g****h****t**** ****(****⅋****,**** ****&****,**** ****⊥****,**** ****⊤****,**** ****?****)**** ****a****r****e**** ****c****a****l****l****e****d**** ****n****e****g****a****t****i****v****e****;**** ****c****f****.****\ntable on the right.\nis not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by\nA ⊸ B := A⊥ ⅋ B\n. The connective ⊸ is sometimes pronounced \"[lollipop](https://bliptext.com/articles/lollipop)\", owing to its shape.\n\n# Sequent calculus presentation\nOne way of defining linear logic is as a [sequent calculus](https://bliptext.com/articles/sequent-calculus).\nWe use the letters\nΓ\nand\nΔ\nto range over lists of propositions\nA1, ..., An\n, also called contexts.\nA sequent places a context to the left and the right of the [turnstile](https://bliptext.com/articles/turnstile-symbol), written\nΓ Δ\n. Intuitively, the sequent asserts that the conjunction of\nΓ\n[entails](https://bliptext.com/articles/logical-consequence) the disjunction of\nΔ\n(though we mean the \"multiplicative\" conjunction and disjunction, as explained below).\nGirard describes classical linear logic using only one-sided sequents (where the left-hand context is empty), and we follow here that more economical presentation.\nThis is possible because any premises to the left of a turnstile can always be moved to the other side and dualised.\nWe now give [inference rules](https://bliptext.com/articles/sequent-calculus) describing how to build proofs of sequents.\nFirst, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of [exchange](https://bliptext.com/articles/exchange-rule):\nNote that we do **not** add the structural rules of weakening and contraction, because we do care about the absence of propositions in a sequent, and the number of copies present.\nNext we add initial sequents and cuts:\nThe cut rule can be seen as a way of composing proofs, and initial sequents serve as the [units](https://bliptext.com/articles/identity-element) for composition.\nIn a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof.\nUltimately, this [canonical form](https://bliptext.com/articles/canonical-form) property (which can be divided into the [completeness of atomic initial sequents](https://bliptext.com/articles/completeness-of-atomic-initial-sequents) and the [cut-elimination theorem](https://bliptext.com/articles/cut-elimination-theorem), inducing a notion of [analytic proof](https://bliptext.com/articles/analytic-proof)) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware [lambda-calculus](https://bliptext.com/articles/lambda-calculus).\nNow, we explain the connectives by giving logical rules.\nTypically in sequent calculus one gives both \"right-rules\" and \"left-rules\" for each connective, essentially describing two modes of reasoning about propositions involving that connective (e.g., verification and falsification).\nIn a one-sided presentation, one instead makes use of negation: the right-rules for a connective (say ⅋) effectively play the role of left-rules for its dual (⊗).\nSo, we should expect a certain [\"harmony\"](https://bliptext.com/articles/logical-harmony) between the rule(s) for a connective and the rule(s) for its dual.\n\n## Multiplicatives\nThe rules for multiplicative conjunction (⊗) and disjunction (⅋):\nand for their units:\nObserve that the rules for multiplicative conjunction and disjunction are [admissible](https://bliptext.com/articles/admissible-rule) for plain conjunction and disjunction under a classical interpretation\n(i.e., they are admissible rules in [LK](https://bliptext.com/articles/sequent-calculus)).\n\n## Additives\nThe rules for additive conjunction (&) and disjunction (⊕) :\nand for their units:\nObserve that the rules for additive conjunction and disjunction are again admissible under a classical interpretation.\nBut now we can explain the basis for the multiplicative/additive distinction in the rules for the two different versions of conjunction: for the multiplicative connective (⊗), the context of the conclusion (\nΓ, Δ\n) is split up between the premises, whereas for the additive case connective (&) the context of the conclusion (\nΓ\n) is carried whole into both premises.\n\n## Exponentials\nThe exponentials are used to give controlled access to weakening and contraction.\nSpecifically, we add structural rules of weakening and contraction for\n?\n'd propositions:\nand use the following logical rules, in which\n?Γ\nstands for a list of propositions each prefixed with\n?\nOne might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives, resembling the inference rules governing modalities in sequent calculus formalisations of the [normal modal logic](https://bliptext.com/articles/normal-modal-logic) [S4](https://bliptext.com/articles/s4-modal-logic), and that there is no longer such a clear symmetry between the duals\n!\nand\n?\n. This situation is remedied in alternative presentations of CLL (e.g., the [LU](https://bliptext.com/articles/logic-of-unity) presentation).\n\n# Remarkable formulas\nIn addition to the [De Morgan dualities](https://bliptext.com/articles/de-morgan-s-laws) described above, some important equivalences in linear logic include:\nBy definition of\nA ⊸ B\nas\nA⊥ ⅋ B\n, the last two distributivity laws also give:\n(Here\nA ≣ B\nis\n(A ⊸ B) & (B ⊸ A)\n.)\nA map that is not an isomorphism yet plays a crucial role in linear logic is:\nLinear distributions are fundamental in the proof theory of linear logic.\nThe consequences of this map were first investigated in and called a \"weak distribution\".\nIn subsequent work it was renamed to \"linear distribution\" to reflect the fundamental connection to linear logic.\nThe following distributivity formulas are not in general an equivalence, only an implication:\n\n# Encoding classical/intuitionistic logic in linear logic\nBoth intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as\n!A ⊸ B\n, while classical implication can be encoded as\n!?A ⊸ ?B\nor\n!A ⊸ ?!B\n(or a variety of alternative possible translations).\nThe idea is that exponentials allow us to use a formula as many times as we need, which is always possible in classical and intuitionistic logic.\nFormally, there exists a translation of formulas of intuitionistic logic to formulas of linear logic in a way that guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula is provable in linear logic.\nUsing the [Gödel–Gentzen negative translation](https://bliptext.com/articles/g-del-gentzen-negative-translation), we can thus embed classical [first-order logic](https://bliptext.com/articles/first-order-logic) into linear [first-order logic](https://bliptext.com/articles/first-order-logic).\n\n# The resource interpretation\nLafont (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.\n[Tony Hoare](https://bliptext.com/articles/tony-hoare) (1985)'s classic example of the vending machine can be used to illustrate this idea.\nSuppose we represent having a candy bar by the atomic proposition\ncandy\n, and having a dollar by\n$1\n. To state the fact that a dollar will buy you one candy bar, we might write the implication\n$1 ⇒ candy\n. But in ordinary (classical or intuitionistic) logic, from\nA\nand\nA ⇒ B\none can conclude\nA ∧ B\n. So, ordinary logic leads us to believe that we can buy the candy bar and keep our dollar!\nOf course,\nwe can avoid this problem by using more sophisticated encodings, although typically such encodings suffer from the [frame problem](https://bliptext.com/articles/frame-problem).\nHowever, the rejection of weakening and contraction allows linear logic to avoid this kind of spurious reasoning even with the \"naive\" rule.\nRather than\n$1 ⇒ candy\n, we express the property of the vending machine as a linear implication\n$1 ⊸ candy\n. From\n$1\nand this fact, we can conclude\ncandy\n, but not\n$1 ⊗ candy\n. In general, we can use the linear logic proposition\nA ⊸ B\nto express the validity of transforming resource\nA\ninto resource\nB\n.\nRunning with the example of the vending machine, consider the \"resource interpretations\" of the other multiplicative and additive connectives.\n(The exponentials provide the means to combine this resource interpretation with the usual notion of persistent [logical truth](https://bliptext.com/articles/logical-truth).)\nMultiplicative conjunction\n(A ⊗ B)\ndenotes simultaneous occurrence of resources, to be used as the consumer directs.\nFor example, if you buy a stick of gum and a bottle of soft drink, then you are requesting\ngum ⊗ drink\n. The constant 1 denotes the absence of any resource, and so functions as the unit of ⊗.\nAdditive conjunction\n(A & B)\nrepresents alternative occurrence of resources, the choice of which the consumer controls.\nIf in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, each costing one dollar, then for that price you can buy exactly one of these products.\nThus we write\n$1 ⊸ (candy & chips & drink)\n. We do not write\n$1 ⊸ (candy ⊗ chips ⊗ drink)\n, which would imply that one dollar suffices for buying all three products together.\nHowever, from\n$1 ⊸ (candy & chips & drink)\n, we can correctly deduce\n$3 ⊸ (candy ⊗ chips ⊗ drink)\n, where\n$3 := $1 ⊗ $1 ⊗ $1\n. The unit ⊤ of additive conjunction can be seen as a wastebasket for unneeded resources.\nFor example, we can write\n$3 ⊸ (candy ⊗ ⊤)\nto express that with three dollars you can get a candy bar and some other stuff, without being more specific (for example, chips and a drink, or $2, or $1 and chips, etc.).\nAdditive disjunction\n(A ⊕ B)\nrepresents alternative occurrence of resources, the choice of which the machine controls.\nFor example, suppose the vending machine permits gambling: insert a dollar and the machine may dispense a candy bar, a packet of chips, or a soft drink.\nWe can express this situation as\n$1 ⊸ (candy ⊕ chips ⊕ drink)\n. The constant 0 represents a product that cannot be made, and thus serves as the unit of ⊕ (a machine that might produce\nA\nor\n0\nis as good as a machine that always produces\nA\nbecause it will never succeed in producing a 0). So unlike above, we cannot deduce\n$3 ⊸ (candy ⊗ chips ⊗ drink)\nfrom this.\n\n# Other proof systems\n\n## Proof nets\nIntroduced by [Jean-Yves Girard](https://bliptext.com/articles/jean-yves-girard), proof nets have been created to avoid the bureaucracy, that is all the things that make two derivations different in the logical point of view, but not in a \"moral\" point of view.\nFor instance, these two proofs are \"morally\" identical:\nThe goal of proof nets is to make them identical by creating a graphical representation of them.\n\n# Semantics\n\n## Algebraic semantics\n\n# Decidability/complexity of entailment\nThe [entailment](https://bliptext.com/articles/entailment) relation in full CLL is [undecidable](https://bliptext.com/articles/undecidable-problem).\nWhen considering fragments of CLL, the decision problem has varying complexity:\n\n# Variants\nMany variations of linear logic arise by further tinkering with the structural rules:\nDifferent intuitionistic variants of linear logic have been considered.\nWhen based on a single-conclusion sequent calculus presentation, like in ILL (Intuitionistic Linear Logic), the connectives ⅋, ⊥, and ?\nare absent, and linear implication is treated as a primitive connective.\nIn FILL (Full Intuitionistic Linear Logic) the connectives ⅋, ⊥, and ?\nare present, linear implication is a primitive connective and, similarly to what happens in intuitionistic logic, all connectives (except linear negation) are independent.\nThere are also first- and higher-order extensions of linear logic, whose formal development is somewhat standard (see [first-order logic](https://bliptext.com/articles/first-order-logic) and [higher-order logic](https://bliptext.com/articles/higher-order-logic)).","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-25T20:04:24.044Z","updated_at":"2025-01-25T20:04:24.044Z","search_vector":"'linear':1 'logic':2","search_content":" \n \n\n# \n**Linear logic** is a [substructural logic](https://bliptext.com/articles/substructural-logic) proposed by French [logician](https://bliptext.com/articles/logician) [Jean-Yves Girard](https://bliptext.com/articles/jean-yves-girard) as a refinement of [classical](https://bliptext.com/articles/classical-logic) and [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic), joining the [dualities](https://bliptext.com/articles/duality-mathematics) of the former with many of the [constructive](https://bliptext.com/articles/constructivism-mathematics) properties of the latter.\nAlthough 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](https://bliptext.com/articles/programming-languages), [game semantics](https://bliptext.com/articles/game-semantics), and [quantum physics](https://bliptext.com/articles/quantum-physics) (because linear logic can be seen as the logic of [quantum information theory](https://bliptext.com/articles/quantum-information-theory)), as well as [linguistics](https://bliptext.com/articles/linguistics), particularly because of its emphasis on resource-boundedness, duality, and interaction.\nLinear logic lends itself to many different presentations, explanations, and intuitions.\n[Proof-theoretically](https://bliptext.com/articles/proof-theory), it derives from an analysis of classical [sequent calculus](https://bliptext.com/articles/sequent-calculus) in which uses of (the [structural rules](https://bliptext.com/articles/structural-rule)) [contraction](https://bliptext.com/articles/idempotency-of-entailment) and [weakening](https://bliptext.com/articles/monotonicity-of-entailment) are carefully controlled.\nOperationally, 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.\nIn terms of simple [denotational models](https://bliptext.com/articles/denotational-semantics), linear logic may be seen as refining the interpretation of intuitionistic logic by replacing [cartesian (closed) categories](https://bliptext.com/articles/cartesian-closed-categories) by [symmetric monoidal (closed) categories](https://bliptext.com/articles/symmetric-monoidal-categories), or the interpretation of classical logic by replacing [Boolean algebras](https://bliptext.com/articles/boolean-algebras) by [C*-algebras](https://bliptext.com/articles/c-algebras).\n\n# Connectives, duality, and polarity\n\n## Syntax\nThe language of classical linear logic (CLL) is defined inductively by the [BNF notation](https://bliptext.com/articles/backus-naur-form)\nHere\n p \nand\n p ⊥\nrange over [logical atoms](https://bliptext.com/articles/atomic-formula).\nFor reasons to be explained below, the [connectives](https://bliptext.com/articles/logical-connective) ⊗, ⅋, 1, and ⊥ are called multiplicatives, the [connectives](https://bliptext.com/articles/logical-connective) &, ⊕, ⊤, and 0 are called additives, and the [connectives](https://bliptext.com/articles/logical-connective) !\nand ?\nare called exponentials.\nWe can further employ the following terminology:\nBinary connectives ⊗, ⊕, & and ⅋ are associative and commutative; 1 is the unit for ⊗, 0 is the unit for ⊕, ⊥ is the unit for ⅋ and ⊤ is the unit for &.\nEvery proposition\n A \nin CLL has a **dual**\n A ⊥\n, defined as follows:\nObserve that\n(-)⊥\nis an [involution](https://bliptext.com/articles/involution-mathematics), i.e.,\n A ⊥⊥ = A \nfor all propositions.\n A ⊥\nis also called the linear negation of\n A \n.\n****T****h****e**** ****c****o****l****u****m****n****s**** ****o****f**** ****t****h****e**** ****t****a****b****l****e**** ****s****u****g****g****e****s****t**** ****a****n****o****t****h****e****r**** ****w****a****y**** ****o****f**** ****c****l****a****s****s****i****f****y****i****n****g**** ****t****h****e**** ****c****o****n****n****e****c****t****i****v****e****s**** ****o****f**** ****l****i****n****e****a****r**** ****l****o****g****i****c****,**** ****t****e****r****m****e****d**** ****:**** ****t****h****e**** ****c****o****n****n****e****c****t****i****v****e****s**** ****n****e****g****a****t****e****d**** ****i****n**** ****t****h****e**** ****l****e****f****t**** ****c****o****l****u****m****n**** ****(****⊗****,**** ****⊕****,**** ****1****,**** ****0****,**** ****!****)**** ****a****r****e**** ****c****a****l****l****e****d**** ****p****o****s****i****t****i****v****e****,**** ****w****h****i****l****e**** ****t****h****e****i****r**** ****d****u****a****l****s**** ****o****n**** ****t****h****e**** ****r****i****g****h****t**** ****(****⅋****,**** ****&****,**** ****⊥****,**** ****⊤****,**** ****?****)**** ****a****r****e**** ****c****a****l****l****e****d**** ****n****e****g****a****t****i****v****e****;**** ****c****f****.****\ntable on the right.\nis not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by\n A ⊸ B := A ⊥ ⅋ B \n. The connective ⊸ is sometimes pronounced \"[lollipop](https://bliptext.com/articles/lollipop)\", owing to its shape.\n\n# Sequent calculus presentation\nOne way of defining linear logic is as a [sequent calculus](https://bliptext.com/articles/sequent-calculus).\nWe use the letters\nΓ\nand\nΔ\nto range over lists of propositions\n A 1, ..., A n\n, also called contexts.\nA sequent places a context to the left and the right of the [turnstile](https://bliptext.com/articles/turnstile-symbol), written\nΓ Δ\n. Intuitively, the sequent asserts that the conjunction of\nΓ\n[entails](https://bliptext.com/articles/logical-consequence) the disjunction of\nΔ\n(though we mean the \"multiplicative\" conjunction and disjunction, as explained below).\nGirard describes classical linear logic using only one-sided sequents (where the left-hand context is empty), and we follow here that more economical presentation.\nThis is possible because any premises to the left of a turnstile can always be moved to the other side and dualised.\nWe now give [inference rules](https://bliptext.com/articles/sequent-calculus) describing how to build proofs of sequents.\nFirst, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of [exchange](https://bliptext.com/articles/exchange-rule):\nNote that we do **not** add the structural rules of weakening and contraction, because we do care about the absence of propositions in a sequent, and the number of copies present.\nNext we add initial sequents and cuts:\nThe cut rule can be seen as a way of composing proofs, and initial sequents serve as the [units](https://bliptext.com/articles/identity-element) for composition.\nIn a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof.\nUltimately, this [canonical form](https://bliptext.com/articles/canonical-form) property (which can be divided into the [completeness of atomic initial sequents](https://bliptext.com/articles/completeness-of-atomic-initial-sequents) and the [cut-elimination theorem](https://bliptext.com/articles/cut-elimination-theorem), inducing a notion of [analytic proof](https://bliptext.com/articles/analytic-proof)) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware [lambda-calculus](https://bliptext.com/articles/lambda-calculus).\nNow, we explain the connectives by giving logical rules.\nTypically in sequent calculus one gives both \"right-rules\" and \"left-rules\" for each connective, essentially describing two modes of reasoning about propositions involving that connective (e.g., verification and falsification).\nIn a one-sided presentation, one instead makes use of negation: the right-rules for a connective (say ⅋) effectively play the role of left-rules for its dual (⊗).\nSo, we should expect a certain [\"harmony\"](https://bliptext.com/articles/logical-harmony) between the rule(s) for a connective and the rule(s) for its dual.\n\n## Multiplicatives\nThe rules for multiplicative conjunction (⊗) and disjunction (⅋):\nand for their units:\nObserve that the rules for multiplicative conjunction and disjunction are [admissible](https://bliptext.com/articles/admissible-rule) for plain conjunction and disjunction under a classical interpretation\n(i.e., they are admissible rules in [LK](https://bliptext.com/articles/sequent-calculus)).\n\n## Additives\nThe rules for additive conjunction (&) and disjunction (⊕) :\nand for their units:\nObserve that the rules for additive conjunction and disjunction are again admissible under a classical interpretation.\nBut now we can explain the basis for the multiplicative/additive distinction in the rules for the two different versions of conjunction: for the multiplicative connective (⊗), the context of the conclusion (\nΓ, Δ\n) is split up between the premises, whereas for the additive case connective (&) the context of the conclusion (\nΓ\n) is carried whole into both premises.\n\n## Exponentials\nThe exponentials are used to give controlled access to weakening and contraction.\nSpecifically, we add structural rules of weakening and contraction for\n?\n'd propositions:\nand use the following logical rules, in which\n?Γ\nstands for a list of propositions each prefixed with\n?\nOne might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives, resembling the inference rules governing modalities in sequent calculus formalisations of the [normal modal logic](https://bliptext.com/articles/normal-modal-logic) [S4](https://bliptext.com/articles/s4-modal-logic), and that there is no longer such a clear symmetry between the duals\n!\nand\n?\n. This situation is remedied in alternative presentations of CLL (e.g., the [LU](https://bliptext.com/articles/logic-of-unity) presentation).\n\n# Remarkable formulas\nIn addition to the [De Morgan dualities](https://bliptext.com/articles/de-morgan-s-laws) described above, some important equivalences in linear logic include:\nBy definition of\n A ⊸ B \nas\n A ⊥ ⅋ B \n, the last two distributivity laws also give:\n(Here\n A ≣ B \nis\n( A ⊸ B ) & ( B ⊸ A )\n.)\nA map that is not an isomorphism yet plays a crucial role in linear logic is:\nLinear distributions are fundamental in the proof theory of linear logic.\nThe consequences of this map were first investigated in and called a \"weak distribution\".\nIn subsequent work it was renamed to \"linear distribution\" to reflect the fundamental connection to linear logic.\nThe following distributivity formulas are not in general an equivalence, only an implication:\n\n# Encoding classical/intuitionistic logic in linear logic\nBoth intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as\n! A ⊸ B \n, while classical implication can be encoded as\n!? A ⊸ ? B \nor\n! A ⊸ ?! B \n(or a variety of alternative possible translations).\nThe idea is that exponentials allow us to use a formula as many times as we need, which is always possible in classical and intuitionistic logic.\nFormally, there exists a translation of formulas of intuitionistic logic to formulas of linear logic in a way that guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula is provable in linear logic.\nUsing the [Gödel–Gentzen negative translation](https://bliptext.com/articles/g-del-gentzen-negative-translation), we can thus embed classical [first-order logic](https://bliptext.com/articles/first-order-logic) into linear [first-order logic](https://bliptext.com/articles/first-order-logic).\n\n# The resource interpretation\nLafont (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.\n[Tony Hoare](https://bliptext.com/articles/tony-hoare) (1985)'s classic example of the vending machine can be used to illustrate this idea.\nSuppose we represent having a candy bar by the atomic proposition\n candy \n, and having a dollar by\n $1 \n. To state the fact that a dollar will buy you one candy bar, we might write the implication\n $1 ⇒ candy \n. But in ordinary (classical or intuitionistic) logic, from\n A \nand\n A ⇒ B \none can conclude\n A ∧ B \n. So, ordinary logic leads us to believe that we can buy the candy bar and keep our dollar!\nOf course,\nwe can avoid this problem by using more sophisticated encodings, although typically such encodings suffer from the [frame problem](https://bliptext.com/articles/frame-problem).\nHowever, the rejection of weakening and contraction allows linear logic to avoid this kind of spurious reasoning even with the \"naive\" rule.\nRather than\n $1 ⇒ candy \n, we express the property of the vending machine as a linear implication\n $1 ⊸ candy \n. From\n $1 \nand this fact, we can conclude\n candy \n, but not\n $1 ⊗ candy \n. In general, we can use the linear logic proposition\n A ⊸ B \nto express the validity of transforming resource\n A \ninto resource\n B \n.\nRunning with the example of the vending machine, consider the \"resource interpretations\" of the other multiplicative and additive connectives.\n(The exponentials provide the means to combine this resource interpretation with the usual notion of persistent [logical truth](https://bliptext.com/articles/logical-truth).)\nMultiplicative conjunction\n( A ⊗ B )\ndenotes simultaneous occurrence of resources, to be used as the consumer directs.\nFor example, if you buy a stick of gum and a bottle of soft drink, then you are requesting\n gum ⊗ drink \n. The constant 1 denotes the absence of any resource, and so functions as the unit of ⊗.\nAdditive conjunction\n( A & B )\nrepresents alternative occurrence of resources, the choice of which the consumer controls.\nIf in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, each costing one dollar, then for that price you can buy exactly one of these products.\nThus we write\n $1 ⊸ ( candy & chips & drink )\n. We do not write\n $1 ⊸ ( candy ⊗ chips ⊗ drink )\n, which would imply that one dollar suffices for buying all three products together.\nHowever, from\n $1 ⊸ ( candy & chips & drink )\n, we can correctly deduce\n $3 ⊸ ( candy ⊗ chips ⊗ drink )\n, where\n $3 := $1 ⊗ $1 ⊗ $1 \n. The unit ⊤ of additive conjunction can be seen as a wastebasket for unneeded resources.\nFor example, we can write\n $3 ⊸ ( candy ⊗ ⊤)\nto express that with three dollars you can get a candy bar and some other stuff, without being more specific (for example, chips and a drink, or $2, or $1 and chips, etc.).\nAdditive disjunction\n( A ⊕ B )\nrepresents alternative occurrence of resources, the choice of which the machine controls.\nFor example, suppose the vending machine permits gambling: insert a dollar and the machine may dispense a candy bar, a packet of chips, or a soft drink.\nWe can express this situation as\n $1 ⊸ ( candy ⊕ chips ⊕ drink )\n. The constant 0 represents a product that cannot be made, and thus serves as the unit of ⊕ (a machine that might produce\n A \nor\n0\nis as good as a machine that always produces\n A \nbecause it will never succeed in producing a 0). So unlike above, we cannot deduce\n $3 ⊸ ( candy ⊗ chips ⊗ drink )\nfrom this.\n\n# Other proof systems\n\n## Proof nets\nIntroduced by [Jean-Yves Girard](https://bliptext.com/articles/jean-yves-girard), proof nets have been created to avoid the bureaucracy, that is all the things that make two derivations different in the logical point of view, but not in a \"moral\" point of view.\nFor instance, these two proofs are \"morally\" identical:\nThe goal of proof nets is to make them identical by creating a graphical representation of them.\n\n# Semantics\n\n## Algebraic semantics\n\n# Decidability/complexity of entailment\nThe [entailment](https://bliptext.com/articles/entailment) relation in full CLL is [undecidable](https://bliptext.com/articles/undecidable-problem).\nWhen considering fragments of CLL, the decision problem has varying complexity:\n\n# Variants\nMany variations of linear logic arise by further tinkering with the structural rules:\nDifferent intuitionistic variants of linear logic have been considered.\nWhen based on a single-conclusion sequent calculus presentation, like in ILL (Intuitionistic Linear Logic), the connectives ⅋, ⊥, and ?\nare absent, and linear implication is treated as a primitive connective.\nIn FILL (Full Intuitionistic Linear Logic) the connectives ⅋, ⊥, and ?\nare present, linear implication is a primitive connective and, similarly to what happens in intuitionistic logic, all connectives (except linear negation) are independent.\nThere are also first- and higher-order extensions of linear logic, whose formal development is somewhat standard (see [first-order logic](https://bliptext.com/articles/first-order-logic) and [higher-order logic](https://bliptext.com/articles/higher-order-logic)).","revisionCount":0},"hasMore":false,"nextCursor":null}

History