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

What would make me already happy , if we would be able
to make definitions of these terms, namely:
- Affine logic
- Linear logic
I found this helpful, which isn't behind a paywall:
https://en.wikipedia.org/wiki/Substructural_type_system
"Type system" can be another word for "logic with
proof terms", if you look at:
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
And substructural fits the idea to drop
some of the structural rules.
But to be precise one would need to distingish
left and right structural rules. For example
contraction can happen in at least these two forms:
A & A -> A
A -> A v A
If you have (A & B -> C) == (A -> (B -> C)) you most
lilely won't get rid of the first form.
Julio Di Egidio schrieb:

On 28/11/2024 09:04, Mild Shock wrote:

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.

 Should have been yesterday, but it's still the next frontier:
 <https://girard.perso.math.cnrs.fr/0.pdf>
 Of course more than half of it is under a pay wall, but we'll do what we can...
 -Julio