Access to the full content is only available to members of institutions that have purchased access. If you belong to such an institution, please log in or find out more about how to order.

### Contents

• content locked
1
• content locked
2
• content locked
3
• content locked
4
• content locked

# Linear logic

DOI
10.4324/9780415249126-X006-1
DOI: 10.4324/9780415249126-X006-1
Version: v1,  Published online: 1998
Retrieved November 15, 2019, from https://www.rep.routledge.com/articles/thematic/linear-logic/v-1

## Article Summary

Linear logic was introduced by Jean-Yves Girard in 1987. Like classical logic it satisfies the law of the excluded middle and the principle of double negation, but, unlike classical logic, it has non-degenerate models. Models of logics are often given only at the level of provability, in that they provide denotations of formulas. However, we are also interested in models which provide denotations of deductions, or proofs. Given such a model two proofs are said to be equivalent if their denotations are equal. A model is said to be ‘degenerate’ if there are no formulas for which there exist at least two non-equivalent proofs. It is easy to see that models of classical logic are essentially degenerate because any formula is either true or false and so all proofs of a formula are considered equivalent. The intuitionist approach to this problem involves altering the meaning of the logical connectives but linear logic attacks the very connectives themselves, replacing them with more refined ones. Despite this there are simple translations between classical and linear logic.

One can see the need for such a refinement in another way. Both classical and intuitionistic logics could be said to deal with static truths; both validate the rule of modus ponens: if A→B and A, then B; but both also validate the rule if A→B and A, then A∧B. In mathematics this is correct since a proposition, once verified, remains true – it persists. Many situations do not reflect such persistence but rather have an additional notion of causality. An implication A→B should reflect that a state B is accessible from a state A and, moreover, that state A is no longer available once the transition has been made. An example of this phenomenon is in chemistry where an implication A→B represents a reaction of components A to yield B. Thus if two hydrogen and one oxygen atoms bond to form a water molecule, they are consumed in the process and are no longer part of the current state. Linear logic provides logical connectives to describe such refined interpretations.