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

Well you have to name it natural deduction
and not gentzen. It goes back to Stanisław Jaśkowski:
https://en.wikipedia.org/wiki/Stanis%C5%82aw_Ja%C5%9Bkowski
The paper is this here:
https://www.logik.ch/daten/jaskowski.pdf
Gentzens innovation was probably the Sequent
Calculus and not the natural deduction.
Julio Di Egidio schrieb:

On 21/12/2024 01:30, Mild Shock wrote:

Hi,
>
Could you define what you mean by "gentzen"?

 Really?? This is what I mean by "gentzen" (lowercase):
 <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
 Code is law!  All else failing...
 

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?

 I'll see if I can figure it out.
 -Julio