What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))

Hi,
Could you define what you mean by "gentzen"?
The problem is Gentzen paper contains two calculi:
- NK/NJ: Classical and Intuitionistic Natural Deduction
   The rules are called elimination/introduction rules
https://en.wikipedia.org/wiki/Natural_deduction
- LK/LJ: Classical and Intuitionistic Sequent Calculus
   The rules are called left/right rules
https://en.wikipedia.org/wiki/Sequent_calculus
Can you convert this proof:
 > ?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
 > Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
 > false
Into a BCK expression?
Bye
Julio Di Egidio schrieb:

On 20/12/2024 19:31, Mild Shock wrote:
 

<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.

 Hmm, gentzen proves them all:
 ```
?- prove(pos, []=>(a->a)->(a->a), Ps).
Ps = [impI,init(0)] ;
Ps = [impI,impI,init(0)] ;
Ps = [impI,impI,impE(1),[init(0)],[init(0)]] ;
false.
 ?- prove(pos, []=>a->((a->b)->b), Ps).
Ps = [impI,impI,impE(0),[init(0)],[init(0)]] ;
false.
 ?- prove(pos, []=>a->(b->a), Ps).
Ps = [impI,impI,init(1)] ;
false.
 ?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
false.
```
 -Julio