Path: ...!3.eu.feeder.erje.net!feeder.erje.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: Negative translation for propositional linear (or affine) logic?
Date: Thu, 28 Nov 2024 02:38:26 +0100
Message-ID: <vi8hij$gi0t$1@solani.org>
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> <vi8h9s$ghq4$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 28 Nov 2024 01:38:27 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="542749"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:DL9uaMQKTWG8jn7pDp3BcNm/8tQ=
X-User-ID: eJwNy9EBACAEBcCVUB7GEdl/hLr/0wVG2YZi6+jUnESbXha2Hlt93XZSUPcRoeqJP6iwHGpJ/06oI1KKfR5j0BVx
In-Reply-To: <vi8h9s$ghq4$1@solani.org>
Bytes: 3577
Lines: 72


In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.

Define A^n o- B as:

A o- A o- .. A o- B
\-- n times --/

The running the prover with this notation:

A -> B  := A^n o- B

repeatedly with increasing n .

Mild Shock schrieb:
> 
> But in a linear logic you can do
> intuitionistic logic by using this notation:
> 
>      A -> B := !A o- B
> 
> BTW: There are alternative approaches to
> directly find a notation for classical implication
> in linear logic, without the need for Glivenkos theorem.
> 
> Just put an eye here:
> 
> https://en.wikipedia.org/wiki/Linear_logic#Encoding_classical/intuitionistic_logic_in_linear_logic 
> 
> 
> Julio Di Egidio schrieb:
>> 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.
>>
>> 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> 
>>
>>
>> -Julio
>>
>