Happy Now? (Was: Please be patient)

https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p
/* 3 positive test cases */
% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = c*k .
% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 7,
% X = c*(c*k*k) .
% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .
/* 2 negative test case */
% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.
Mild Shock schrieb:

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
>