Re: Famous unsolved problems in ordinary category theory

[soloviev@irit.fr]

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 this
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 by
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 => 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") required
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/ ]