Re: A cut-free CoS system for S5

Hello,

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

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.

I think that this difference must be given a name, and I thought that 
deep inference could be that name, or at least this is the way I used 
it so far. If we put the other formalisms under the deep inference 
label (without even being asked to ...), then we need another label, 
I believe.

Clearly, this is not a vital matter, but we expect from the Lisbon 
workshop to start new formalisms in the `deep inference' hierarchy

    CoS -> Formalism A -> Formalism B -> ... -> deductive derivation nets ,

and I think it's good if we agree on the terminology. (I also think 
in Lisbon we better discuss technical matters, since we are there in 
person with a blackboard.)


Greg: I agree entirely.


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

Some more comments:

At 16:56 +1000 13/6/05, Jon Cohen wrote:
>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.

If you restrict yourself to classical and modal logics, I agree. 
However, the display calculus has a predetermined amount of 
meta-level structure. You can almost certainly invent a logic with 
such a rich language that the meta-level becomes insufficient.

If you want to see one of the rare, truly beautiful mathematical 
ideas, look at Alwen's paper <http://www.loria.fr/~tiu/deep.pdf>. 
There, Alwen describes a logical fractal which shows that deep 
inference is necessary for a certain language.

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.

>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! You're not limited by *any* 
meta level constraint. This is not so extraordinary, though, since 
CoS has no more provability power than a Hilbert system.

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.

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.

>Moreover, the fact that display calculus comes equipped with a 
>mechanism for handling polarity makes the answer even less obvious.

You can handle polarities in CoS as well, see the recent work of 
Alwen on intuitionistic logic: 
<http://www.loria.fr/~tiu/localint.pdf>.


Charles: we can agree on the taxonomy you propose, but how do you 
address the point I raised above?

At 16:37 +0200 13/6/05, Charles A Stewart wrote:
>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.

Because there was no necessity! In the case of intuitionistic logic, 
see Alwen's paper.

In any case: what could the difficulty be? Of course you can invent 
negative and positive contexts and double the number of rules (and 
start creating a bureaucracy). What would be the point in doing so if 
one can do without?


At 09:40 +1000 14/6/05, Rajeev.Gore-/[email protected] wrote:
>I would even argue that there are reasons why we might want to avoid 
>deep inference. That is, it should be derivable but not necessarily 
>built in from the start to make sure that our rules capture 
>substitution properly.

What is the problem with substitution? Regarding derivability of deep 
inference, see above for my opinion. I mean: I don't think that any 
CoS system can be captured, as far as its provability goes, by a 
display calculus system. I think one can build a counterexample by 
generalising Alwen's one.


Ciao,

-Alessio