Q350: Inference Rules and Proofs - Handout 1

Negation Elimination (¬ Elim.)
|
|¬¬P
|.
>|P
|

Conjunction Introduction (^ Intro.)
|
|P1
|||
\/
|Pi
|||
\/
|Pn
|.
|.
|.
>|P1 ^ ... ^ Pi ^ ... ^ Pn
|

Conjunction Elimination (^ Elim.)
|
|P1 ^ ... ^ Pi ^ ... ^ Pn
|.
|.
|.
>|Pi
|

Disjunction Introduction (v Intro.)
|
|Pi
|.
|.
|.
>|P1 v ... v Pi v ... v Pn
|

Conditional Elimination (→ Elim.)
|
|P → Q
|.
|.
|.
|P
|.
|.
|.
>|Q
|

Biconditional Elimination (↔ Elim.)
|
|P ↔ Q (or Q ↔ P)
|.
|.
|.
|P
|.
|.
|.
>|Q
|

Proofs:

  1. Given:Cube(a) ^ Cube(b)
    Prove:Cube(a) v Cube(c)

     
     
  2. Given:Cube(a) ^ Cube(b)
    Prove:(Cube(a) v Cube(c)) ^ Cube(b)

     
     
  3. Given:Cube(a) → Cube(b)
    Cube(a) ^ Cube(c)
    Prove:Cube(c) ^ Cube(b)

     
     
  4. Given:Cube(a) <→ Cube(b)
    Cube(b)
    Cube(b) → Cube(c)
    Prove:Cube(a) ^ Cube(c)

     
     
  5. Given:(P v Q) ^ R
    R → S
    S → T
    Prove:T ^ (P v Q)

     
     
  6. Given:P ^ Q ^ R
    (Q v S) → T
    T → U
    Prove:U v V

     
     
  7. Given:P
    P ↔ (Q v R)
    (Q v R) → S
    S → T
    Prove:P ^ S ^ T

     
     
  8. Given:P → W
    (Q v R) ↔ (S ^ T)
    Q
    S → V
    V → P
    Prove:W