Re: intuitionistic vs. classical implication in Prolog code

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