Re: intuitionistic vs. classical implication in Prolog code

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
>