Re: Red and blue (again)

The order of discovery is irrelevant. A modality
of the linear logic kind simply has that structure.
That structure has some mathematical properties that
are unavoidable. Given that there are good examples of wanting
modalities of that form, interest in their properties is
justified.

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.

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.

David


Alessio Guglielmi wrote:
> At 15:54 +0100 28/7/05, David J. Pym wrote:
> 
>>> In linear logic, this works for all connectives but not for the 
>>> modalities: differently coloured modalities are independent, they 
>>> aren't equivalent.
>>>
>> Well that's good.
>>
>> Mathematical models of linear logic's proof theory (MLL!, for simplicity)
>> are given by monoidal categories (for tensor, implication, etc) with a
>> monoidal co-monad for the exponential, ! .
>>
>> There is no reason why (the co-algebras for) two different monoidal 
>> co-monads
>> should be equivalent. So it would be unfortunate if their 
>> axiomatizations were
>> equivalent (no completeness, for one thing).
> 
> 
> If I'm not terribly mistaken, these models were found *after* the 
> definition of linear logic's sequent calculus. In that case, I don't see 
> your point. I mean: if the properties of the sequent calculus of linear 
> logic were different, people would have had to look for different 
> complete models.
> 
> You could make the same argument with phase semantics, but, again, it's 
> a semantics that came afterwards, meaning that it simply tries to catch 
> up with the syntax (I almost completely agree with Giorgi on these 
> matters).
> 
> Anyway, I agree that the fact that differently coloured modalities of 
> linear logic are not equivalent is good, simply because they don't 
> behave the same way if you just colour the modalities rules, as I argued 
> in my answer to Raj.
> 
> -Alessio
> 

-- 
Prof. David J. Pym                Telephone: +44 (0)1 225 38 3246
Professor of Logic & Computation  Facsimile: +44 (0)1 225 38 3493
University of Bath                Email: [email protected]
Bath BA2 7AY, England, U.K.       Web: http://www.bath.ac.uk/~cssdjp

Royal Society Industry Fellow, HP Labs, Bristol: [email protected]

This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed.