# Proof of ¬(¬1 ⊗ ¬1) in tensorial logic

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?

Your notation is a bit confusing because usually in linear logic and related systems $$\top$$ denotes the unit of additive conjuction (i.e., categorically, the terminal object), but then when you formulate your question in categorical terms you clearly say that by $$\top$$ you mean the monoidal unit, which instead is traditionally denoted by $$1$$ (this is the notation used by Melliès, for instance in his habilitation thesis, see p.83-84).
So, the answer depends on what is $$\top$$. If it is the terminal object, then $$\lnot(\lnot\top\otimes\lnot\top)$$ is indeed provable; if it is the monoidal unit (which I am going to denote by $$1$$ here), then $$\lnot(\lnot 1\otimes\lnot 1)$$ is not provable.
In the former case, here's a proof: $$\begin{array}{rcl} \lnot\top & \vdash & \top \\ \hline \lnot\top,\lnot\top & \vdash & \bot \\ \hline \lnot\top\otimes\lnot\top & \vdash & \bot \\ \hline & \vdash & \lnot(\lnot\top\otimes\lnot\top) \\ \end{array}$$
In the latter case, non-provability comes from 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).
• I honestly don't know the exact definition of innocent sequential strategy (the one corresponding to tensorial logic) so I can't tell you what goes wrong. I'm pretty sure that it has to do with the fact that the two copies of $1$ are in parallel here, which is precisely the intuition behind the mix rule... but I don't know, it's a good question. – Damiano Mazza Oct 20 '18 at 19:11