Propositions and Proofs

Selected scripts from the third chapter of the book

Exercises

  1. Exercises 3.2 page 58 and 3.3 page 65
  2. Exercise 3.4 page 67
  3. Exercise 3.5 page 69

Errata

  1. Page 21, in the Var rule, read (x:A) instead of
  2. Page 52, same correction.
  3. Page 47, Definition 8, "A goal is the pairing ... and a type P that is well-formed ..."
    "a proof of P that should be a well-formed term t of type P in the environment ..."
  4. Page 63 (last paragraph): read "Calling "apply H0" generates three subgoals: P->Q->R, R and T->Q" Please replace intro H2 with intro H1 and H1 with H0, to be OK with the proof script.
  5. Page 70 (last paragraph): read "forall P Q R: Prop"