double switch

Hi Frogs,

Apologies if my concerns are a little naive, I am still just learning
CoS. So, it is highly possible that I made lots of mistakes... Also,
apologies in advance for the length! My post is in regard to the switch
rule, which in Kai's thesis is

  ([R,U],T)
s ----------
  [(R,T),U]

This rule seems to me to be the heart of the classical systems, because
things like the deduction theorem follow easily with its use. I was,
however, intrigued to find the following in an old post of Allesio's to
the FOM mailing list:

Rule ^ becomes what I call a `switch':

      C{(A V D) ^ (B V E)}
    s -------------------- ,
      C{(A ^ B) V (D V E)}

(from http://www.cs.nyu.edu/pipermail/fom/2003-June/006823.html).

Assuming that there isn't just a typo on the bottom line (which seems to
be a reasonable assumption, since it is repeated for linear logic
below), I'll call this modified rule "double switch" and label it s'.  
The reason for the name is because it can be derived with two
applications of s:

  ([A,D],[B,E])
s -------------
  [(A,[B,E]),D]
s -------------
  [[(A,B),E],D]
= -------------
  [(A,B),[D,E]]

Of course, Allesio could have just meant precisely that the R^ rule
coincides, essentially, with applying s a couple of times. I'll run with
my first reading for a little while longer though.

Now, if we take Kai's system SKSg and replace s with s' (call this
system SKSg'), then it seems that we cannot derive s. Let us try:

      ([R,U],T)
=   -------------
    ([R,U],[T,f])
w   --------------
    ([R,U],[T,T])
s'  --------------
    [(R,T),[U,T]]

What we would like to do at this point is to use something like
co-weakening  to get rid of the T in [U,T]. This won't work, because
doing so would destroy everything else (we get [U,t], which then makes
the whole structure implode to t...).

This then makes the deduction theorem fail (I think) in SKSg' for
similar reasons, since we end up with (when trying to move from proofs
of [~T,R] to derivations from T to R):

      (T,[~T,R])
=   --------------
    ([T,f],[~T,R])
w   --------------
    ([T,T],[~T,R])
s'  --------------
    [(T,~T),[T,R]]
=   --------------
        [T,R]

We cannot get rid of T using co-weakening for the same reason as above.
Another downer is that s' is no-longer self symmetric, since its De
Morgan dual is:

([A,B],(D,E))
-------------
[(A,D),(B,E)]

I suspect that these concerns were what led to preferring s over s' in
the first place...

Jon

-- 
http://rsise.anu.edu.au/~jon