Linear logic: Difference between revisions

Revision as of 02:21, 8 December 2020

Revision as of 17:40, 30 December 2020

Line 314:

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

; Distributivity : <math>A\otimes(B\oplus C)\equiv(A\otimes B)\oplus(A\otimes C)</math>

; Exponential isomorphism : <math>\,!(A \& B)\equiv \,!A \otimes \,!B</math>

{| style="margin:auto" border="0"

(Here <math>A\equiv B\quad=\quad(A\multimap B)\&(B\multimap A)</math>.)

|-

| {{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>A</VAR> ⅋ <VAR>B</VAR>)}}

|}

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

Assume that ⅋ is any of the binary operators times, plus, with or par (but not linear implication). The following is not in general an equivalence, only an implication:

{| style="margin:auto" border="0"

; Linear-distributions :

|-

| {{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>)}}

|-

| {{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 <ref>J. Robin Cockett and Robert Seely "Weakly distributive categories" Journal of Pure and Applied Algebra 114(2) 133-173, 1997</ref> and called a "weak distribution". 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>}}

|}

==Encoding classical/intuitionistic logic in linear logic==