Re: Red and blue (again)

At 19:44 +0100 28/7/05, Paul B Levy wrote:
>To expand on David's argument: for many of us, what makes us 
>interested in linear logic and similar systems in the first place is 
>primarily the models, not the proof theory (can I say that on this 
>list?).

Just speaking for myself, I certainly support this. I don't know the 
models enough, but, for example, I definitely agree that the proof 
theory of linear logic has some serious flaws. (I should say that it 
was and still is an important proof theory and certainly I owe much 
to it.)

However, one thing is to consider the models interesting, another is 
being religious about them.

>The order of motivation (I'm interested in X, therefore I'm 
>interested in Y) for an
>individual may differ from the historical order.

Myself included, agreed. The only reason why I mention order is that 
categorical semantics was born for the sequent calculus, which means 
(to me) that it's a bit unfair to judge the sequent calculus against 
it.

I think that it is conceivable that in order to capture interesting 
proof theoretic properties we will have to innovate a lot in the 
semantics, which could also mean using less natural constructions.

Perhaps there is no free lunch: on one hand you get wonderful models 
for a so-so proof theory, on the other you might need so-so models 
for a wonderful proof theory. I don't know.

Good night!

-Alessio