Editing Linear logic (section)

==Remarkable formulas==

In addition to the [[De Morgan's laws|De Morgan dualities]] described above, some important equivalences in linear logic include:

; Distributivity :

{| style="margin:auto" border="0"
|-
| {{math|<VAR>A</VAR> ⊗ (<VAR>B</VAR> ⊕ <VAR>C</VAR>) ≣ (<VAR>A</VAR> ⊗ <VAR>B</VAR>) ⊕ (<VAR>A</VAR> ⊗ <VAR>C</VAR>)}}
|-
| {{math|(<VAR>A</VAR> ⊕ <VAR>B</VAR>) ⊗ <VAR>C</VAR> ≣ (<VAR>A</VAR> ⊗ <VAR>C</VAR>) ⊕ (<VAR>B</VAR> ⊗ <VAR>C</VAR>)}}
|-
| {{math|<VAR>A</VAR> ⅋ (<VAR>B</VAR> & <VAR>C</VAR>) ≣ (<VAR>A</VAR> ⅋ <VAR>B</VAR>) & (<VAR>A</VAR> ⅋ <VAR>C</VAR>)}}
|-
| {{math|(<VAR>A</VAR> & <VAR>B</VAR>) ⅋ <VAR>C</VAR> ≣ (<VAR>A</VAR> ⅋ <VAR>C</VAR>) & (<VAR>B</VAR> ⅋ <VAR>C</VAR>)}}
|}

By definition of {{math|<VAR>A</VAR> ⊸ <VAR>B</VAR>}} as {{math|<VAR>A</VAR><sup>⊥</sup> ⅋ <VAR>B</VAR>}}, the last two distributivity laws also give:

{| style="margin:auto" border="0"
|-
| {{math|<VAR>A</VAR> ⊸ (<VAR>B</VAR> & <VAR>C</VAR>) ≣ (<VAR>A</VAR> ⊸ <VAR>B</VAR>) & (<VAR>A</VAR> ⊸ <VAR>C</VAR>)}}
|-
| {{math|(<VAR>A</VAR> ⊕ <VAR>B</VAR>) ⊸ <VAR>C</VAR> ≣ (<VAR>A</VAR> ⊸ <VAR>C</VAR>) & (<VAR>B</VAR> ⊸ <VAR>C</VAR>)}}
|}

(Here {{math|<VAR>A</VAR> ≣ <VAR>B</VAR>}} is {{math|(<VAR>A</VAR> ⊸ <VAR>B</VAR>) & (<VAR>B</VAR> ⊸ <VAR>A</VAR>)}}.)

; Exponential isomorphism :

{| style="margin:auto" border="0"
|-
| {{math|!(<VAR>A</VAR> & <VAR>B</VAR>) ≣ !<VAR>A</VAR> ⊗ !<VAR>B</VAR>}}
|-
| {{math|?(<VAR>A</VAR> ⊕ <VAR>B</VAR>) ≣ ?<VAR>A</VAR> ⅋ ?<VAR>B</VAR>}}
|}

; Linear distributions :

A map that is not an isomorphism yet plays a crucial role in linear logic is:

{| style="margin:auto" border="0"
|-
| {{math|(<VAR>A</VAR> ⊗ (<VAR>B</VAR> ⅋ <VAR>C</VAR>)) ⊸ ((<VAR>A</VAR> ⊗ <VAR>B</VAR>) ⅋ <VAR>C</VAR>)}}
|}

Linear distributions are fundamental in the proof theory of linear logic. The consequences of this map were first investigated in Cockett & Seely (1997) and called a "weak distribution".{{sfn|Cockett|Seely|1997}} In subsequent work it was renamed to "linear distribution" to reflect the fundamental connection to linear logic.

; Other implications :

The following distributivity formulas are not in general an equivalence, only an implication:

{| style="margin:auto" border="0"
|-
| {{math|!<VAR>A</VAR> ⊗ !<VAR>B</VAR> ⊸ !(<VAR>A</VAR> ⊗ <VAR>B</VAR>)}}
|-
| {{math|!<VAR>A</VAR> ⊕ !<VAR>B</VAR> ⊸ !(<VAR>A</VAR> ⊕ <VAR>B</VAR>)}}
|}

{| style="margin:auto" border="0"
|-
| {{math|?(<VAR>A</VAR> ⅋ <VAR>B</VAR>) ⊸ ?<VAR>A</VAR> ⅋ ?<VAR>B</VAR>}}
|-
| {{math|?(<VAR>A</VAR> & <VAR>B</VAR>) ⊸ ?<VAR>A</VAR> & ?<VAR>B</VAR>}}
|}

{| style="margin:auto" border="0"
|-
| {{math|(<VAR>A</VAR> & <VAR>B</VAR>) ⊗ <VAR>C</VAR> ⊸ (<VAR>A</VAR> ⊗ <VAR>C</VAR>) & (<VAR>B</VAR> ⊗ <VAR>C</VAR>)}}
|-
| {{math|(<VAR>A</VAR> & <VAR>B</VAR>) ⊕ <VAR>C</VAR> ⊸ (<VAR>A</VAR> ⊕ <VAR>C</VAR>) & (<VAR>B</VAR> ⊕ <VAR>C</VAR>)}}
|}

{| style="margin:auto" border="0"
|-
| {{math|(<VAR>A</VAR> ⅋ <VAR>C</VAR>) ⊕ (<VAR>B</VAR> ⅋ <VAR>C</VAR>) ⊸ (<VAR>A</VAR> ⊕ <VAR>B</VAR>) ⅋ <VAR>C</VAR>}}
|-
| {{math|(<VAR>A</VAR> & <VAR>C</VAR>) ⊕ (<VAR>B</VAR> & <VAR>C</VAR>) ⊸ (<VAR>A</VAR> ⊕ <VAR>B</VAR>) & <VAR>C</VAR>}}
|}