Re: A cut-free CoS system for S5

Hi Alessio, hi amphimaniacs,

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

The terminology I'm now favouring is distinguishing three kinds of
depth:
  1. Surface inference: what you get with no-frills Gentzen sequent
  systems: for LK-like systems this means you can swim about
  outermost disjunctions and no deeper.  (Note that one can be less
  deep even than this: ie. the Hilbert calculus, and Alessio has
  suggested one may even be able to get cut-elimination result for
  some such depthless inference systems).
  2. Non-surface inference: able to perform inference deeper than this:
  the hypersequent calculus is an example of this; the system for S5
  allows you to freely act around disjunctions inside necessities
  inside disjunctions, but no deeper.
  3. True deep inference: there is no bound on the logical complexity
  that you're able to move about in.  Hence display logic is truly
  deep.

Display logic does have a catch, and the way I would put it is this:
in order to maintain the subformula property, it is necessary to
"freeze" formulae that are produced by logical (as opposed to
structural) inference rules.  This means that conjunction-like rules
force a separation of their premisses, and so the inference takes
a tree shape that has no possibility of different branches sharing
information.

You can call this a restriction on the application of inference, but
it is not a restriction on the depth at which inference is performed,
rather it is like walls closing in and squeezing out the possibilities
for structural manipulations as one approaches the conclusion.  On the
other hand, display logic has the possibility of manipulating negative
structure in a manner that we haven't really figured out how to do in
CoS yet.

Charles

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

For S5 you need very little beyond surface inference, but to get really
clean results it looks like you need to go quite a bit deeper.  I'd
love to know more about how to tell how much depth a given modal
logic needs.
 
> 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.

I'm guessing you won't like my definitions, then.

Charles