Negative translation for propositional linear (or affine) logic?

On 28/11/2024 00:55, Mild Shock wrote:

This is Peirce law:
((p->q)->p)->p
Peirce law is not provable in minimal logic.
 But I guess this is not Glivenko:
notation(dnt(X), ~X->(~(~X)))
 https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
 Glivenko would be simply:
notation(gliv(X), (~(~X)))

Indeed Glivenko's is to embed classical into intuitionistic, not into linear (or affine).
OTOH, you can try the code yourself: with that 'dnt' the solver solves all the classical theorems I have been able to think about, Pierce's law included, otherwise it fails: because of linearity essentially, i.e. not enough hypotheses...
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
That said, that 'dnt' is almost surely not really correct, indeed maybe it only works for me because my reduction rules are linear (affine actually), yet my operators for now are only the intuitionistic ones, I do not have the whole set of linear operators.
Here are lecture notes that maybe have a complete answer/recipe, see from page 5, but I still cannot fully parse what they write:
<https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>
Meanwhile, you might have seen it, I have also asked on SE:
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>
-Julio