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

Hi everybody,

here is a formula discovered by Robert which shows that the 4 rules (4^ and
4_) cannot be interchanged without affecting the completeness of the
systems. In particular, the system that extends KSm with the 4 down rule: 

     S{??R}
4_ ----------  is complete for K4, 
     S{?R}
                                                        S{!R}
whereas the same system but with the 4 down rule: 4'_  --------- is not
complete.
                                                        S{!!R}

(Notation: "!" stands for a box and "?" for a diamond. 4^ and 4_ are the 4
up and down rules respectively) 
   
The counterexample is formula [ ? -P, ? -Q, !(!P, !Q ) ], which is a theorem
of K4 but not provable in the second system. So, although we would like to
get rid of the current 4_ rule because of its inappropriateness for proof
search, we cannot do so by replacing it with the rule 4'_. A sketch of the
proof follows.


Bye,
Phiniki


-------------------------------

1. The system for K4 that extends KS with the rules

     S{![R,T]}         S{!R}
k_  -----------  , 4_ --------  and the equalities {t = !t, f = ?f}
     S[!R,?T]          S{!!R}

is not complete. T1: [ ? -P, ? -Q, !(!P, !Q ) ] is a theorem of K4 but it is
not provable in the system. 

Argument. Any proof of T1 must include applications of the 4_ rule, since T1
is not a theorem of K and the system obtained as the above but without the
4_ rule is complete for logic K. However, when applying bottom-up, we
observe that applications of the 4_ rule to T1 do not result a new formula
(modulo the equalities). That is, the 4_ rule is applicable in T1 only on
!!t and equivalents. Moreover, none of the other rules can create a new box
or pull boxes out of a conjunction, so that the 4_ rule cannot be applied on
any derivations which conclude T1 and so,no such derivation can be extended
to a proof.


2. T1 is a theorem of the system for K4 that extends KS with the rules

     S{![R,T]}         S{??R}
k_  ----------- , 4_ -------  and the equalities {t = !t, f = ?f}.
     S[!R,?T]          S{?R}


Proof. T1 is provable as follows:

                 t
  i_  ----------------------------
       ![ ? -P,   ? -Q,  (!P, !Q) ]
  k_  ----------------------------
       [ ?? -P, ![? -Q,  (!P, !Q) ]]
  k_  ----------------------------
       [ ?? -P,  ?? -Q, !(!P, !Q) ]
  4_  ----------------------------
       [ ?? -P,   ? -Q, !(!P, !Q) ]
  4_  ----------------------------
       [  ? -P,   ? -Q, !(!P, !Q) ]


-- 
Psssst! Mit GMX Handyrechnung senken: http://www.gmx.net/de/go/mail
100 FreeSMS/Monat (GMX TopMail), 50 (GMX ProMail), 10 (GMX FreeMail)