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

At least this would resolve the disambiguity that
the name Gentzen refers to two completely different
deduktive systems:
- 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
They have fundamentaly different proof shapes.
Mild Shock schrieb:

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
>