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