Re: Negative translation for propositional linear (or affine) logic?

But in a linear logic you can do
intuitionistic logic by using this notation:
     A -> B := !A o- B
BTW: There are alternative approaches to
directly find a notation for classical implication
in linear logic, without the need for Glivenkos theorem.
Just put an eye here:
https://en.wikipedia.org/wiki/Linear_logic#Encoding_classical/intuitionistic_logic_in_linear_logic
Julio Di Egidio schrieb:

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