Re: double switch

Hi Kai,

Thanks for the reply. 

> 1) that it can transform into conjunctive normal form 

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)?

> 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?

> 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.

Unless I'm missing something, this seems to work. First, [A,f]/A is
derivable:

    [A,f]
w_  -----
    [A,A]
c_  -----
      A  

(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. 

I guess the equalities missing are the negation rules and context
closure? 
      
> Also: what's the value of a deduction theorem? The one-sided sequent
> calculus for predicate logic seems to do pretty well without one.

I take its value a bit philosophically: It shows that whatever notion of
implication we are using matches up with the notion of derivability that
we are using. This is nice, because one usually performs deductions when
performing proofs of implications in practice. I guess the other option
is to use a different sort of implication.. The one sided calculus goes
around this issue by "hiding" implication. 

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

Your thesis was passed onto me by an ANU proof theorist with a penchant
for display logic...I suppose that I am after an introduction to CoS.
Between your thesis and Alessio's "System of interaction and structure"
(which I am yet to read), I guess that I will get that.

Jon

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