CPMA 511: Logic and Proof

Homework Assignment #2

1. Finish the proof of the completeness theorem, i.e., show that the lemma is true when the formula is a disjunction or a negation.

2. An alternative, but closely related, system of deduction is the sequent calculus. A sequent is of the form "Gamma |- phi" where Gamma is a set of formulas and phi is a single formula. Each proof rule derives a new sequent from a set of other sequents. Explicitly listing the premises of a formula (the set Gamma) means that we don't need the box notation of the book. It is fairly straightforward to convert the rules of natural deduction from the book to those of the sequent calculus. For example the ^i rule in sequent calculus is:

          Gamma |- phi
          Gamma |- psi
          ------------------
          Gamma |- phi ^ psi
   

   which means that if we can derive phi from a set of formulas (Gamma), and we can derive psi from the same set, then we can derive phi ^ psi from that set.

   Rules which use boxes translate to rules that change the set of premises, Gamma. For example, ->i becomes:

         Gamma, phi |- psi
         -------------------
         Gamma |- phi -> psi
   

   So, if psi is derivable from Gamma plus phi, then we can derive the implication phi -> psi from Gamma alone.

   The sequent calculus requires an assumption axiom:

         ------------------------------------------
         Gamma |- phi (if phi is a member of Gamma)
   

   The assumption axiom corresponds to the notion that the premises of a theorem are provable.

   Express the other ten rules of the book's system of natural deduction in the sequent calculus and use the resulting rules to prove the theorem p->q |- ~p v q in the sequent calculus.

3. Complete steps 2 and 3 of the proof in the note below.

4. A simple algorithm for making correct change using the fewest number of coins is to always use the biggest coin possible first, and then repeat the process for the remainder of the money owed. For example, to make change for $.42, the largest coin would be a quarter, leaving $.17, the next coin would have to be a dime, leaving $.07, then a nickel, and finally two pennies, for a total of five coins (the minimum number). Prove using mathematical induction that this algorithm will always work, i.e., result in the minimum number of coins.

5. Suppose that we remove the ~~e elimination rule from the set of twelve rules of natural deduction. Is the resulting system complete (here the system does /not/ include the four derived rules, just the remaining eleven rules)? Prove your answer.

First a note about top (-\). The book doesn't actually consider top or bottom to be propositional constants (although it should) and there are no proof rules that deal with top. We should consider -\ to be shorthand notation for ~\_ (not bottom). For example, using the proof rules, we can derive |- -\_.

+-------------------+
| 1. \_      Assume |
+-------------------+
  2. ~\_     ~i 1

I thought it would be useful to show how we derive a short proof using the technique of the completeness theorem to solidify how that proof works. Consider the theorem |- (p -> q) -> (~p v q).

1. Replacing p by top (~\_) yields (~\_ -> q) -> (~~\_ v q).
   1. Replacing q by top yields (~\_ -> ~\_) -> (~~\_ v ~\_).

      The lemma says that we can construct a proof of this by combining the proofs of the sub-formulas (which are found recursively). So, to prove |- (~\_ -> ~\_) -> (~~\_ v ~\_), we first (recursively) prove |- (~\_ -> ~\_) and |- (~~\_ v ~\_). To prove |- (~\_ -> ~\_) we use the proof of |- ~\_ (twice) and the rules about implication. So, we get

        +----------------------+
        | 1. ~\_      Assume   |
        |   +----------------+ |
        | 2.| \_      Assume | |
        |   +----------------+ |
        | 3. ~\_     ~i 2      |
        +----------------------+
          4. ~\_ -> ~\_ ->i 1-3
      

      And the proof of ~~\_ v ~\_ is simply

          +----------------+ 
        1.| \_      Assume | 
          +----------------+ 
        2. ~\_     ~i 1     
      
        3. ~~\_ v ~\_  vi2 2
      

      We don't actually need the proof of the hypothesis to prove (~\_ -> ~\_) -> (~~\_ v ~\_), but just the proof of the conclusion, so the whole proof is:

        +-------------------------+
        | 1.  (~\_ -> ~\_) Assume |
        |   +----------------+    |
        | 2.| \_      Assume |    |
        |   +----------------+    |
        | 3. ~\_     ~i 2         |
        |                         |
        | 4. ~~\_ v ~\_  vi2 3    |
        +-------------------------+
          5. (~\_ -> ~\_) -> (~~\_ v ~\_) ->i 1-4.
      

      Next we substitute q back for the occurrences of ~\_ which correspond to q, add the initial assumption q, and replace the proof of ~\_ (lines 2 and 3 above) by a copy of that initial assumption (line 3 below):

          1. q           Assume
        +-------------------------+
        | 2.  (~\_ -> q) Assume   |
        |                         |
        | 3.  q          Copy 1   |
        |                         |
        | 4. ~~\_ v q    vi2 3    |
        +-------------------------+
          5. (~\_ -> q) -> (~~\_ v q) -> 2-4
      

   2. Replacing q by bottom yields (~\_ -> \_) -> (~~\_ v \_). Here, the hypothesis is false, so the lemma says that we can prove its negation, i.e.:

       +-------------------------+
       | 1. ~\_ -> \_   Assume   |
       |   +-------------------+ | 
       | 2.| \_         Assume | |
       |   +-------------------+ | 
       | 3. ~\_         ~i 2     | 
       |                         |
       | 4. \_          ->e 3, 1 |
       +-------------------------+
         5. ~(~\_ -> \_) RAA 1-4
      

      We can skip the proof of the negation of the conclusion since we won't use it. The proof of the implication is then:

       +-----------------------------+
       |   1. ~\_ -> \_   Assume     |
       | +-------------------------+ |
       | | 2. ~\_ -> \_   Assume   | |
       | |   +-------------------+ | |
       | | 3.| \_         Assume | | |
       | |   +-------------------+ | |
       | | 4. ~\_         ~i 3     | |
       | |                         | |
       | | 5. \_          ->e 4,2  | |
       | +-------------------------+ |
       |   6. ~(~\_ -> \_) RAA 2-5   |
       |   7. \_           ~e 1,6    |
       |   8. ~~\_ v \_    \_e 7     |
       +-----------------------------+
           9. (~\_ -> \_) -> (~~\_ v \_) ->i 1-8
      

      We substitute q for those occurrences of \_ which stem from q, and add the initial assumption ~q. However, whenever we derived \_ in the proof above (line 5 above), we will now derive q (line 6 below), so we must use ~e (with the assumption ~q) to derive \_ again (line 7 below). The resulting proof is:

           1. ~q          Assume
       +-----------------------------+
       |   2. ~\_ -> q    Assume     |
       | +-------------------------+ |
       | | 3. ~\_ -> q    Assume   | |
       | |   +-------------------+ | |
       | | 4.| \_         Assume | | |
       | |   +-------------------+ | |
       | | 5. ~\_         ~i 4     | |
       | |                         | |
       | | 6. q           ->e 5,3  | |
       | | 7. \_          ~e 6,1   | |
       | +-------------------------+ |
       |   8. ~(~\_ -> q) RAA 3-7    |
       |   9. \_           ~e 2,8    |
       |  10. ~~\_ v q    \_e 9      |
       +-----------------------------+
          11. (~\_ -> q) -> (~~\_ v q) ->i 2-10
      

   3. We use LEM (q v ~q) together with the two proofs above to get:

          1. q v ~q      LEM
      +-----------------------------------------+
      |   2. q           Assume                 |
      | +-------------------------+             |
      | | 3.  (~\_ -> q) Assume   |             |
      | |                         |             |
      | | 4.  q          Copy 2   |             |
      | |                         |             |
      | | 5. ~~\_ v q    vi2 4    |             |
      | +-------------------------+             |
      |   6. (~\_ -> q) -> (~~\_ v q) -> 3-5    |
      +-----------------------------------------+
      +-----------------------------------------+
      |   7. ~q            Assume               |
      | +-----------------------------+         |
      | |   8. ~\_ -> q    Assume     |         |
      | | +-------------------------+ |         |
      | | | 9. ~\_ -> q    Assume   | |         |
      | | |   +-------------------+ | |         |
      | | |10.| \_         Assume | | |         |
      | | |   +-------------------+ | |         |
      | | |11. ~\_         ~i 10    | |         |
      | | |                         | |         |
      | | |12. q           ->e 11,9 | |         |
      | | |13. \_          ~e 12,7  | |         |
      | | +-------------------------+ |         |
      | |  14. ~(~\_ -> q) RAA 9-13   |         |
      | |  15. \_           ~e 8,14   |         |
      | |  16. ~~\_ v q    \_e 15     |         |
      | +-----------------------------+         |
      |    17. (~\_ -> q) -> (~~\_ v q) ->i 8-16|
      +-----------------------------------------+
         18. (~\_ -> q) -> (~~\_ v q)  ve 1, 2-6, 7-17
      

      This concludes the proof of the formula when top is substituted for p.

2. We replace p by \_ and construct a proof using the same techniques as in 1.

3. We use LEM (p v ~p), along with the proofs of steps 1 and 2 to prove the original theorem.