I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.
Is it possible, in Melliès' tensorial logic, to give a proof of ¬(¬1 ⊗ ¬1) (a.k.a. 1 ⅋ 1)? Equivalently, is there an arrow in a dialogue category (with monoidal unit 1 and negation functor ¬) from ¬1 to 1?
The formula $\lnot(\lnot 1\otimes\lnot 1)$ is not provable. This is similar to the non-provability of $1⅋1$ in linear logic without mix.
If you want to see it directly in tensorial logic, simply observe that, by cut-elimination (which holds in tensorial logic) and reversibility of the $\lnot$-right and $\otimes$-left rules, derivability of $\vdash\lnot(\lnot 1\otimes\lnot 1)$ is equivalent to derivability of $\lnot 1,\lnot 1\vdash\bot$, which may only come from a proof of $\lnot 1\vdash 1$, which is unprovable because no rule (except cut) admits such a sequent as its conclusion, as shown by a straightforward inspection of the various rules (cf. for instance p.84 of Melliès habilitation thesis).
To add a semantic argument: models of tensor logic are given by symmetric monoidal categories with an exponentiating object $\bot$ serving as pole; negation is then given by $\neg A = \bot^A$. For example, one may choose any object of a symmetric monoidal closed category as pole, and degenerate special cases of this are given by abelian groups viewed as discrete categories. Now take eg the additive group of integers, and $1$ as pole. Then an arrow $\bot\otimes\bot\to\bot$ in the model would mean that $1+1=1$.
