Re:New bureacracy/coherence

At 2:22 PM +0100 3.6.05, Richard McKinley wrote:
> 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,

there might be reasons to consider these phenomena a bit disturbing, I think.

I would like to clarify, mainly to myself, the situation. Let's start 
from a possible viewpoint:

1) Optional. Anyway, let's agree that the formalism should allow for 
as many different derivations as it is conceivable. This could mean, 
at an extreme, to consider deductive systems, in that formalism, 
where every sound inference is possible. (Of course this is not very 
meaningful if one wants to do some non-trivial proof theory on such a 
deductive system.) Formalism B and wired deduction are very liberal 
at this, I cannot imagine anything more liberal. In any case CoS is 
already liberal enough, while anything else is clearly not (short of 
`simulating' CoS in the sequent calculus by heavy use of the cut 
rule, and things like that).

2) However, let's say that the interesting deductive systems are 
those which don't allow for `too many' derivations. For example, one 
might criticise SKS for allowing the two derivations shown by Richard 
and there might be interest in restricting the possible derivations, 
by designing a more restrictive deductive system. Maybe this can 
generate interesting research, if the quest can be made technical in 
some sense.

So the question: which criteria to use in order to discriminate what 
is allowed and what is not?

`Simple' coherence laws might be such a criterion, however it looks 
to me a possibly too debatable criterion (many papers, little 
agreement, etc.).

The main reason for which I find Richard's example disturbing is that 
the derivation with medial has a double inversion between `and' and 
`or' (in the relation between A and C) that the other derivation has 
not. Not that I know much, but everything I know about geometric 
models tells me: DIFFERENT!

This, unless somebody comes up with a model where this double 
inversion makes sense, which is not impossible given that in the end 
the logical relation (between A and C) is conserved. We can imagine 
some sort of node that is tied and untied; however: what to make of 
the switch?

I have no answers, maybe some of you has some idea?

I only have a mild opinion, possibly due to ignorance. I think that 
it is more challenging to find geometric models rather than 
categorical axiomatisations. If this is true, then the final choice 
should be made based on the geometric model, not on the categorical 
one.

I believe that in the system of wired deduction that I showed you a 
few weeks ago, the problem doesn't show up because the second 
derivation that Richard shows is impossible. The system is

       (t  t)         [a a]         (f t)
   wi_ -|--|- ,   wc_ -|-|- ,   ww_ -|-|- ,
       [a -a]         [a f]         [a f]

       (a -a)         (a t)         (a t)
   wi^ -|--|- ,   wc^ -|-|- ,   ww^ -|-|- ,
       [f  f]         (a a)         [t f]

      (A [B  C])       [(A B) (C D)]
   s  =|==|==|=  ,   m  =|===X===|=  .
     [(A  B) C]        ([A C] [B D])

I think that the problem is the up-f rule, it should be impossible to 
perform it in the system above. Can anybody confirm this? (I might be 
very wrong...)

Can anybody find an example of two different derivations in my 
system, that `should be equal', and where there is a double inversion 
of `and' and `or', like in Richard's example?

Ciao,

-Alessio