Lambda abstraction

Hello,

for several reasons (Elaine and intersection types, Kai and 
intuitionistic logic, etc.), we got to the point in which we should 
ask ourselves questions about term calculi related to deep inference 
formalisms.

I just noticed a trivial fact, I don't know whether it might be 
important or not.

We all know that in natural deduction we can make the deduction transformation

              [A]
    A          |
    |   ~>     B    ,
    B        ------
             A -> B

which corresponds to forming the term

    t   ~>   lambda x.t .

There are a few cumbersome technicalities one has to deal with, like 
discharging hypothesis and taking care of `parcels' of them, which 
means using some care in variable bindings, etc.

In this case, one can argue that the typed lambda calculus notation 
is superior to the natural deduction one because the lambda term is 
more precise, for example the names of variables are enough for 
taking care of parcels of hypothesis and which of them are 
discharged, what is instead cumbersome in natural deduction notation.

The situation is worse in the sequent calculus: if you want to 
express a `->' introduction with discharging of hypotheses you have 
to perform a global transformation of the proof in which you add 
hypothesis A everywhere, and you only use it in some axioms 
somewhere. Terrible from the point of view of making the relation to 
a term calculus.

Instead, and this is the observation, I noticed that if you use 
formalism `A', the whole thing becomes natural, so possibly 
convenient in view of the search for a term calculus.

The same transformation as above simply becomes:

                 t
             ----------
    A        [      A ]
    |   ~>   [ -A , | ] ,
    B        [      B ]

in the case there is only one hypothesis A. Notice that in formalism 
`A' the conclusion of the derivation on the right is [-A,B].

In the case there are, say, three hypotheses A, two of which in the 
parcel, one uses contraction on -A and explicitly kills those that 
are in the parcel; for example:

                             A
                   =====================
    (A,A,A)        [ [-A,-A]   (A,A,A) ]
       |      ~>   [ ------- ,    |    ] ,
       B           [   -A         B    ]


What is, I believe, important here:

1) the language of derivations is entirely sufficient and natural for 
expressing all the details of the transformation, contrary to natural 
deduction, and

2) it does so without having to touch the initial derivation, 
contrary to the sequent calculus.

You see that what is crucial is being able to put the `hypothesis 
killer' in parallel to an entire derivation, what is possible in 
formalism `A' and impossible in CoS, sequent calculus, natural 
deduction, etc. I think this should be useful for designing a term 
calculus.

I've put the description of formalism `A' as a note on the web: 
<http://www.ki.inf.tu-dresden.de/~guglielm/res/notes/AG11.pdf>.

-Alessio