Assignment 2: Assigned September 22
Note new deadline: due Monday, October 3 at 8:30am
Note: 2 more hints given at the end of the notes on Coq proofs (September 28)
    For questions 1, 2, and 3 give a natural deduction proof.
  1. p.79, 1.2 (2e)
  2. p.80, 1.2 (3q)
  3. p.80, 1.2 (3r)
  4. p.84, 1.4 (2h). In addition answer the question: is this formula semantically entailed from the empty set of premises? (See definition 1.34.)
  5. Do a proof in Coq of the sequent in Question 3 above (p.80, 1.2 (3r)).
  6. Do a proof in Coq of the sequent in Exercise 1.2 (3u) on p.80.

    Notes on Coq proofs:

    • You may use any Coq commands learned in class except for "auto" and "tauto". You are not restricted to using only Coq commands that correspond to natural deduction inference rules. You may also use other commands you find in the Coq documentation, but if you are not sure a command is acceptable, please ask.
    • Your solutions to questions (5) and (6) must be placed in one single file named YourLastNameFirstInitial.v. Please separate the proofs using different Coq sections. (Don't forget to begin and end all sections.) This file must be in text format (no Word documents or any other kind of document). A file saved from a CoqIDE session will work fine. The corrector must be able to save the file, load it into CoqIDE, and successfully execute every line.
    • Recall that the "Save" command in Coq does not save to a file. It saves the current completed theorem into the environment so that it can be used as a lemma in later proofs. To save your work, save it into a file.
    • If desired, you may load Examples1.v which contains the derived rule "MT" and other rules. Do "Load Examples1." before starting your proof. This file is available from the course web page.
    • You may want to use the derived rules MT, classic, and NNPP in your Coq proofs. As stated in the file CoqND.txt, use "generalize". We went over in class how to do this with MT. The other two are similar. To review this, load the file Examples1.v and execute it up until the end of the "Require Import Classical" statement. Then do:
        Check MT.
        Check classic.
        Check NNPP.
      Then continue execution up until the use of the MT rule in the last example. You will note that MT has 4 arguments, given in the order they are displayed when you do "Check MT". You will also note that NNPP takes 2 arguments and classic takes 1. You will need to figure out what arguments need to be given in the particular proof you are working on.
    • For question 6, here are hints about two possible approaches:
      • Apply \/e using the premise to break the proof into 2 cases, and in each case use the LEM rule. In one case use s\/~s and in the other use t\/~t.
      • Prove the sequent p->q |- ~p \/ q. Apply \/e using the premise to break the proof into 2 cases, and in each case use the above sequent as a derived rule.

    Notes on handing in your assignment:

    • Your Coq proofs must be handed in electronically on Blackboard Learn.
    • Solutions to questions (1), (2), (3), and (4) can be submitted either by handing in a hard copy or by submitting a second file on Blackboard Learn.