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: Tue, 3 Dec 2024 13:59:22 +0100
Organization: A noiseless patient Spider
Lines: 28
Message-ID: <vimvba$vkn$2@dont-email.me>
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> <vii9vv$2eqeg$5@dont-email.me>
 <vijpj3$a69e$2@solani.org> <vijr25$a72h$1@solani.org>
 <vijr94$a72h$2@solani.org> <vik7bi$39c73$2@dont-email.me>
 <vilfmi$b855$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 03 Dec 2024 13:59:22 +0100 (CET)
Injection-Info: dont-email.me; posting-host="908b13ceb23b80a0fcd06b4db7988bd6";
	logging-data="32407"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+C/Y97mQ/x3T75mOOmltH/2CJFrMByp28="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:o3u/JkXdHrqk8qaXOrNuuTtpooo=
Content-Language: en-GB
In-Reply-To: <vilfmi$b855$1@solani.org>
Bytes: 2153

On 03/12/2024 00:26, Mild Shock wrote:

> Its actually easier, you don't need to go
> semantical. You need only to show that
> Consequentia mirabilis aka Calvius Law
> 
> becomes admissible as an inference rule:
>       G, ~A |- A
>     ---------------- (MIR)
>         G |- A
> https://de.wikipedia.org/wiki/Consequentia_mirabilis

(I have too many links already, and you can't even be bothered to link 
to articles in English?)

DNE and equivalent is not provable in any intuitionistic logic.  So, 
what does it even mean to prove it "admissible" here?  In the object 
theory?  Under TNT itself??

> Which is a form of contraction.

Which is not allowed in a linear or affine logic.

Also, with reference to another comment of yours: my rules are 
"directed", and that is a feature... as I have read somewhere.

-Julio