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

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
>