6
$\begingroup$

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?

$\endgroup$
6
+50
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ Apologies for the notation. I should have said 1 — I've edited the question. $\endgroup$ – Twey Oct 19 '18 at 20:24
  • 2
    $\begingroup$ I have to say, this is very surprising to me in a game-semantic sense. Surely it's always possible to win the dialogue game represented by ¬(¬1 ⊗ ¬1). $\endgroup$ – Twey Oct 19 '18 at 20:51
  • $\begingroup$ 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. $\endgroup$ – Damiano Mazza Oct 20 '18 at 19:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.