Editing Linear logic (section)

==Variants==

Many variations of linear logic arise by further tinkering with the structural rules:

* [[Affine logic]], which forbids contraction but allows global weakening (a decidable extension).
* [[Strict logic]] or [[relevant logic]], which forbids weakening but allows global contraction.
* [[Noncommutative logic|Non-commutative logic]] or ordered logic, which removes the rule of exchange, in addition to barring weakening and contraction.  In ordered logic, linear implication divides further into left-implication and right-implication.

Different intuitionistic variants of linear logic have been considered. When based on a single-conclusion sequent calculus presentation, like in ILL (Intuitionistic Linear Logic), the connectives ⅋, ⊥, and ? are absent, and linear implication is treated as a primitive connective. In FILL (Full Intuitionistic Linear Logic) the connectives ⅋, ⊥, and ? are present, linear implication is a primitive connective and, similarly to what happens in intuitionistic logic, all connectives (except linear negation) are independent.
There are also first- and higher-order extensions of linear logic, whose formal development is somewhat standard (see [[first-order logic]] and [[higher-order logic]]).