Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: intuitionistic vs. classical implication in Prolog code
Date: Mon, 2 Dec 2024 09:27:50 +0100
Message-ID: <vijr25$a72h$1@solani.org>
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> <vii9vv$2eqeg$5@dont-email.me>
 <vijpj3$a69e$2@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 Dec 2024 08:27:49 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="334929"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:FOlMtgboFHZq8XUnALIpMcatWoA=
In-Reply-To: <vijpj3$a69e$2@solani.org>
X-User-ID: eJwFwYEBwCAIA7CXhNEi5yDa/09Ygo/GySAYEOQbajGTMmUgb5ccNf3W1sqBtincdDzzsdQr/PESx2v8B1YaFYQ=
Bytes: 3118
Lines: 81

Ok my fault I tested Glivenko and not your TNT,
with TNT I get indeed this here:

?- solve_case(TT, pierce, G), solve_t__sel(TT, G).
TT = neg,
G = ([((p->q)->p)]=>p).

Oki Doki

But I am not familiar with this proof display:

[
   impI((p->0))
   impI((p->0))
   [
     impE1(1:(p->q))
     impI(p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       botE(3:0)
     ]
   ]
   [
     impE2(1:p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       unif(3:0)
     ]
   ]
]

How is one supposed to read the above?

Mild Shock schrieb:
> 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
>>
>