Please be patient (Was: Repetition vs Use)

Hi,
Ok, Ok, nobody cares. I will put different
labels on the bottles. And use this naming:
BCI: Linear Logic
BCK: Affine Logic
SK: Minimal Logic
You will see a further file linear.p in this
gist in a blink. Please be patient.
https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72 Bye
P.S.: The logics concerning derivable
sentences show this inclusion:
Linear ⊂ Affine ⊂ Minimal
Julio Di Egidio schrieb:

On 20/12/2024 18:46, Mild Shock wrote:

Julio Di Egidio schrieb:

On 20/12/2024 02:48, Mild Shock wrote:

 

I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

>
That is simply wrong, affine logic can of course prove a statement where, after the intros, hypothesis 1 is used once and hypothesis 2 is not used at all.  That wouldn't be valid for linear logic (in the sense still of a substructural logic), as we are not using all hypothesis.

>
If it were a tautology of Affine Logic,
it would have a BCI combinator expression.

 Indeed, BCI gives linear logic (in the substructural sense), not affine...
 <https://ncatlab.org/nlab/show/combinatory+logic>
 -Julio