Re: Repetition vs Use (Was: Advent of Logic 2024: Specification and Deadline)

To the best of my knowledge (A -> (B -> A)) is
not a tautology of Affine Logic.
If it were a tautology of Affine Logic,
it would have a BCI combinator expression.
What should be the BCI combinator expression
that fills in the blank ?? here:
?? : (A -> (B -> A))
Can you demonstrate a BCI combinator expression
that has the type (A -> (B -> A)).
Julio Di Egidio schrieb:

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

Its quite intersting that Affine Logic can
be measured by the realization of this output:
>
 > - Output = Variable         % Repetition

 Though, can it?  (More below.)
 

λx:A.λy:B.x : (A -> (B -> A))
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.
 As to how that relates to the lambda calculus side I still don't know, but I find significant that you says Repetition while I (substructural logic) says Use...
 -Julio