Subject: categories: Proof nets

From: Robin Houston <[email-masked]>
Date: Mon, 19 Jul 2004 13:05:33 +0100

Dear categorists,

The category of ordinary MLL proof nets (where an object is a term,
and a morphism X -> Y is a cut-free proof net for |- X^, Y) is the
free unitless *-autonomous category generated by the literals.

Does the corresponding result hold for MALL? The Hughes-van Glabeek
notion of MALL proof net has the ring of truth about it, and indeed
they claim to have proven (theorem 4.22) that "two cut-free MALL
proofs translate to the same proof net iff they can be converted into
each other by a series of rule commutations". Of course the category
of MALL proof nets is a unitless *-autonomous category with binary
products and coproducts, but nowhere (to my knowledge) is it described
as the *free* such category.

Is that because it isn't, or merely because it isn't (yet) known to be?
Enlightenment will be much appreciated.

Yours,
Robin