Re: A cut-free CoS system for S5

On 6/14/05, Alessio Guglielmi <Alessio.Guglielmi-r/[email protected]> wrote:

> I think that we have to consider an important point: when one says
> `inference occurs at any depth in formulae', one says *much more*
> than `any part of a formula is accessible to inference'. 

I agree. Also in that CoS is the only deep inference formalism. But I
am also using 'deep inference' as a property of *systems* (i.e.
independent of the calculus) in the following sense: a system enjoys
deep inference if
1. it has inputs of unbounded depth and
2. it has at least one (possibly admissible) rule which is applicable
at any depth.

accordingly, some systems out of CoS might enjoy deep inference
although they are not systems of a deep inference formalism.
Apparently this is confusing, I should change the name. Ideas?

Phiniki