Implication in linear logic

Question

Linear logic abandons the structural rules of weakening and contraction.

I wanted to know whether we have $p ⊸ p$ in linear logic.

Can anyone help?

Answer 1

$\DeclareMathOperator{\par}{\unicode{8523}}$Not exactly.   We have Linear Implication, $\,a \multimap b\,$ , (the lollipop operator) which can be defined by linear negation and multiplicative disjunction, $\,a^\bot \par b\,$ .

Answer 2

$\DeclareMathOperator{\par}{\unicode{8523}}$

Under Linear logic, we have the following derive:

$$\frac{\displaystyle\frac{\displaystyle\frac{}{p\ \vdash\ \ p}{\;init}}{\vdash\ \ p^\bot,\ p}{\;(\cdot)^\bot R}}{\vdash\ \ p^\bot \par p} \;\par\!R$$

The system I chosen can be found in the Stanford Encyclopedia of Philosophy. It have the benefit that it is fully symmetric.

As mentioned by the other answer, the proposition at the end is the definition of the linear implication $\multimap$. So we have shown that $p \multimap p$ is a theorem in Linear Logic. QED.