Re: New bureacracy/coherence

On Fri, 3 Jun 2005, Richard McKinley wrote:

> Hi all,
>
> I was investigating the simulation of LK cut-reduction in SKS (from a 
> semantic point of view) and I came across the following pair of proofs 
> (notation as in Lutz's recent paper on proof nets and SKS):
>
> [(A, f ) , (B,C)]
> -----------------m
> ( [A,B] , [f, C])
> ----------------- up-t
> ( [A,B] , C)
> ----------------- s , plus some \sigmas
> [ A , (B , C)]
>
>
> and
>
> [(A, f ) , (B,C)]
> ------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
> [(A, t ) , (B,C)]
> --------------------- up-f
> [ A , (B , C)]
>
> Has anyone considered this kind of thing before?  The reason behind 
> considering the two equal would be admissibilty of sequent calculus cut 
> reduction in SKS (specifically reduction of cut against contraction). 
> It also looks like the kind of coherence you might want to hold of a 
> categorical medial law.


Hi Richard,

you are quite right. From the viewpoint of coherence one might want to 
have an equality between the two. And in fact, the two are the same in our 
proof net categories (see [1] and [2]), and also in the category mentioned 
at the end of my paper [3] that you are citing above. However, what are 
the right axioms? This should be a simple and beautiful set of equations, 
and not something ugly as we have here. Since we were not able to produce 
such a set, we came up with the sledge-hammer axiom of "graphicality" in 
[2] and relegated medial to a footnote.

Right now we are working on the categorical treatment of medial. But the 
only useful thing that I can at the moment say about your example is that 
it seems not to follow from the equations that I have right now (which is 
probably not very useful...) --- maybe Francois can say more.

Regards,
Lutz


[1] F.Lamarche & L.Strassburger: "Naming Proofs in Classical Propositional 
Logic", TLCA'05

[2] F.Lamarche & L.Strassburger: "Constructing free Boolean Categories", 
LICS'05

[3] L.Strassburger: "From Deep Inference to Proof Nets", SD'05

(all available from my webpage)