2
$\begingroup$

Consider the sequent calculus presentations of propositional linear logic (LL) and propositional intuitionistic linear logic (ILL). Clearly, there are formulas in LL that are not in ILL, such as $\bot$ or $?X$ or $X \,⅋\, X^\perp$. So, a natural question arises:

For every formula $F$ of LL, is there a formula $G$ in ILL that is provably equivalent in LL to $F$?

I say that $F$ is provably equivalent to $G$ in LL if the formulas $F^\perp \,⅋\, G$ and $G^\perp \,⅋\, F$ (i.e. $F \multimap G$ and $G \multimap F$ in the two-sided sequent calculus) are provable in LL.

If the same question is about classical logic LK (instead of LL) and intuitionistic logic LJ (instead of ILL), the answer is positive thanks to double negation translations. But the same argument cannot be applied here, even because it is not clear to me what a negation is in ILL.

$\endgroup$
  • $\begingroup$ mathoverflow.net/questions/201665/… (The result in the Troelstra reference mentioned embeds CLL into ILZ which is ILL + an intuitionistic zero connective.) $\endgroup$ – Derek Elkins Jun 2 '18 at 1:33
  • $\begingroup$ @DerekElkins - Thank you so much for the precise reference, but it doesn't answer my question. The result you mentioned (Troelstra's Lectures on Linear Logic, Ch. 5, Sect. 12, p. 55) proves only that if $A$ is provable in LL then a translation $A^k$ of $A$ is provable in ILL, but it does not claim that $A$ and $A^k$ are provably equivalent in LL (and it does not seem evident to me). $\endgroup$ – Taroccoesbrocco Jun 2 '18 at 4:08
  • $\begingroup$ It reduces the problem to showing 9 equivalences in CLL. This is quite easy to do as it is easy to prove ${\sim}{\sim}F\circ\!\!-\!\!\circ F$ and section 2.4 mentions the de Morgan dualities you need to prove the ones that aren't handled by double "negation" elimination. The result follows by a straightforward structural induction. $\endgroup$ – Derek Elkins Jun 2 '18 at 4:24
  • $\begingroup$ @DerekElkins - Thank you again. Actually, you give a positive answer for my question between LL and ILZ, but ILZ is a system different from ILL. Essentially, ILZ is ILL (with at most one formula on the right of $\vdash$) + $\bot$ (the notation of Troelstra's Lectures on Linear Logic is misleading, pp. 20-21). But my question is for LL and ILL, where ILL is as defined here, with exactly one formula on the right of $\vdash$ and without $\bot$. $\endgroup$ – Taroccoesbrocco Jun 3 '18 at 8:15
  • $\begingroup$ @DerekElkins - I think that there is no formula in ILL (as defined here) that is provably equivalent in LL to $\bot$. But I don't have any prove of it, whence my question. $\endgroup$ – Taroccoesbrocco Jun 3 '18 at 9:39

Your Answer

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

Browse other questions tagged or ask your own question.