Re: intuitionistic vs. classical implication in Prolog code

On 01/12/2024 17:27, Mild Shock wrote:

Well then Pierce Law is not povable under
the usual Glivenko translation in affine logic.
So what? Whats your point?

That my TNT (I am now dubbing it "triple-negation translation") instead works, and where is some piece of theory to attach to it?

I found only one book that discusses Glivenk
style translations for substructural logics:
Chatpter 8: Glivenko Theorems
Residuated Lattices: an algebraic glimpse at substructural logics
https://www.researchgate.net/publication/235626321

Indeed there is a lot of not much around.  But Girard talks about not having and not wanting a separate semantics, it's all purely syntactic. But I still have only a vague intuition about what that means.
<https://girard.perso.math.cnrs.fr/0.pdf>
Anyway, pretty much along that line, I am thinking: could I prove in Prolog the meta-properties I have proved in Coq (so far)? Meta-programming and program-analysis features of Prolog are certainly not lacking...
-Julio