Re:A cut-free CoS system for S5

At 21:42 +0200 2/6/05, Phiniki Stouppa wrote:
>attached is a paper (draft) I've written lately on the technical
>results of my master thesis (completed last October in Dresden,
>supervised by Charles Stewart). It is entitled "a system of deep
>inference for the modal logic S5" and presents a cut-admissible system
>for S5 in the calculus of structures. A short elaboration on the
>importance and consequences of deep inference in modal systems is
>given in the introduction.
>
>I am planning to apply the final corrections/changes and submit it for
>publication by the end of next week. Comments/suggestions/corrections
>are more than welcome.

Hello,

I'm sending you several comments privately. I have one issue which 
could be suitable for discussion on the list.

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