Re: Lambda abstraction

Alessio,

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?  I 
also don't really see how this could help in the design of a term calculus.

>   [...] I would expect that finding a term calculus for formalism A 
> will be more productive than doing the same for CoS. 

I think the same. My simple cut elimination procedure for SKS 1) 
duplicates more and worse than Gentzen's for LK and 2) it doesn't 
necessarily terminate when allowing free choice on which cut to 
eliminate first. But both is for a stupid reason which seems easily 
fixable by moving from CoS to formalism A ("categorial"? "functorial"? CoS).

-Kai