Re:Red and blue (again)

Hi Alessio,

> If differently coloured connectives are all reduced to the SAME meta
> level (the classical one), then, OF COURSE, one gets equivalence.
> And, OF COURSE, equivalence is missing when there is no meta level
> corresponding to the connectives, like in the case of linear logic
> modalities.

Yes, this was one of the motivating reasons for Wansing's display
calculus for modal logic: it could derive equality of blue boxes and
red boxes.

> So, the sequent calculus is only apparently half-adequate to deal
> with the situation, and I guess the same is true with every
> formalism which commits to a fixed meta level, like hypersequents
> and the display calculus.

Not sure what you mean here Alessio. What is wrong with translating
into a fixed meta level ? The problem with traditional sequent calculi
is that they have no meta-level connective for box at all. Thus the
red-box right rule has to look for red-boxes in the antecedent so it
can construct the corresponding premise. But when faced with 
  [blue] p |- [red] p 
as a conclusion, it gets confused, and it can't construct 
  p |- p
from this situation.

Raj