How to use `deep inference'?

Hello,

I propose to discuss a bit the use of the words `deep inference' and 
`calculus of structures'. I'd like to understand what is the opinion 
of the majority and I will stick to it, in the papers, the web site, 
lectures, talks, whatever.

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.

You also know that the formalism we use mostly is called the 
`calculus of structures', or CoS. There are perfectly legitimate, 
historical reasons to use this name, which I briefly recall. The word 
`structure' is used in philosophical logic to call exactly what we 
call structure, i.e., a certain kind of expression used in formalisms 
where the emphasis is on the structural component of deduction. This 
is exactly what we are doing, and the name `calculus of structures' 
precisely describes our deducing directly on structures, instead of 
mixed expressions involving sequents, structures and formulae, as, 
for example, in the well-known display calculus.

It looks like, probably for different reasons, many people don't like 
this name, including me. I find it pompous and lacking creativity. In 
fact, at the time I coined the name I couldn't imagine I will use it 
so much; at that time it was just a byproduct of relation webs (then 
called traces) and I didn't spend much effort into thinking about it.

So, the temptation would be to use `deep inference' in the place of 
`calculus of structures'. I believe this is a mistake, so I will say 
why and I will describe my current view of the subject.

I think that we can divide deductive systems into two categories: 
deep inference ones and shallow inference ones. The class of shallow 
inference contains the sequent calculus, natural deduction, tableaux, 
etc., while deep inference contains Schuette's calculus, (arguably) 
the display calculus and our own CoS, plus some more formalisms to 
come soon.

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

Of course, all of this is still vaporware, it requires a lot of 
development and I hope to find the resources for doing it, but it 
shows my reasons for keeping the words `deep inference' at a higher 
abstraction level than the one needed to name the single formalism.

Independently of all of this, there's the fact that CoS is now a very 
well-known name, it would be masochistic not to use it. My personal 
solution to the problem of my disliking CoS is to use the name very 
sparingly, and tending to argue about, for example, the `benefits 
that deep inference brings to proof theory' rather than the `benefits 
that CoS brings to proof theory'.

Not to use the name at all is, I believe, a mistake. Please let me 
know what you think, if you disagree but also if you agree. Sorry for 
the long email!

-Alessio