Re: Advent of Logic 2024: Friendly Reminder (Re: Advent of Logic 2024: Specification and Deadline)

Ok, I made a solution for Weekend 3,
first I made minimal logic. I opted for
Lambda Expressions with de Brujin indexes:
/* 4 positive test cases */
% ?- between(1,13,N), search(typeof(X, [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .
% ?- between(1,13,N), search(typeof(X, [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .
% ?- between(1,13,N), search(typeof(X, [], (a->(b->a))), N, 0).
% N = 3,
% X = lam(a, lam(b, 1)) .
% ?- between(1,13,N), search(typeof(X, [], ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = lam((a->a->b), lam(a, 1*0*0)) .
For example the 2nd solution with de Brujin indexs
can be read without de Brujin indexes as follows:
λx:a.λy:(a->b).(y x)    :    (a->((a->b)->b))
https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-minimal-p
Mild Shock schrieb:

Hi,
 Friendly Reminder that the Deadline 24. December 2024
is approaching. Please be aware that Weekend 3 asks for
Natural Deduction, where (E⊃) and Modus Ponens are synonymous:
 /* Scope of Weekend 3 */
    C, X  ⊢  Y
-------------- (I⊃)
   C ⊢ X ⊃ Y
    C ⊢ X    C ⊢ X ⊃ Y
--------------------- (E⊃) /* Also known as Modus Ponens */
        C ⊢ Y
  Simply Types and its Curry Howard is primarily defined
for Natural Deduction. Extracting Lambda Experessions
from Non-Natural Deduction is a little bit more complicated.
 So Weekend 3 is NOT for Sequent Calculus:
 /* Not Scope of Weekend 3 */
    C, X  ⊢  Y
-------------- (R⊃)
   C ⊢ X ⊃ Y
    C ⊢ X    C, Y ⊢ Z
--------------------- (L⊃)
     C, X ⊃ Y ⊢ Z
 Bye
 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
>