Editing Linear logic (section)

==Sequent calculus presentation==

One way of defining linear logic is as a [[sequent calculus]].  We use the letters {{math| Γ}} and {{math| Δ}} to range over lists of propositions {{math|<VAR>A</VAR><sub>1</sub>, ..., <VAR>A</VAR><sub>''n''</sub>}}, also called ''contexts''. A ''sequent'' places a context to the left and the right of the [[turnstile (symbol)|turnstile]], written {{math|Γ {{tee}} Δ}}. Intuitively, the sequent asserts that the conjunction of {{math| Γ}} [[Logical consequence|entails]] the disjunction of {{math| Δ}} (though we mean the "multiplicative" conjunction and disjunction, as explained below).  Girard describes classical linear logic using only ''one-sided'' sequents (where the left-hand context is empty), and we follow here that more economical presentation. This is possible because any premises to the left of a turnstile can always be moved to the other side and dualised.

We now give [[Sequent calculus#Inference rules|inference rules]] describing how to build proofs of sequents.{{sfn|Girard|1987|loc=p.22, Def.1.15}}

First, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of [[exchange rule|exchange]]:

{| style="margin:auto" border="0"
|-
| {{math|{{tee}} Γ, A<sub>1</sub>, A<sub>2</sub>, Δ}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, A<sub>2</sub>, A<sub>1</sub>, Δ}}
|}

Note 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.

Next we add ''initial sequents'' and ''cuts'':

{| style="margin:auto"
|-
| style="text-align: center;" |
{| border="0"
|-
| &nbsp;
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR>, <VAR>A</VAR><sup>⊥</sup>}}
|}
| width="50" |
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, <VAR>A</VAR>}} || &nbsp;&nbsp; || &nbsp;&nbsp; || {{math|{{tee}} <VAR>A</VAR><sup>⊥</sup>, Δ}}
|-
| colspan=4 style="border-top:2px solid black;" |
|-
| colspan=4 align="center" | {{math|{{tee}} Γ, Δ}}
|}
|}

The cut rule can be seen as a way of composing proofs, and initial sequents serve as the [[identity element|units]] for composition.  In 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.  
Ultimately, this [[canonical form]] property (which can be divided into the [[completeness of atomic initial sequents]] and the [[cut-elimination theorem]], inducing a notion of [[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]].

Now, we explain the connectives by giving ''logical rules''.  Typically 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).  
In 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 (⊗).  
So, we should expect a certain [[Logical harmony|"harmony"]] between the rule(s) for a connective and the rule(s) for its dual.

===Multiplicatives===

The rules for multiplicative conjunction (⊗) and disjunction (⅋):

{| style="margin:auto"
|-
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, <VAR>A</VAR>}} || &nbsp;&nbsp; || &nbsp;&nbsp; || {{math|{{tee}} Δ, <VAR>B</VAR>}}
|-
| colspan=4 style="border-top:2px solid black;" |
|-
| colspan=4 align="center" | {{math|{{tee}} Γ, Δ, <VAR>A</VAR> ⊗ <VAR>B</VAR>}}
|}
| width="50" |
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, <VAR>A</VAR>, <VAR>B</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, <VAR>A</VAR> ⅋ <VAR>B</VAR>}}
|}
|}

and for their units:

{| style="margin:auto"
|-
| style="text-align: center;" |
{| border="0"
|-
| &nbsp;
|-
| colspan=4 style="border-top:2px solid black;" |
|-
| colspan=4 align="center" | {{math|{{tee}} 1}}
|}
| width="50" |
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, ⊥}}
|}
|}

Observe that the rules for multiplicative conjunction and disjunction are [[Admissible rule|admissible]] for plain ''conjunction'' and ''disjunction'' under a classical interpretation
(i.e., they are admissible rules in [[Sequent calculus#The system LK|LK]]).

===Additives===

The rules for additive conjunction (&) and disjunction (⊕) :

{| style="margin:auto"
|-
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, <VAR>A</VAR>}} || &nbsp;&nbsp; || &nbsp;&nbsp; || {{math|{{tee}} Γ, <VAR>B</VAR>}}
|-
| colspan=4 style="border-top:2px solid black;" |
|-
| colspan=4 align="center" | {{math|{{tee}} Γ, <VAR>A</VAR> & <VAR>B</VAR>}}
|}
| width="50" |
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, <VAR>A</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, <VAR>A</VAR> ⊕ <VAR>B</VAR>}}
|}
| width="25" |
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, <VAR>B</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, <VAR>A</VAR> ⊕ <VAR>B</VAR>}}
|}
|}

and for their units:

{| style="margin:auto"
|-
| style="text-align: center;" |
{| border="0"
|-
| &nbsp;
|-
| colspan=4 style="border-top:2px solid black;" |
|-
| colspan=4 align="center" | {{math|{{tee}} Γ, ⊤}}
|}
| width="50" |
| style="text-align: center;" | (no rule for {{math|0}})
|}

Observe that the rules for additive conjunction and disjunction are again admissible under a classical interpretation. 
But 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 ({{math|Γ, Δ}}) is split up between the premises, whereas for the additive case connective (&) the context of the conclusion ({{math|Γ}}) is carried whole into both premises.

===Exponentials===

The exponentials are used to give controlled access to weakening and contraction. Specifically, we add structural rules of weakening and contraction for {{math|?}}'d propositions:{{sfn|Girard|1987|loc=p.25-26, Def.1.21}}

{| style="margin:auto"
|-
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, ?<VAR>A</VAR>}}
|}
| width="50" |
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, ?<VAR>A</VAR>, ?<VAR>A</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, ?<VAR>A</VAR>}}
|}
|}

and use the following logical rules, in which {{math|?Γ}} stands for a list of propositions each prefixed with {{math|?}}:

{| style="margin:auto"
|-
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} ?Γ, <VAR>A</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} ?Γ, !<VAR>A</VAR>}}
|}
| width="50" |
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} Γ, <VAR>A</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} Γ, ?<VAR>A</VAR>}}
|}
|}

One 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]] [[S4 (modal logic)|S4]], and that there is no longer such a clear symmetry between the duals {{math|!}} and {{math|?}}.  
This situation is remedied in alternative presentations of CLL (e.g., the [[Logic of unity|LU]] presentation).