Re:Red and blue (again)

At 09:42 +1000 28/7/05, Rajeev.Gore-/[email protected] wrote:
>>However, the existence of another proof theory (for example, CoS), 
>>where the outcome of the experiment can be chosen at will, shows 
>>that the experiment only reveals an artifact of the sequent 
>>calculus.
>
>But display logic also give you this freedom. Instead of turning red 
>boxes and blue boxes into black blobs (say) at the meta-level, you 
>can turn red boxes into red blobs and blue boxes into blue blobs.

But of course!, sure!, and you can also have the same freedom in the 
sequent calculus by painting commas and branches, as Jon suggested. 
However, this entirely misses the point of the original question. Let 
me try in a different way to explain the point as I see it.

First of all, what does the plain sequent calculus do? For proving a 
formula, it takes it and breaks it into pieces, then organises the 
pieces in a two-level (hierarchical) structure: an outer 
`conjunction' (branches) and an inner `disjunction' (commas). Gentzen 
proved that this can provide an analytic proof system for classical 
logic, and this is not surprising (with hindsight, of course).

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

Back to the original question of colour-blindness. Asking the 
question means asking whether *forgetting* the colour when mapping 
formulae into the two-level organisation maintains logical 
equivalence or not. The answer is always trivial and we always agree: 
sometimes equivalence is maintained, sometimes it's not.

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?

The problem with the question `What about colour-blindness?' is that, 
posed this way, it looks like an important, fundamental question. 
However, I argue that the question actually is `What about 
colour-blindness in the idiosyncratic bureaucracy of the sequent 
calculus?'. If you agree with me, then the question is not a 
fundamental one, because it asks for a logical property (equivalence) 
as a dependency of a purely computational device (the way the sequent 
calculus performs structural induction).

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?

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). For me, CoS is the 
first step towards a bureaucracy-free, semantics-independent proof 
theory, which is a task that needs deep inference. I also consider it 
a much nicer proof theory than the traditional one, but I might be 
biased.

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?

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?

-Alessio