Re: predicate logic and deep inference

Alessio,

> 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. 

Sure, sorry for giving this impression.

> 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.

Is it? It's floating around for propositional logic, not for predicate 
logic, unless you know something I don't know. Btw, are you going write 
down formally splitting for propositional logic? If not, I could put it 
into one of my background threads.


> 4   I see that you're using `deep inference' instead of CoS for 
> referring to the formalism.

Yes. I vote for dropping CoS in favour of deep inference, for several 
reasons, in particular because I find "Calculus of Structures" too 
generic. My current view is that your formalisms "A" and "B" aren't 
different formalisms, but the same formalism (whatever that may mean) 
with some bureaucracy removed. In any case I'd like to avoid arguing 
about the name and I'm perfectly happy to continue using "CoS" as well, 
should the majority be in favour of that or if you have strong feelings 
about it. Of course the name "CoS" will appear in the paper somewhere no 
matter what, if only for historical reasons. Preferably in a footnote 
though.  <-- funny, laugh!



> 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).

You can't tell from the draft I sent. And technically it doesn't matter. 
I have to decide this now that I put the definitions.

What's more important, i.e. what matter's technically, is to see whether 
vacuous quantifier should be a rule instead of an an equation. Turning 
it into a pair of rules would allow eliminating it's up-part, and that 
could be important.

> 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'.

I really prefer "formula".

  > 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 would find that misleading. Of course any two rules that are 
admissible for a system are "independently" admissible in some sense 
because you can simply eliminate both of them then add one or the other 
or both "independently", according to your taste. However "eliminating 
them independently" to me suggests that 1) I can eliminate the first 
from a proof without touching the second _and_ 2) I can eliminate the 
second from a proof without touching the first. I only have procedure 
for 1) and I don't see how to do 2). That's why I don't use the word 
"independently".

-Kai