Re: How to use `deep inference'?

At 16:13 +0200 14.4.04, Finiki Stouppa wrote:
>I also use deep inference as a property, in the way Alessio does.

I didn't get answers to my previous email about the use of deep 
inference. Please answer, it's important we take a decision! From 
what Phiniki says, it looks like she agree on using `deep inference' 
as the general name of the approach, rather than the name for a 
specific formalism.

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

First comment, probably obvious: I think it would be nice if there 
were also external reasons justifying the classification, like, for 
example, the ability to capture or not to capture a certain class of 
logics.

In other words, saying `display logic is an unbound system and 
hypersequents are bound' (based on a classification purely made by 
observing the shape of inference rules) is OK. However, it's much 
better to say the same and being able to add something like: `... and 
in fact display logic captures this <modal logic, whatever>, while 
hypersequents don't, since we know that bound systems cannot cope 
with <feature>...'.

Second comment: I'm not very fond of the word `absolute' for CoS 
rules, for two reasons:

1) There are formalisms which are more general than CoS, like for 
example the two I was proposing in the past months.

2) There are even more general notions of deep inference if we go 
beyond a tree representation of formulae/structures; for example, in 
relation webs you can do really wild things.

It is conceivable that one wants to discriminate subclasses in this 
big sea of formalisms more general than CoS, so I would try not to 
use ultimate words like `absolute'. (I'm confident that in his almost 
inexhaustible vocabulary Charles can find the right one!)

-Alessio