Re: double switch

> How do you get it into negated normal form first, given the absense of
> the negation equalities (or do you assume that the formula is given in
> nnf)?

Yes, that's my assumption.

 
> > I don't even know how to embed the sequent calculus in a natural way.
> 
> I don't see where the proof of your Theorem 2.3.3 breaks down for this
> system?

I use associativity for every single rule since the comma in a sequent
is associative. Maybe it's easily adapted though, I haven't tried.


> (By symmetry we get A/(A,t) also). One can then use, essentially, what
> Robert pointed out to derive switch also. The deduction theorem then
> goes through in the normal way.

Ah, right. Strange though, to use a contraction just to introduce a unit.


> I guess the equalities missing are the negation rules and context
> closure?

There are no equations at all. Oh, and the connectives are binary.

Best,

-Kai