Re: A cut-free CoS system for S5

I think I concur with Alessio on the matter of the characterisation  
of Deep Inference as "fully deep" inference.

There's no doubt that even the classical sequent calculus can be seen  
as an inference system that is somewhat deep: if you think of a  
sequent of the form X |- Y as consisting of a conditional with a  
conjunction in the antecedent and a disjunction in the antecedent,  
then we can make inferences down to that depth.

Display logic presentations of modal or other substructural logics  
allow inferences to go inside more, allowing for existential  
operators (diamond, or fusion) in antecedent position and universal  
operators (box, or arrow, or fission) in succedent position, together  
with a dualising operator.  There's no doubt that this allows for  
more depth, but it doesn't provide a structure in which formulas can  
be /atomised/, and this is the difference when we compare with CoS.   
A disjunction in antecedent position cannot be converted into  
structure.  (Its inferential power is exhibited by branching in the  
sequent derivation: another way that the difference with CoS  
manifests itself.  Here hypersequents and display sequents are on the  
side of the sequent calculus, and CoS stands apart.)

(I'm beginning to form some ideas of why both approaches have their  
own advantages/disadvantages, but the *detail* is not completely  
clear to me yet.)

I'd be interested to hear if my take on this is thought to be  
idiosyncratic, or if it's a fair statement of the situation.

Best wishes,

Greg

On 13/06/2005, at 2:36 PM, Alessio Guglielmi wrote:
> The question is: Are the display calculus or hypersequents deep  
> inference formalisms? Should we consider them so?
>
> As far as I know, people in these areas never considered themselves  
> as doing deep inference. Am I right? I think the term `deep  
> inference' has been invented by Kai, actually. If so, I'm not sure  
> we should tag the display calculus or hypersequents with deep  
> inference, at least in context where there isn't a thorough  
> discussion.
>
> I see the reasons for the modal logicians: there is a clear  
> indication that, in order to do proof theory for modal logic, there  
> is a need of *some form* of deep inference. This is clear.
>
> However, the notion of deep inference we have, which is `inference  
> at any depth in formulae', is not obviously translatable into the  
> display calculus or hypersequents. My suggestions is to continue  
> arguing that these formalisms are `deeper' than the sequent  
> calculus, that `some form' of deep inference is necessary for doing  
> proof theory of certain logics, but to stop at this point, and keep  
> the idea of deep inference in its pure form of inference at any  
> depth. The reason is that the definition we have is simple and  
> clear, while using it for other formalisms makes it vague.
>
> Ciao,
>
> -Alessio