Editing Linear logic (section)

==Connectives, duality, and polarity==
===Syntax===
{{anchor|Classical linear logic}}
The language of ''classical linear logic'' (CLL) is defined inductively by the [[Backus–Naur form|BNF notation]]

{| style="margin:auto"
|-
| {{math|<VAR>A</VAR>}}
| ::=
| {{math|<VAR>p</VAR> ∣ <VAR>p</VAR><sup>⊥</sup>}}
|-
|
| {{math|∣}}
| {{math| <VAR>A</VAR> ⊗ <VAR>A</VAR> ∣ <VAR>A</VAR> ⊕ <VAR>A</VAR>}}
|-
|
| {{math|∣}}
| {{math| <VAR>A</VAR> & <VAR>A</VAR> ∣ <VAR>A</VAR> ⅋ <VAR>A</VAR>}}
|-
|
| {{math|∣}}
| {{math| 1 ∣ 0 ∣ ⊤ ∣ ⊥}}
|-
|
| {{math|∣}}
| {{math| !<VAR>A</VAR> ∣ ?<VAR>A</VAR>}}
|}

Here {{math|<VAR>p</VAR>}} and {{math|<VAR>p</VAR><sup>⊥</sup>}} range over [[Atomic formula|logical atoms]].  For reasons to be explained below, the [[Logical connective|connectives]] ⊗, ⅋, 1, and ⊥ are called ''multiplicatives'', the connectives &, ⊕, ⊤, and 0 are called ''additives'', and the connectives ! and ? are called ''exponentials''. 
We can further employ the following terminology:

{| class="wikitable"
|+
!Symbol
! colspan="3" |Name
|-
|⊗ 
|multiplicative [[Logical conjunction|conjunction]]
|times 
|tensor
|-
|⊕
|additive [[Logical disjunction|disjunction]]
| colspan="2" |plus
|-
|&
|additive [[Logical conjunction|conjunction]]
| colspan="2" |with
|-
|{{Anchor|⅋}}⅋
|multiplicative [[Logical disjunction|disjunction]]
| colspan="2" |par
|-
|!
|of course
| colspan="2" |bang
|-
|?
|why not
| colspan="3" |quest
|}


Binary 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 &. 

Every proposition {{math|<VAR>A</VAR>}} in CLL has a '''dual''' {{math|<VAR>A</VAR><sup>⊥</sup>}}, defined as follows:

{| border="1" cellpadding="5" cellspacing="0" style="margin:auto"
|-
| colspan=3 align="center"| {{math|(<VAR>p</VAR>)<sup>⊥</sup>  {{=}}  <VAR>p</VAR><sup>⊥</sup>}}
| colspan=3 align="center"| {{math|(<VAR>p</VAR><sup>⊥</sup>)<sup>⊥</sup>  {{=}} <VAR>p</VAR>}}
|-
| colspan=3 align="center"| {{math|(<VAR>A</VAR> ⊗ <VAR>B</VAR>)<sup>⊥</sup> {{=}} <VAR>A</VAR><sup>⊥</sup> ⅋ <VAR>B</VAR><sup>⊥</sup>}}
| colspan=3 align="center"| {{math|(<VAR>A</VAR> ⅋ <VAR>B</VAR>)<sup>⊥</sup> {{=}} <VAR>A</VAR><sup>⊥</sup> ⊗ <VAR>B</VAR><sup>⊥</sup>}}
|-
| colspan=3 align="center"| {{math|(<VAR>A</VAR> ⊕ <VAR>B</VAR>)<sup>⊥</sup> {{=}} <VAR>A</VAR><sup>⊥</sup> & <VAR>B</VAR><sup>⊥</sup>}}
| colspan=3 align="center"| {{math|(<VAR>A</VAR> & <VAR>B</VAR>)<sup>⊥</sup> {{=}} <VAR>A</VAR><sup>⊥</sup> ⊕ <VAR>B</VAR><sup>⊥</sup>}}
|-
| colspan=3 align="center"| {{math|(1)<sup>⊥</sup> {{=}} ⊥}}
| colspan=3 align="center"| {{math|(⊥)<sup>⊥</sup> {{=}} 1}}
|-
| colspan=3 align="center"| {{math|(0)<sup>⊥</sup> {{=}} ⊤}}
| colspan=3 align="center"| {{math|(⊤)<sup>⊥</sup> {{=}} 0}}
|-
| colspan=3 align="center"| {{math|(!<VAR>A</VAR>)<sup>⊥</sup> {{=}} ?(<VAR>A</VAR><sup>⊥</sup>)}}
| colspan=3 align="center"| {{math|(?<VAR>A</VAR>)<sup>⊥</sup> {{=}} !(<VAR>A</VAR><sup>⊥</sup>)}}
|-
|}

{| class="wikitable" style="float:right"
|+ Classification of connectives
|- 
!     !! add   !! mul   !! exp
|-
! pos 
| ⊕ 0 || ⊗ 1 || !
|-
! neg 
| & ⊤ || ⅋ ⊥ || ?
|}

Observe that {{math|(-)<sup>⊥</sup>}} is an [[Involution (mathematics)|involution]], i.e., {{math|<VAR>A</VAR><sup>⊥⊥</sup> {{=}} <VAR>A</VAR>}} for all propositions.  {{math|<VAR>A</VAR><sup>⊥</sup>}} is also called the ''linear negation'' of {{math|<VAR>A</VAR>}}.

The columns of the table suggest another way of classifying the connectives of linear logic, termed '''{{em|{{visible anchor|polarity}}}}''': the connectives negated in the left column (⊗, ⊕, 1, 0, !) are called ''positive'', while their duals on the right (⅋, &, ⊥, ⊤, ?) are called ''negative''; cf. table on the right.

{{em|{{visible anchor|Linear implication}}}} is not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by {{math|<VAR>A</VAR> ⊸ <VAR>B</VAR> :{{=}} <VAR>A</VAR><sup>⊥</sup> ⅋ <VAR>B</VAR>}}.  The connective ⊸ is sometimes pronounced "[[lollipop]]", owing to its shape.