Re: How to use `deep inference'?

> 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 agree: just think of allowing arbitrarily many context schemas in an 
inference rule (not just one like in CoS). The formalism still works on 
formulas but is strictly more expressive than CoS in terms of inference 
rules. Such rules are even deeper than CoS rules, so the deepness of CoS 
is not "absolute".

Two more comments:

1) I'm happy with using CoS as formalism and deep inference as a 
property (of a bunch of formalisms) as I just did. I'd just emphasise 
"deep inference" rather than "CoS" as the main idea that's behind the 
good properties we get.

2) Charles' categorisation looks a bit unnatural to me. I suppose that 
the "extra" in "extra connectors" for "relative deepness" means "in 
addition to comma and branching" of the SC. Now, my (probably ignorant 
and CoS-centric) way of looking at it is that already the SC has 
connectives (the structural ones, i.e. comma and branching) that are 
"extra" with respect to the what is the minimal set of connectives 
needed: just the logical ones. I thus think that a categorisation should 
start by distinguishing whether or not there are any extra connectives 
at all in addition to the logical ones and should not start by 
distinguishing whether or not there are extra structural connectives in 
addition to the ones that Gentzen happened to come up with.


-Kai