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

On 28/11/2024 01:52, Julio Di Egidio wrote:

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.

Though that is itself most probably nonsense: there are no linear operators in the classical theorems...

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>

And I thought this was an easy one.  Maybe that 'dnt' *is* correct: but maybe not.  I just thought the expert would know straight away: me, I'd have to formalize the whole thing in Coq to prove meta-properties, but then I don't know what I am paying taxes for...
-Julio