Re:A cut-free CoS system for S5

Ribbit all,

On Mon, 2005-06-13 at 14:36, Alessio Guglielmi wrote:
> The question is: Are the display calculus or hypersequents deep 
> inference formalisms? Should we consider them so?

I don't know much about hypersequents but, from the little I know of
display calculus, I believe that it ought to be considered as a form of
deep inference. For instance, suppose we are working in a display
formalism and want to use a version of switch. Let's look at how to do
this on the left of the turnstile. What we want is a rule that says
something like (where | is "or" and "&" is and):

(R|U)&T |- XoY
---------------  (*)
(R&T)|U |- XoY

How to show that this is admissable? Well, suppose that we have a proof
of (R|U)&T. Let us unravel it:


R |- T*oX   U |- Y
-----------------
  (R|U) |- *ToXoY
  --------------
  (R|U)oT |- XoY
  --------------
  (R|U)&T |- XoY

Now we can yank the proofs of R |- T*oX and U |- Y and travel by a
different path:


R |- T*oX
---------
 RoT |- X
----------
(R&T) |- X    U |- Y
---------------------
  (R&T)|U |- XoY
  

So, rule (*) is admissable. We can do the same thing for switch on the
RHS. (An aside: there is nothing dodgy with having XoY on the RHS of the
turnstile. Since the "|" connective can be properly displayed on the
left, it must have been introduced by the left rule for this connective
(since we restrict identity to atoms)).

> 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.

If one takes this to be the case, then display calculus certainly ought
to be considered as having some form of deep inference, especially in
light of Kracht's results on properly displaying modal and tense logics.

> 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. 

The trick I used above, of unravelling and "reravelling" a proof seems
to give one the ability to perform deep inference in your sense. That
is, unravel up the proof until the piece of the formula/structure you
want is displayed (this is guaranteed to happen). Then, perform the
inference you want and travel back down the tree. It is now as if you
performed that inference deep inside the formula. So, making hearty
abuse of terminology, I believe that deep inference is admissable for
display calculus. My arm waving above lends support to this hypothesis,
but I am yet to flesh it out.

What I see CoS as doing is allowing one to say the same thing without
all the "diddling". That is, one can point to a piece of a structure and
say something like "darn, I really wanted to weaken that piece of the
formula". In display calculus, one needs to travel up the tree to redo
it. In CoS, however, one can do it where it stands! 

Now, it is apparent that the deep inference mechanism in CoS is more
elegant, but whether this leads to stronger "provability power" is not
obvious (to me at least). Moreover, the fact that display calculus comes
equipped with a mechanism for handling polarity makes the answer even
less obvious.

best,
Jon