Path: ...!news.mixmin.net!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: Sun, 1 Dec 2024 17:36:32 +0100
Message-ID: <vii3af$97h8$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 Dec 2024 16:36:31 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="302632"; 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:XZVyhORUIKIPXCfZfNdZuucxvTo=
X-User-ID: eJwNysEBwCAIA8CVioEg4wjI/iPYe5+BwnKlUW1s1KLOblREH5dWKtdotR9xSwnD9vpCkAWMrIyb/2bhCrc+SksVEg==
In-Reply-To: <vii2qb$97ao$1@solani.org>
Bytes: 3588
Lines: 79


Warning: Research gate points to some slides,
which are not exactly the 2007 book.
Also in terms of accelerate superhuman AI,
its probably already an old book.

I didn't check back with ChatGPT although
there is no gurantee that ChatGPT gives
you top notch information, but could be still
helpful nevertheless, more helpful than

https://www.lix.polytechnique.fr/~dale/lolli/

And related systems back then. But did anything
change since then. What don't you like in
the answer:

A -> B  :=   ! A -o B

In my opinion this gives some cues how a translation
could nevertheless work. Something along replacing
A -> B by A -> .. A -> B, i.e. doing the

repeat as a preprocessing. What makes you doubt that
this work. Or do you have some aesthetic critieria
that exclude such a solution?

Mild Shock schrieb:
> Well then Pierce Law is not povable under
> the usual Glivenko translation in affine logic.
> 
> So what? Whats your point?
> 
> 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
> 
> But how do you prove rigorously that affine
> logic rejects certain Glivenko translations.
> You would need to have a (counter-)model finder and
> 
> not a proof finder. The "algebraic viewpoint"
> could help you in building a (counter-)model finder.
> What also sometimes helps is to use modal
> 
> translations together with (counter-)model finders,
> that would then search for some tree models.
> 
> Julio Di Egidio schrieb:
>> On 01/12/2024 16:50, Mild Shock wrote:
>>
>>> This inference rule is incorrect:
>>> % (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
>>> reduction(elim, imp, (C0=>Z), Gs, Ps) :-
>>>      nth1(H, C0, (X->Y), C1),
>>>      append(C1, [Y], C2),
>>>      Gs = [C1=>X,C2=>Z],
>>>      Ps = [H:X,H:Y].
>>>
>>> The correct one would be, X->Y has to
>>> be repeated in the left proof branch:
>>> % (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
>>
>> You are incorrect: that the logic is *affine* indeed means that we 
>> cannot use hypotheses more than once.
>>
>> This is a nice intro scheme, notice also that this is all quite 
>> orthogonal to the classical vs intuitionistic distinction:
>>
>> <https://en.wikipedia.org/wiki/Substructural_type_system>
>>
>> HTH.
>>
>> -Julio
>>
>