Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: intuitionistic vs. classical implication in Prolog code
Date: Sun, 1 Dec 2024 17:07:26 +0100
Organization: A noiseless patient Spider
Lines: 26
Message-ID: <vii1jv$2eqeg$4@dont-email.me>
References: <vihumn$2eqeg$3@dont-email.me> <vihvl9$9568$1@solani.org>
 <vii0l0$m02t$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 01 Dec 2024 17:07:27 +0100 (CET)
Injection-Info: dont-email.me; posting-host="9457540d49654f8b44273a26fe4626ef";
	logging-data="2582992"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18YRxGqKL7GagF9aZtJtYXNuCrGVJh52X4="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:ltzyrOuL93GsBwkHv7jFtKnNKAg=
Content-Language: en-GB
In-Reply-To: <vii0l0$m02t$1@solani.org>
Bytes: 1800

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