On Fri, 24 Jun 2005, Alwen Tiu wrote:
Hi Jon,
In Christian Retore's paper on Pomset Logic, he shows (via coherence
semantics) that there is only one self-dual noncommutative binary
operator which can be added to MLL. Since BV gives such an operator,
can't one just conclude that it captures the Pomset operator? That is,
do we *really* need to consider the proof nets for Pomset (of which
there are two flavours - the one in Retore's original paper, and the one
based on "directed cographs").
The problem is that of completeness, that is, whether BV captures all
provable pomset-logic formulas. Lutz has shown in his thesis that BV is
sound with respect to Pomset logic.
Actually there is a different proof than mine already in one of
Christian's papers on pomset logic. He also could show only soundness, but
not completeness.
There's just a little "gap" in the
completeness proof (Lutz can tell you more about it) that we are unable
to bridge for four years now! I'll be interested if you have any thought
about it.
The weird thing is that for the par-tensor fragment the situation is clear
because we are in the unit-free MLL case for which we know that proof nets
are complete, and in the par-seq (or par-before) fragment the situation is
clear because the rules are complete for the inclusion of series-parallel
orders (see the RTA97 paper by Denis Bechet, Philippe de Groote and
Christian Retore). By duality also the tensor-seq fragment is clear. Only
when all three connectives are together, it becomes mind-boggling...
Ciao,
Lutz
