Re: intuitionistic vs. classical implication in Prolog code

On 12/01/2024 10:30 AM, Julio Di Egidio wrote:

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
>

When somebody says "not semantics: only syntax"
it's sort of like Tarski wanting to make "only constants"
so that original and singular things don't introduce
their hyper-geometric, for example, about 0 1 infinity,
or, usually they're after having quasi-modal material implication,
then you can just give them "not semantics is false, so,
here's your material implication satisfied and now your
syntactical guarantee agrees it doesn't itself hold".
Like a lie, ....
A convenient lie I suppose, just you know, anathematic.