Re: Red and blue (again)

At 18:20 +0100 28/7/05, David J. Pym wrote:
> The order of discovery is irrelevant.

Then, I don't understand your argument. Let me try and make a scheme 
of what I understand, which shows why the order is relevant:

1) There's LL sequent calculus, which happens not to induce 
equivalence on coloured modalities.
2) People find models for it, which of course don't exhibit that 
equivalence, either.
3) You say: it's good that the sequent calculus behaves that way, 
because this is what the models suggest.

So I say: of course! The models are made for it!

My reaction would have been different if all started from the models, 
as in this hypothetical situation:

1) There are nice and universally appreciated models, which happen 
not to induce equivalence on coloured modalities.
2) One looks for a formalism and a deductive system in it which is 
complete for the models, and one finds that the sequent calculus 
deals graciously with the problem. In this case I would agree with 
you when you say that this is good of the sequent calculus.

You see what I mean?

Perhaps what you really mean is that, for you, the existing models of 
linear logic are so natural and so right that just the thought of 
different models and deductive systems that behave differently 
disturbs you. On this, I take no position, simply because I'm too 
ignorant and never developed an opinion.

> By all means invent others logic with different properties that you 
> like better, but the one mentioned is well-motivated and has some 
> unavoidable mathematical properties that are well-handled by its 
> sequent calculus.

On this, too, I don't argue, because, as I said, my only problem is 
to design syntax (based on good, *general* principles of proof 
semantics) which is completely agnostic regarding specific logics, 
and able to accommodate all reasonable needs.

> The phase semantics is a very different matter and irrelevant in 
> this context. The *semantics of proofs* to which I referred is 
> mathematically natural and has good computational examples.

We're talking about logical equivalence, so phase semantics is 
relevant, because you could have used it to prove or disprove 
equivalence of colour modalities, and so argue about the naturalness 
of LL sequent calculus *if only the semantics preexisted the 
calculus*.

Am I missing anything? (It's a bit late but I still didn't drink my beer.)

-Alessio