Re: double switch

Hi Jon!

Its funny that I stumbled onto the "double switch" myself just
recently. Of course, as Robert already pointed out, it's just a
special case of switch in the presence of equations. However, once you
remove the equations that's not the case anymore. Stephane and I are
playing around with term calculi for deep inference and they are
difficult to define if we work modulo equations. So we put them as
inference rules and of course we just want to add the minimum
necessary. It turns out that the "double switch" (which I call s_, 
switch-down", because it's not self-dual) allows to discard
associativity completely. The following system is easily shown to be
complete by the standard way of showing 1) that it can transform into
conjunctive normal form and 2) that it can prove valid conjunctive
normal forms. (Unless I'm stupid.)

du_:  t / (t,t)
un_:  A / [A,f]
co_:  [A,B] / [B,A]
ai_:  t / [a,-a]
s_ :  ([A,B],[C,D]) / [[A,C],(B,D)]
c_ :  [A,A] / A
w_ :  f / A

Of course, the lack of equations makes this system cumbersome to use.
I don't even know how to embed the sequent calculus in a natural way.
But apart from that it seems that we can do some proof theory. To
reduce weakening and contraction to atomic form, we have to add
medial, f / (f,f), and a weak sort of associativity, like medial, but
the only connective appearing is disjunction. Since cut is admissible,
there also has to be some way of eliminating it syntactically.

Now, your question about the deduction theorem is not so easily
answered for (the symmetric closure of) this system. I don't see how
to prove it, but I also didn't try much.

Er, I guess I just unanswered your question, in a sense, sorry for that. 

Also: what's the value of a deduction theorem? The one-sided sequent
calculus for predicate logic seems to do pretty well without one.

Btw, I'm flattered, I didn't know you were reading my thesis. Are you
after something specific?

-Kai