Re: Advent of Logic 2024: Specification and Deadline (Was: Advent of Logic 2024: Weekend 1)

Its quite intersting that Affine Logic can
be measured by the realization of this output:
 > - Output = Variable         % Repetition
Its seems to me that in Affine Logic a variable
is only allowed to occur in a Repetition at most
once, it seems also to me that each variable
must be also repeated at least once. So that
variables are repreated exactly once.
Here is a counter example with too many repetitions,
this would not be a valid output for weekend 3,
since it cannot be converted into the output of weekend 2:
λx:A->A.λy:A.(x (x y))   :  ((A -> A) -> (A -> A))
And her is a counter example with too few repetitions,
equally well it cannot be converted to a BCI expression.
λ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.
Mild Shock schrieb:

Specification:
  Weekend 2:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication
 - Output = B               % B Axiom Schema
          | C               % C Axiom Schema
          | I               % I Axiom Schema
          | (Output Output) % Modus Ponens
 Weekend 3:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication
 - Output = Variable         % Repetition
          | λVariable.Output % Assumption & Detachment
          | (Output Output)  % Modus Ponens
  Deadline:
 24. December 2024