Path: ...!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 09:04:24 +0100
Message-ID: <vi9868$4fkp$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>
 <vi8hij$gi0t$1@solani.org> <vi8itf$1n1h$4@dont-email.me>
 <vi97l3$4fgl$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 08:04:24 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="147097"; 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:e3C710glu61Z/5euhSpADRDBKkY=
In-Reply-To: <vi97l3$4fgl$1@solani.org>
X-User-ID: eJwNxUcBwEAIADBLwDHlMP1LaPOJPEVtYxVlOTlPrJ2nE+x4seYVRNPU3n036AsxAKEDnrrFuTbb9Xdk/QF0PRb1
Bytes: 2576
Lines: 47

Affin and linear logic share the use once of a
hypothesis for implication, the unprovability of
P -o P * P being an example of this similarity.

The difference between these logics is somewhere
else in structural rules, and therefore I guess
disjunction is different, but not implication.

But this translation would at least cover implication:

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


Mild Shock schrieb:
> Well I don't know an online affine logic prover.
> But you can play with linear logic here:
> 
> P -o P * P is not provable
> https://click-and-collect.linear-logic.org/?s=P+-o+P+*+P
> 
> !P -o P * P is provable
> https://click-and-collect.linear-logic.org/?s=%21P+-o+P+*+P
> 
> Julio Di Egidio schrieb:
>> On 28/11/2024 02:38, Mild Shock wrote:
>>>
>>> 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 .
>>
>> Yeah, something like that, but I am pretty sure we can do better than 
>> just trial and error.
>>
>> -Julio
>>
>