Re:Red and blue (again)

Dear Raj,

I guess we agree on many things, but there is still something... (not 
really related to the colours).

At 10:15 +1000 29/7/05, Rajeev.Gore-/[email protected] wrote:
>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.

Yes, but it is also important that the compilation preserves the 
properties of proofs. For example, CoS is very good for attacking 
bureaucracy, because it allows for many different normal forms. I 
think that the important questions are not really those related to 
how many logics one can do, but *how* they are represented, and 
(especially for me) whether there is a reasonable semantics of proofs 
(not necessarily in the categorical sense) associated to them.

A problem I see with the sequent calculus, for example, is that it 
might have an excellent `theory of meaning' associated to the 
inference rules and the connectives, but the way proofs are 
represented in the large, well..., it's the triumph of bureaucracy. 
It looks like the display calculus is even more baroque in this 
respect (please tell me if I'm wrong).

Now, as I said, I'm not competitive, I don't take bureaucracy as the 
only measure, for example, I'm sure that the philosophers are happier 
with the display calculus than with anything else.

My only point is that compiling one formalism into another is not 
enough, and in my opinion it only establishes a very tenuous relation.

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

My only claim is that taking a given meta-level means not choosing 
about the equivalence. This is true of the display calculus as well 
as of the sequent calculus.

What you propose is to change the meta level every time you have a 
different need. You can do that, but what happens to the `theory of 
meaning', to the general cut elimination theorem, etc.? I mean: the 
value of a meta level should be to be fixed once and for all, isn't 
it?

I'm probably missing again many things here, but don't do like David, 
be specific on what I'm missing!

>>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 ?

I can't believe you don't see the difference!

Given a language with 10 connectives, I just use 10 connectives in 
CoS, which is the moral, legal and mathematical minimum.

Given the same in the display calculus, you use 10 at the object 
level and 10 at the meta level! Who pays for this bureaucracy? You'd 
need a bit of Berlusconi in Australia, I hope we'll send him over to 
you.

-Alessio