Re: predicate logic and deep inference

At 14:46 +0200 8.4.04, Kai Brünnler wrote:
>>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.

Last thing I've heard about this is that you, 
Charles and I should write this paper. Let's do 
it!

>I vote for dropping CoS in favour of deep 
>inference, for several reasons, in particular 
>because I find "Calculus of Structures" too 
>generic.

But deep inference is even more generic! And 
then, really, we cannot change the name of the 
formalism after four years and so many papers.

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

No, in my opinion this is not right. There are 
many reasons, I'll tell you just one.

In CoS *any* natural normalisation procedure is 
bound not to be confluent, simply because of the 
sequentialisation imposed by the formalism. In 
`A' and even more in `B', instead, you'll have 
that most normalisation procedures will be 
confluent, because of the possibility of putting 
in parallel different `branches' (they're not 
really branches but you get my point).

This alone is such an important feature that 
should require different names, even if we know 
very well that the difference is more superficial 
than it seems.

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

I agree with all you said above. I had the 
impression that indeed you could `eliminate them 
independently'. I'll read your paper with more 
attention.

-Alessio