Basic equivalences in linear logic

124 Views Asked by At

How do we obtain the equivalence $A \otimes 0 \equiv 0$ and its dual in linear logic? Are they a consequence of cut-elimination?

I found them listed as basic equivalences in the following resource: http://iml.univ-mrs.fr/~lafont/pub/llpages.pdf , but have not found an explicit way of proving it in the literature.

1

There are 1 best solutions below

0
On

Using the definition in the paper, we need to show that the sequent $\vdash 0, \Gamma$ is provable if and only if $\vdash A \otimes 0, \Gamma$ is provable.

Note that

  1. By the rule for $\top$: $\vdash \top, \Delta$ for any $\Delta$. So for both directions it is sufficient to prove that the assumption implies $\top \in \Gamma$.

  2. The sequent $\vdash 0, \Delta$ is provable only by using the id rule which introduces its dual, i.e. $\top \in \Delta$, since there is no introduction rule for $0$.

From (2) it is immediate that $\vdash 0, \Gamma$ is provable only if $\top \in \Gamma$.

Assume $\vdash A \otimes 0, \Gamma$ is provable. The only introduction rule for $\otimes$ requires that both $\vdash A, \Gamma_1$ and $\vdash 0, \Gamma_2$ are provable, and $\Gamma = \Gamma_1, \Gamma2$. By (2) we get that $\top \in \Gamma_2$ and therefore $\top \in \Gamma$.