predicate logic and deep inference

Hello fellow amphibians,

in case you are interested: I finally managed to prove cut elimination 
for a deep inference system for predicate logic. The proof is very 
different from the cut elimination proofs in sequent systems because 
deep inference has much more freedom in applying a cut. In particular a 
cut can be applied inside an existential quantifier which binds a 
variable in both cut formulas. That's a case that obviously can not 
occur in the sequent calculus. It bugged me quite a bit and I think it 
rules out all the cut elimination techniques known from the sequent 
calculus.

My proof relies on the fact that deep inference allows to split the cut 
into two distinct rules, a cut on quantifiers and a cut on atoms, 
roughly speaking. Eliminating the first happens to yield Herbrand's 
Theorem as a corollary, which then allows to apply propositional cut 
elimination to get rid of the cut on atoms. I particularly enjoy the 
fact that thanks to deep inference Herbrand's Theorem is naturally 
stated as a normal form of derivations, which is impossible in the 
sequent calculus.

I attached a first draft, and I'm interested in comments. I'm afraid 
that in its current state it is only readable by those that are familiar 
with both deep inference and Herbrand's Theorem. I'll send out another 
draft once I added all the definitions and an introduction.


-Kai