Re: A cut-free CoS system for S5

At 19:47 +0200 14/6/05, Phiniki Stouppa wrote:
>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?

I have no brilliant idea. However, I don't see anything wrong in 
using `deep inference', perhaps in quotes, when explaining the 
special case you're mentioning above. This will probably happen in a 
context where it's clear what you're talking about.

The problem I see is in defining the class of deep inference systems 
as including the display calculus, hypersequents, Schuette's 
calculus, etc. In this case, we would collect together formalisms 
that are only connected at a superficial level on one aspect, 
unboundedness of inference, and not on another important one, 
branching. In my opinion, we would spoil a strong term for not much 
in exchange.

By the way, there's something we didn't mention so far. It looks like 
most of our current research is in solving the problem of identity of 
proofs. This is a semantic problem, rather remote, in principle, from 
the technicalities of syntax. Wouldn't it be nice to be able to say, 
in a couple of years, that deep inference solves the problem?

-Alessio