Re: A cut-free CoS system for S5

Ribbit,

I need more time to think about some of the concerns Alessio raised, but
thought that I would give my initial impressions. My goal is to
understand CoS and the essential differences between it and display
calculus, so I'll take this opportunity to try and elucidate my
feelings. Sorry for the long post!

On Tue, 2005-06-14 at 15:16, Alessio Guglielmi 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'. The 
> difference is that the meta level disappears entirely! Inference 
> *occurs at* ... (With meta level, I intend the structural level of 
> punctuation symbols, commas, branching, etc.)

Ok, this definition of deep inference seems different from what I had
previously understood it to be, derived from some reading. In [Br], Kai
defines an inference rule to be deep if both the assumption and
conclusion contain a schematic context. That is, if we have something
like:

  S{A}
p ----
  S{B}

It is defined in pretty much the same way by Alwen in [Tiu]. This
particular definition strikes me as being very close to display logic.
The sense in which I mean this is, suppose we have a rule:

A |- X
-------
B |- X

If we then come across something like S{A} |- X, then by the display
property we can move to A |- f(S){X}, apply the inference rule to obtain
B |- f(S){X} and then undisplay by going back to S{B} |- X. So, really,
we could have made the rule to be:

S{A} |- X
----------
S{B} |- X

This is more or less what I mean when I say that deep inference is
admissable for display calculus. 

Now, the foremost question is "Where does the meta level go in CoS?".
I'll give my take on each of the aspects that Alessio listed above.

** Punctuation symbols/commas: Unless I am mistaken, Alessio is
referring to the reliance of display calculus on different punctuation
symbols, such as 'o', which acts like Gentzen's comma. These punctuation
symbols are purely proxies for the symbols they represent. For example,
for disjunction on the right, we have the rule:

X |- YoZ
---------
X |- Y|Z

There is nothing wrong with adding the inverse of the above rule also,
since this is admissable ([Kracht] does this explicitly in his modal
calculi). That is, we can also have:

X |- Y|Z
--------
X |- YoZ

So, 'o' is there purely to make diddling around with the display
property more transparent. Now, CoS has "punctuation" of its own -- the
various brackets. When we give a structure like (A,B), what we really
mean is A & B. In Display logic, we can change the symbols, in CoS we
cannot. To my mind, this is not a substantial difference.

** Branching: The two most striking properties of CoS are that proofs do
not branch and the cut rule looks really odd! This puzzled me for quite
a while, but my understanding now is that they are different aspects of
the same phenomenon.

Where does the branching go? Since the original CoS systems are built
around the idea that we are working "on the right of the turnstile",
there are two sources of branching. These are from the and-introduction
rule and the cut rule. Now, traditionally, a cut rule serves two
purposes: "merging branches" and enforcing bivalence. In CoS, it
seemingly only enforces bivalence. The reason why this works out is
because CoS really does branch, albeit internally to the syntax. What I
mean by this is that suppose one is travelling up a proof and happens
upon (A,B). Then if you push up another level, A and B are not allowed
to communicate ([Gug, page 18]). But this is precisely what branching
is. This point is hammered home when we derive sequent-style cut for a
CoS system. The pattern is that we have proofs of |- X,a and |- Y, ~a.
Or, in CoS syntax, of [X,a] and [Y,~a]. In order to cut on a, we first
need to "make them communicate" and then "enforce bivalence". In
sequent-style calculi (including display calclus), this is done in one
step. In CoS, we need to do it in two steps by first bringing them
together into ([X,a],[Y,~a]) and then enforcing bivalence (by first
switching a bit to bring a and ~a together and then applying the cut
rule).

** Remaining Meta: The remaining "meta-level" aspects are, I suppose,
certain structural rules including associativity, commutativity etc. In 
display logic, these are stated explicitly as rules, whereas in CoS
these are hidden away in the equational base. However, when performing a
deduction in a CoS system, one invariably needs to use an "inference",
which is derived from the equational base. How is this not seperating
the meta level?


> I mean: in the sequent calculus you break formulae apart and put the 
> pieces on the desk, in hypersequents you have a couple of desks, in 
> the display calculus you have an entire ministry. In deep inference 
> (the way we called it so far) you just don't break the formula into 
> pieces: when you do inference you do it on the spot. In formalism B, 
> you can even replace a subformula with an entire derivation, but you 
> do it on the spot, you don't scatter all around the context.


> Jon: I think we might agree on the technical parts, but do you agree 
> on what I said above?

I agree that CoS does "inference anywhere deep" more elegantly than
display logic. 


> I think you can generalise the fractal to a language richer than what 
> the display calculus can handle, perhaps something with as many 
> operators as there are punctuation symbols, plus one. In that case 
> you would obtain a logic that CoS can prove and the display calculus 
> cannot.

I need to think about this more...


> >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).
> 
> Of course CoS has more provability power! 

What I meant is whether there is a system that can be captured in CoS
but not in display calculus, in the sense of BV for CoS/sequents. At the
moment, I still do not share your certainty that this is the case. Of
course, it would be great if it is the case, since I do rather like
CoS...


> I don't think provability should be the point. The point is making 
> interesting proof theory, which, I believe, is something that applies 
> to a much restricted class of languages than those that are provable. 
> In fact, you don't do proof theory with Hilbert axioms.

Ok, but this is breaking with the traditional use of the term. A first
thought would be to call the study of proofs "proofs theory", but that
sounds truly horrendous :)

I agree that doing proof theory via Hilbert systems is not ideal. For
instance, Girard has made the observation (on several occasions) that
cut elimination is the "true" completeness theorem. I agree with this
sentiment. 

> What is so nice about the work that Phiniki and Charles did 
> <http://www.linearity.org/cas/supervision/phiniki04sbm.pdf>, is that 
> you can take Hilbert axioms for modal logic and turn them into very 
> simple CoS inference rules over which you can do proof theory.

I still need to read that paper properly. However, this sounds very
similar to what [Kracht] did for modal logic: any hilbert-style modal
logic axiomatizable by primitive axioms can be properly displayed. 

best,
Jon

[Br] Deep Inference and Symmetry in Classical Proofs. Kai Bruennler.
[Gug] A system of interaction and structure. Alessio Guglielmi.
[Kracht] Power and weakness of the modal display calculus. Marcus
Kracht.
[Tiu] A System of interaction and structure II: The need for deep
inference. Alwen Tiu.