Re: Red and blue (again)
"David J. Pym" <[email protected]> Thu, 28 Jul 2005 18:37:42 +0100
| Newsgroups | gmane.science.mathematics.frogs |
|---|---|
| Message-ID | <[email protected]> |
By the way, the structures in question, for the fragment I mentioned (without LL's "additives"), date from Lambek's work around thirty years ago; and the mathematical structure, including what amounted to the modalities, was certainly the primary concern there. See the sequence of papers, Deductive Systems amd Categories, I, II, and III. 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.