Re: counterexample for reversing the 4 rules in the CoS system for K4

Hello frogs,

allow me just put Phinki's email into perspective a bit. She is talking 
about a problem in the design of deep inference systems for modal 
logics. The great thing about deep inference is that it gives us the 
same systematicity that we have in Hilbert systems and that cannot be 
achieved in the sequent calculus. For example you get a system for K4 
from a given system for K by simply turning the Hilbert axiom for 4 into 
an inference rule and adding it. However, there are of course _two_ ways 
of turning the Hilbert axiom into an inference rule, namely

        S{??R}
4-bad ----------  
        S{?R}

and 

         S{!R}
4-good  ---------
        S{!!R}

and we have to choose which one of them is the "down" rule, i.e. which 
one we put into the "cut-free" system. Clearly we would like to have 
4-good in the down system, rather than 4-bad, because then proof search 
is easier. The trouble is, and that's what Phiniki showed, that the 
system K + 4-good is not complete (while K + 4-bad is complete). Darn.

However, the counterexample disappears once we add the inference rule

    !(R,T)
x_ --------
    (!R,!T)

to the underlying inference system for K. It's sound for K, so we keep 
systematicity and it's good for proof search. Conjecture: K + x_ + 
4-good is complete.

Cheers!

-Kai