Re: How to use `deep inference'?

Hello Frogs,

There was recently some discussion on the list about terminology: 
"deep inference" vs. "calculus of structures" (CoS)
Since Alessio asked, I will here explain my personal opinion about the matter.

I mainly agree with Alessio, that "deep inference" is more a general concept, 
whereas "CoS" is a concrete formalism. Both are two different things, and one 
can not simply drop one in favour of the other. (I am not going to discuss 
the "marketing reasons", that Alessio has already explained; I fully agree 
with him on that.)

On Thursday 08 April 2004 11:13, Alessio Guglielmi wrote:
> As you perhaps know, it took some years for us to understand what is
> the most important concept we are using. In the end, Darwin spoke and
> it is deep inference, while top-down symmetry and other contestants
> lost the race.

I think the situation is more subtle. Of course, deep inference is THE main 
concept that makes the CoS work, but there is certainly more to it. Deep 
inference as such appeares also in Schuettes work and in Display logic, and 
also in "sequent systems", for example Bunched Implications and Abrusci-Ruet 
Noncommutative Linear logic. But all these logical systems use deep inference 
because they cannot do without, but they do not explore the new possibilies. 
They somehow stick to the "sequent style thinking". This is where CoS is 
different. It can be seen as a formalism (i.e. a methodology for presenting 
inference rules of a logical system) that starts from deep inference (and 
does not dodge to it as an unavoidable malady) and explores it by designing 
the rules in a clever way. This "clever way" is what distinguishes the CoS 
from other known formalism that have some deep inference, and what gives us 
all the nice properties like top-down symmetry, decomposition, etc. It is 
also this "clever way" that we still do not fully understand. All we have so 
far is the "recipe for the core", and some vague idea for the non-core, 
provided it is weakening and contraction. Alessio, any news about subatomic 
logic?

> In my personal research perspective, I see Deep Inference as the
> frame in which I developed CoS and will develop two other formalisms,
> which for now are called `A' and `B'. I sent an email before
> Christmas about formalism `A': it's a formalism in which derivations
> can be composed according to the same rules structures are made by:
> this removes a good deal of bureaucracy. Formalism `B' goes one step
> further, as I argued in an email to Frogs in February, and removes
> further bureaucracy from `A' by allowing inference rules between
> derivations.
>
> The three formalisms, CoS, `A' and `B', are connected in the sense
> that `A' is an abstraction of CoS and `B' is an abstraction of `A',
> so that CoS describes faithfully the others, it simply contains more
> information. Beyond `B', there should be proof nets (perhaps `B' is
> already proof nets, I don't know yet).

I have the impression that "A" pushes the idea of "deep inference" even 
further than CoS. My guess is that it will lead to new normal forms, once we 
have found the right notation.

For "B", I have the feeling that it (if done correctly) is already proof 
nets, and that in this case it is arguable, whether it still makes sense to 
talk about "inference". In other words, I am not sure, whether it is really 
"deep inference" as concept that teaches us to do the right proof nets. But I 
am convinced that the CoS (with its "clever-way-rules") can tell us 
something. At least I found proof nets for MLL with units, as well as proof 
nets for classical logic out of that---I will post it on frogs in a separate 
mail.

Summarising, let me say that I will continue to use "CoS" and "deep 
inference" in parallel, with the meanings that I tried to indicate above.

-Lutz