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 Newsgroups: sci.logic Subject: Re: Negative translation for propositional linear (or affine) logic? Date: Thu, 28 Nov 2024 02:38:26 +0100 Message-ID: References: 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: 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... >> >> >> 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: >> >> >> >> Meanwhile, you might have seen it, I have also asked on SE: >> >> >> >> -Julio >> >