From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4940 Path: news.gmane.org!not-for-mail From: soloviev@irit.fr Newsgroups: gmane.science.mathematics.categories Subject: Re: Famous unsolved problems in ordinary category theory Date: Sat, 6 Jun 2009 11:18:12 +0200 (CEST) Message-ID: Reply-To: soloviev@irit.fr NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain;charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1244327050 17540 80.91.229.12 (6 Jun 2009 22:24:10 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 6 Jun 2009 22:24:10 +0000 (UTC) To: "Thomas Streicher" , categories@mta.ca Original-X-From: categories@mta.ca Sun Jun 07 00:24:08 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1MD4J5-0005uG-HQ for gsmc-categories@m.gmane.org; Sun, 07 Jun 2009 00:24:07 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MD3oK-0003Ku-6B for categories-list@mta.ca; Sat, 06 Jun 2009 18:52:20 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:4940 Archived-At: Dear All - Here a question related to categorical logic (or categorical proof theory= ) of a very different type. I would like to put it here because it is an illustration of another part of the field and also because it is technically difficult and interesting. It is well known that certain systems of propositional logic have a natural structure of free category for certain classes of categories with structure. For example, we have a structure of free Symmetric Monoidal Closed Category on the Intuitionistic Multiplicative Linear Logic. In thi= s structure formulas are objects and equivalence classes of derivations of the sequents A -> B are morphisms. Free SMCC (in presence of "tensor unit" I) is not "fully coherent": there are non-commutative diagrams. For example, one has the Mac Lane's example A*** -> B*** (called "triple dual diagram"). In terms of IMLL there exist two non-equivalent derivations of ((A-oI)-oI)-o I -> ((A-oI)-oI)-o I w.r.t. the equivalence of free SMCC on the derivations of IMLL. One derivation is identity, another derivation is obtained in obvious way using the derivability of ((A-oI)-oI)-o I -> A-o I. Let us denote these derivations 1 and f respectively. (For the sequent ((A-oI)-oI)-o I -> ((A-oI)-oI)-o I every derivation is equivalent to 1 or to f.) The "triple dual conjecture" says that if we declare f\equiv 1 then all the derivations with the same final sequent in IMLL will become equivalent. I.e. the stronger categorical structure than SMCC (obtained b= y adding this new axiom for equivalence/ commutativity of diagrams) will be "fully coherent". If it is true we would have an interesting new variety of categories (subvariety of SMCCs) in the sense of Universal Algebra. Proof-theoretically, the study of this conjecture requires to study the equivalence relations on derivations of IMLL between the relation of free SMCC and the relation that identifies all derivations with the same final sequent. In my paper S. Soloviev. On the conditions of full coherence in closed categories. Journal of Pure and Applied Algebra, 69:301-329, 1990. it was shown that - if the "triple dual diagram" is commutative w.r.t. some equivalence relation ~ (containing the relation of free SMCC) - and the following additional condition holds: [a-oI/a] h ~ [a-oI/a] g =3D> h~g for any two derivations of the same sequent, then all the derivations of the same sequent in IMLL become equivalent. The additional condition is a) difficult to verify b) has the form different form the equational form ("commutativity of a diagram") require= d from the point of view of Universal Algebra approach. All the attempts to prove "pure" triple dual conjecture (by myself and others) did not yet succeed. One may mention that it is known that some intermediate equivalence relations between the relation of free SMCC and the "total" relation of derivations do exist: L. Mehats, S. Soloviev. Coherence in SMCCs and equivalences on deriva- tions in IMLL with unit. Annals of Pure and Applied Logic, v.147, 3, p. 127-179, august 2007. but all known intermediate relations are contained in the relation generated by commutativity of triple dual diagram. My ph.d. student Antoine El Khoury has checked also that the commutativity of triple dual diagram (equivalence of 1 and f) implies equivalence of derivations of the balanced sequents with 1, 2 or 3 variables (commutativity of corresponding diagrams in SMCC). Remark. Obviosly, the commutativity of triple dual diagram implies A*** isomorphe to A*. Best regards to all Sergei Soloviev [For admin and other information see: http://www.mta.ca/~cat-dist/ ]