[FOM] intuitionistic logic and symmetry

[Vladimir Komendantsky]

Laurent,

> By restricting to intuitionistic logic, one loses this
> symmetry. Is there
> a symmetric way to define intuitionistic logic?

Regarding your category-theoretical posting, in categorical models of
classical logic one needs a duality principle. For the case of linear logic
(from which classical logic can also be derived) the duality principle is
given by the notion of a *-autonomous category:

A symmetric monoidal category C is *-autonomous if it has an involutary
duality (-)^d and if, for every object A, the functor (- \otimes A): C -> C
is left adjoint to (A \otimes (-)^d)^d: C -> C.

If you are looking for a categorical symmetry of this kind, my guess would be
that you will hardly find anything for intuitionism, because of the absence of
the requirement for a model of intuitionistic linear logic to be a
*-autonomous category. If you start following this path, you'll end up with
classical logic instead of intuitionistic!

Regards,
Vladimir

P.S. I would recommend you to read papers by Martin Hyland if you are
interested in categorical representation of logical symmetry.