CIS301 Monday, March 24  


Two rules for negation:

     ... P assume              ... ~P assume
     ... _|_                   ... _|_
~i: -------------        Pbc: ---------------
      ~P                        P


~i  says, when  P  causes a contradiction (proof crash), 
then "P is impossible".

Pbc  says, when "P is impossible" causes a contradiction,
then not only is P possible 
but "P is a certainty" --- a fact. 


EXAMPLES:

   p, ~q  |-  ~(p -> q)         (use the  ~i tactic)

1.  p               premise
2.  ~q              premise
+--------------------
|  3.  p -> q     assumption
|  4.  q          ->e 3,1
|  5.  _|_        ~e 4,2
+---------------------
6.  ~(p -> q)       ~i 3-5

"given facts  p and ~q,  it is impossible for  p->q  to be a fact"



  ~(p ^ ~q), p  |-  q         (use Pbc)  

1.  ~(p ^ ~q)        premise
2.  p                premise
+----------------------------
|  3.  ~q        assumption
|  4.  p ^ ~q    ^i 2,3
|  5.  _|_       ~e 4,1
+----------------------------
6.  q               Pbc 3-5

"given facts  ~(p ^ ~q) and p,  not only is  ~q  impossible, but  q  is a fact"