Re:Red and blue (again)

Hello Kids,

this email is brought to you by the colours blue and red :)

> What is perhaps surprising is that a two-level organisation can
> (more or less) work for four-connective logics (modal) or even
> six-connective ones, like linear logic. In my opinion, this is so
> only because all these logics are not very far from the classical
> one, and also because people actually did a lot of tinkering with
> the original organisation (like inference rules checking modalities
> in the contexts, etc.).

Agreed.

> Next question is: should we worry? My answer is that we should not,
> because the outcome of the experiment is an artifact of the sequent
> calculus. I think we also agree on this, do we?

Yes, the question is a distraction.

> To support this claim one should show an analytic proof system where
> the question has a different outcome. I think you agree with me: in
> order to prove my claim I used CoS, but it looks like you could use
> the display calculus to the same effect. Do we agree?

Yes.

> All that said, it seems there is a competition between the display
> calculus and CoS or deep inference in general. I tend not to be
> competitive because I think that different formalisms serve
> different purposes (some of which purely psychological).

Not quite. I feel that DL and CoS are relatives: you can compile any
DL calculus into a CoS calculus, and I suspect, there is always a DL
calculus for every CoS calculus, although Alwen may disagree here.

What I wanted to ensure was that there was no claim that DL *cannot*
break the equivalence because DL always uses the same meta-level. DL
gives us all the freedom that CoS gives us: that was all I wanted to
say.

> Anyway, regarding a possible competition, I think probably some of
> the important questions you have to answer, which perfectly fit this
> discussion, are: what about branching? What colour are branches in
> the display calculus?

If you use enough meta-level proxies then you don't need to ask this
question. For example, the DL calculus for LL has traditional branches
for and-right and tensor-right. But there is no confusion because the
first is purely extensional while the latter is purely
intensional. The meta-level "comma" or "semin-colon" allows us to keep
them apart.

> I think you see what I mean: on one hand, we all recognise that
> questions like colour-blindness require conserving `outer'
> information while going into formulae to be proved. On the other
> hand, in the display calculus you still have to build formula trees,
> which means pure, simple and *forgetful* structural induction. We
> all agree that this is not enough, so, in order to catch up, the
> display calculus has to introduce even more blobs. Where does this
> blobbitis end?

It ends when the DL calculus faithfully captures your logic. The same
is true of CoS: we have (..) and [..] and <...> and
... side-equations. When does it end ?

Next week we shall look at the number 4 and the colour green :)

raj