Subject: Re:Red and blue (again)
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-07-26 23:10:24 GMT (3 years, 49 weeks, 1 day, 6 hours and 36 minutes ago)
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