80-211                                                                                                             Spring 2003



Derived sequents/theorems.


Below is a list of some frequently used derived sequents/theorems you can use in your proofs (and of course you can use any substitution instance of them).


Name                                                  Sequent/theorem                    Location


The excluded middle:                            P v ~P                                      44 in the book


Negated antecedent                              ~P ├ P → Q                            51 in the book


Affirmed consequence              Q ├ P→Q                               50 in the book


De Morgan #1                                      ~(P v Q)  ┤├  ~P & ~Q          Problem (f) on p.41


De Morgan #2                                      ~(P & Q)  ┤├  ~P v ~Q          Problem (g) on p. 41


Negated-Arrow                                    ~(P→ ~Q) ┤├ P & Q             Problem (e) on p. 41


Wedge-Arrow:                         ~P v Q ┤├ P → Q                  49 in the book


Modus Tollendo Ponens (MTP)            ~P, P v Q ├ Q                         52 in the book