Re: How to use `deep inference'?

Hi,

I also use deep inference as a property, in the way Alessio does. In 
the CoS deep inference is explicit since the inference rules are directly 
applied in any depth. This means that we can freely apply rules in any 
substructure. This is not possible in other systems. In display logic, for 
example, while we can reach (display) any subformula, rules can be freely 
applied only if there are no constraints on their side formulae (which is 
not true for the modal rules).

Charles thought of a classification on systems with deep inference, based 
on the depth of their rules: 
1. "Absolute" for deep rules (CoS). We can reach any subformula for free.
2. "Relative" for shallow rules. In this case deep inference is obtained 
by using extra constructors and so, new structural rules. This means that 
subformulae can be reached by rule applications. Here a further separation 
is possible:
  i. "Bound" rules when rule applications are bounded by the number of the 
constructors. An example is hypersequents, which are finite sets of
usual sequents.
 ii. "Unbound" rules, otherwise. Display logic deals with classes of 
sequents and thus, constructors like the * can appear without limitations.

The definitions are still loose. Any comments are welcome.

Phiniki

On Thu, 8 Apr 2004, Alessio Guglielmi wrote:

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