Re: Negative translation for propositional linear (or affine) logic?

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