Re:predicate logic and deep inference

Hello Kai,

I'm happy to hear this news. I've only read your paper very quickly 
because these days I'm super-busy, so I cannot comment on the 
technical accuracy, but I do have some `high level' comments. Of 
course, your argument makes perfect sense to me, so I believe it is 
(or it can be made, in case) correct. Possibly, it can also be 
simplified substantially, this is just an impression I have but 
wouldn't know how.

1   From your message, somebody might get the impression that cut 
elimination for predicate logic in CoS was not known: of course, this 
is not the case: cut admissibility can be proved semantically (the 
down system is complete) and you described in your thesis a 
constructive cut elimination procedure that translates proofs into 
the sequent calculus and gets back cut-free proofs into CoS. In 
addition, there is a cut elimination proof based on splitting, 
floating around since a long time, which sooner or later will 
condense into a paper.

2   I agree on your emphasis on Herbrand's theorem. In the final 
paper, I would love to see a short and clear exposition of Herbrand's 
theorem, a well-round argument about the fact that the sequent 
calculus doesn't do justice to it, and then a high level detail-free 
summary of why deep inference is necessary for the task. In other 
words: if, as I understand, you want to shift the emphasis from cut 
elimination to Herbrand's theorem, I fully agree with you, because 
this goes in the direction of promoting decompositions, i.e., other 
forms of normalisation that the sequent calculus simply cannot 
achieve.

3   You might perhaps go ahead and argue about the problem of 
identity of proofs: clearly, your normal form should contribute quite 
a bit.

4   I see that you're using `deep inference' instead of CoS for 
referring to the formalism. We did a mistake in the past in using a 
name that nobody loves, but we should be careful now not to do some 
more mistakes. I've started to use deep inference with a different 
meaning than yours, so there's a possibility of confusion. Of course, 
I don't mind changing my use of the word, but I think we should 
discuss a bit the issue in order for all of us to come to an 
agreement. I'm going to send a separate email to Frogs about this.

5   Since we are at it: I think you confuse the reader by speaking of 
`formulae', while in practice you're using equivalence classes of 
them (if I'm not mistaken). I know, it's an old issue, but... At 
least, if you really don't want to use `structure', qualify a bit the 
word `formula'. In general, as for point 4, I think we all benefit 
from using a standardised terminology: we gained the respect of the 
community, but we're still struggling for gaining their attention, 
and common marketing strategies are, in my opinion, very valuable.

6   I think you can be bolder in your description of cut elimination. 
You say that you *first* eliminate the cuts on quantifiers and *then* 
those on atoms. If I'm not mistaken, after seeing your theorem, I 
think you can say it better: you can eliminate both kinds of cuts 
*independently*, what is even more modular.

I'm looking forward to see the final paper.

Ciao,

-Alessio