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