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: Negative translation for propositional linear (or affine) logic?
Date: Thu, 28 Nov 2024 02:17:15 +0100
Organization: A noiseless patient Spider
Lines: 46
Message-ID: <vi8gar$1n1h$3@dont-email.me>
References: <vhgdq0$19evr$1@dont-email.me> <vhgemi$ca9e$1@solani.org>
 <vhgg23$19evr$2@dont-email.me> <vhhsit$d108$1@solani.org>
 <vhhuuf$1qic1$1@dont-email.me> <vhi5ch$d5rb$1@solani.org>
 <vhqemf$16mc2$1@dont-email.me> <vi8bgs$42ft$1@solani.org>
 <vi8et8$1n1h$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 28 Nov 2024 02:17:15 +0100 (CET)
Injection-Info: dont-email.me; posting-host="52d3d32bb300a58b1c7fce645c7cbe65";
	logging-data="56369"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+VPGvrO/AbtGKDNnVsOLf/kA46QGSEQo0="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:743ruG3UmLQfHq+t8TTbvoCiqJE=
In-Reply-To: <vi8et8$1n1h$2@dont-email.me>
Content-Language: en-GB
Bytes: 3161

On 28/11/2024 01:52, Julio Di Egidio wrote:
> On 28/11/2024 00:55, Mild Shock wrote:
>> This is Peirce law:
>> ((p->q)->p)->p
>> Peirce law is not provable in minimal logic.
>>
>> But I guess this is not Glivenko:
>> notation(dnt(X), ~X->(~(~X)))
>>
>> https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
>>
>> Glivenko would be simply:
>> notation(gliv(X), (~(~X)))
> 
> Indeed Glivenko's is to embed classical into intuitionistic, not into 
> linear (or affine).
> 
> OTOH, you can try the code yourself: with that 'dnt' the solver solves 
> all the classical theorems I have been able to think about, Pierce's law 
> included, otherwise it fails: because of linearity essentially, i.e. not 
> enough hypotheses...
> <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
> 
> That said, that 'dnt' is almost surely not really correct, indeed maybe 
> it only works for me because my reduction rules are linear (affine 
> actually), yet my operators for now are only the intuitionistic ones, I 
> do not have the whole set of linear operators.

Though that is itself most probably nonsense: there are no linear 
operators in the classical theorems...

> Here are lecture notes that maybe have a complete answer/recipe, see 
> from page 5, but I still cannot fully parse what they write:
> <https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>
> 
> Meanwhile, you might have seen it, I have also asked on SE:
> <https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

And I thought this was an easy one.  Maybe that 'dnt' *is* correct: but 
maybe not.  I just thought the expert would know straight away: me, I'd 
have to formalize the whole thing in Coq to prove meta-properties, but 
then I don't know what I am paying taxes for...


-Julio