Re: intuitionistic vs. classical implication in Prolog code

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