Re: A cut-free CoS system for S5

At 2:05 PM +1000 15.6.05, Jon Cohen wrote:
> Ribbit,

Hello,

I'm attempting a very quick reply, as I have a train to catch in less 
than two hours.

Let me first tell you my opinion on this general business. I believe 
that in the past there has been an excess of syntax. I mean, 
sometimes it looks like we are in a circus where people take pride in 
juggling more and more expressions, sequents, etc. Part of the 
problem is that there are many computer scientists doing proof theory 
(like myself), and in general they're not afraid of syntax 
(wrongly!!) and actually they like it perversely.

I think we agree that the biggest and most interesting open problem 
is to give semantics to proofs. Now, in order to do so, we do need 
syntax, but I think that if we have too much of it, then we won't be 
in a position of having the right intuitions, find the right 
characterisations, etc.

This is to say that, as happens in many cases, several formalisms can 
be equivalent on *what* they compute/prove/do. However, what matters 
most is *how* they do it, and this how is not just technical, but 
also psychological, it must help intuition.

All that said, I think there are a few problems in the considerations 
you make, I'll try to address all of them (quickly):

1) I thinnk you don't always have a rule

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

in the display calculus for every rule

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

in CoS. In display, you have to introduce connectives going down, if 
I'm not mistaken, so you have to depend on the punctuation symbols 
you have available at the meta level. Moreover, if the main 
connective in B requires branching, what do you do? So, I don't think 
your argument proves that deep inference can be simply mimicked in 
the display calculus. I might be missing something here, as I'm no 
expert of display calculus and I cannot check my papers right now.

2) "Where does the meta level go in CoS?" Nowhere: there really is 
only one level of connectives/logical relations, which is the one 
expressed by parentheses, and only because this is typographically 
more effective than infix operators. Associativity, commutativity, 
etc. have nothing to do with a meta level, in fact you can simply 
express them as normal inference rules if you need to do so.

Another general thing that I believe is that this thing of the meta 
level has been blown out of proportion. In the beginning, Gentzen 
found convenient to use commas and branching as proxies for `or' and 
`and'. This was because, for doing cut elimination, he needed to 
break formulae and proofs into pieces and then rearrange the pieces. 
Maybe he started from branching because this is what you have in the 
modus ponens.

Then philosophy came and started seeing a meaning in doing so (which 
I don't dispute, I agree on what they found). But then again, the 
thing got *too* complicated, and now the `sequent-style' presentation 
suffers from all sorts of technicalities and deviations from the 
original purity and effectiveness.

That's just a very quick, rough and rude opinion, but I have a train to catch!

3) Branching is implicit in CoS. Again, I disagree. It's true that, 
in my BV paper, (A B) branches somehow A and B, but this is only 
because the BV logic is linear. In classical logic, for example, you 
have the medial rule

   S[(A B)(C D)]
   ------------- .
   S([A C][B D])

You can see that A and D are in conjunction in the conclusion, but in 
a disjunction in the premise! So, they can communicate again. This 
you really cannot do in the sequent calculus or in the display one. 
However, this is *precisely* the reason why, for example, contraction 
can be made atomic, and so permuted around in a proof, and this has 
important consequences on proof nets and semantics of proofs.

The medial rule and its *non-branching* nature are very important for 
the semantics of proofs. I live more comments to Francois, Lutz and 
Richard on this (train!).

Gotta go. I'm not sure I addressed all the points. Please, if you're 
not convinced or I missed something, let me know, on the list, or 
privately as you see fit. I really appreciate what you're doing. 
Understanding the relation to the display calculus has always been 
one of our concerns.

Ciao,

-Alessio


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