Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: intuitionistic vs. classical implication in Prolog code
Date: Sun, 1 Dec 2024 19:30:22 +0100
Organization: A noiseless patient Spider
Lines: 27
Message-ID: <vii9vv$2eqeg$5@dont-email.me>
References: <vihumn$2eqeg$3@dont-email.me> <vihvl9$9568$1@solani.org>
 <vii0l0$m02t$1@solani.org> <vii1jv$2eqeg$4@dont-email.me>
 <vii2qb$97ao$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sun, 01 Dec 2024 19:30:23 +0100 (CET)
Injection-Info: dont-email.me; posting-host="9457540d49654f8b44273a26fe4626ef";
	logging-data="2582992"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+XiPPNWqj90gw4ysMljjIKwSgnd0HMFQY="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:o41KQCz7qujAEg/OdwvhC2znQmA=
In-Reply-To: <vii2qb$97ao$1@solani.org>
Content-Language: en-GB
Bytes: 2165

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