Re: Lambda abstraction

At 3:42 AM +0200 31.5.04, Kai Brünnler wrote:
>in your email you pointed out that deep 
>inference allows cancelling of hypotheses in a 
>way that is local (contrary to the sequent 
>calculus) and logical (contrary to natural 
>deduction). I agree, but doesn't natural 
>deduction in sequent-style presentation have 
>exactly the same merits?

Perhaps yes, but I also said that I want a 
formalism with `all the good properties' of the 
sequent calculus (subformula-like, for example).

>I also don't really see how this could help in the design of a term calculus.

I'm not sure, and at this point I can't really 
say more than what I said already.

Basically, it looks like formalism A has 
possibilities of term formation similar to 
natural deduction and less bureaucratic than the 
sequent calculus, so there should be a way of 
exploiting them. (Terms = derivations, of course.)

-Alessio