Re: Pomset vs BV

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