Dear list members, I am currently working in categorical logic with something that might be called a "compact closed deductive system", that is, a deductive system (in the sense of Lambek) defined as a compact closed category (i.e., a *-autonomous category where the tensor unit is a dualizing object). I have two questions. First, it appeared to me that we can show in a compact closed deductive system that every arrow is an isomorphism. Hence, if there is a deduction arrow from A to B, then A is isomorphic (logically equivalent) to B. Is this result accurate? Does this generalize to any compact closed category? Secondly, I wonder what happens if we add an arbitrary arrow A --> B to the category. Put differently, what happens if we add A --> B as an axiom to a compact closed deductive system? Does this also yield an isomorphism between A and B (assuming that the first result is adequate)? Or is it possible to add some axioms that are not necessarily isomorphisms? I hope my question is clear, and if not I would be happy to clarify myself, so do not hesitate to contact me. Any lead will be appreciated. Thanks in advance for those who will respond. Yours, Clayton Peterson Ph. D. candidate Université de Montréal clayton.peterson@umontreal.ca [For admin and other information see: http://www.mta.ca/~cat-dist/ ]