Re: intuitionistic vs. classical implication in Prolog code

It didn't work, I was running:
?- solve_case(TT, pierce, G), solve_t__sel(TT, G).
And it showed me in SWI-Prolog false:
false.
But the result shoud be true.
Julio Di Egidio schrieb:

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