Re: Paper announcement

Hi Frogs,

Carsten Fuehrmann and David Pym made some comments about our classical 
logic paper that has recently been announced here. These comments might be 
of interest for frogs people.

Cheers,
Lutz


On Thu, 4 Nov 2004, Carsten Fuhrmann wrote:

> Dear Francois and Lutz,
> 
> Thanks for making us aware of your TLCS article; I have now read it,
> with pleasure. One difference between our works is of course that you
> add MIX explicitly, and therefore can obtain a confluent
> cut-elimination procedure. By contrast, we consider MIX to be defined
> by using Cut:
> 
>         \pi_1                                    \pi_2
>         .                                           .
>         .                                           .
>         .                                           .
> \Gamma1 |- \Delta1                        \Gamma2 |- \Delta2
> -----------------------    ------------   -----------------------
> \Gamma1 |- \Delta1,\bot    \bot |- \top   \top,\Gamma2 |- \Delta2
> ----------------------------------------------------------------- two cuts
>            \Gamma1,\Gamma2 |- \Delta1,\Delta2
> 
> (This is in tune with the work by Cockett and Seely.) Therefore, our
> cut-elimination is not allowed to stop at MIXes, and so it cannot be
> confluent. However, I consider the confluent approach to be an
> interesting alternative.  In fact, both approaches might be compatible
> to some extent if one considers MIX'es in our setting as normal forms
> - but that remains to be checked.
> 
> I like your Figure 3. In fact, I once drew almost exactly the same
> nets on a whiteboard, arriving exactly the same conclusion: Church
> numerals greater or equal to 2 are collapsed.
> 
> It is very interesting that your diagonals and codiagonals
> are natural. As for your remark
> 
> "In that model the preservation of both weakening and diagonal by
> arbitrary maps is not on the nose, but lax, and this is what prevents
> poset collapse.":
> 
> Thanks for mentioning this. In our models too, it is the naturality of
> the projections and coprojections that forces the collapse (because
> both redexes in Lafont's example become the same). The naturality of
> the (co)diagonals only rules out many models that we find interesting;
> however, we do not believe that it causes a collapse. Could you please
> make a tiny change before final submission, something like
> 
> "In that model the preservation of both weakening and diagonal by
> arbitrary maps is not on the nose, but lax; as in our models, the
> non-naturality of weakening prevents poset collapse."
> 
> As for your remark:
> 
> "this is to be compared with [FP04a,FP04b], where the enrichment is
> over posets, but is extra structure, not deducible from the
> 1-categorical structure.":
> 
> Thanks again for mentioning this. However, the enrichment turned out
> to be deducible from the 1-categorical structure, because our
> "convolution product" is a semilattice. We just didn't know that when
> we submitted our LICS paper. (The proof is contained in a long paper
> that David and I will finish soon - I'll send you a copy when it's
> finished).  Could you remove the non-deducibility claim, e.g.
> 
> "this is to be compared with [FP04a,FP04b], where the enrichment is
> over posets, but given as extra structure."?
> 
> Finally, I found your "weak units" very interesting. Maybe it is worth
> saying a little more about this in the final version?
> 
> Best wishes,
>    Carsten

 
On Thu, 4 Nov 2004, David J. Pym wrote:

> P.s. Could the points Carsten makes also be explained to
> the Frogs list please, if the paper has been advertised there?
>
> Cheers, David
>


On Tue, 2 Nov 2004, Lutz Strassburger wrote:
> 
> Hi Frogs,
> 
> since there was a recent discussion on cut elimination and proof nets for 
> classical logic, there might be some interest in the following paper that 
> we submitted to TLCA'05:
> 
> Title: Naming Proofs in Classical Propositional Logic
> 
> Authors: Francois Lamarche and Lutz Strassburger
> 
> Abstract:
>   We present a theory of proof denotations in classical propositional
>   logic. The abstract definition is in terms of a semiring of weights,
>   and two concrete instances are explored.  With the Boolean semiring
>   we get a theory of classical proof nets, with a geometric
>   correctness criterion, a sequentialization theorem, and a strongly
>   normalizing cut-elimination procedure. With the semiring of natural
>   numbers, we obtain a sound semantics for classical logic, in which
>   fewer proofs are identified. Though a ``real'' sequentialization
>   theorem is missing, these proof nets have a grip on complexity
>   issues.  In both cases the cut elimination procedure is closely
>   related to its equivalent in the calculus of structures, and we get
>   ``Boolean'' categories which are not posets.
> 
> 
> The paper is available on the web at
> http://www.ps.uni-sb.de/%7elutz/papers/namingproofsCL.pdf
> 
> Comments are welcome.
> 
> Best regards,
> Lutz
> 
>