Homework 7 handout distributed; due on March 6.
We're going to talk about some simple logical principles from section 4.3 before continuing with the extended additivity example. Please see under Homework 7 above for the forms of the sentences to be formally proved as indicated on the first page of the handout. I adopt the convention henceforth that ``A'' and ``E'' should not appear as predicates, in order to avoid confusion with the quantifiers Ax and Ex in their ``typewriter'' forms. Here are the things we proved in class: Goal: ~(Ex.Px)<->(Ax.~Px) unpack into two subgoals (implications): Goal: ~(Ex.Px)->(Ax.~Px) open a box for imp intro: | 1. ~(Ex.Px) subpremise | Goal: (Ax.~Px) open a box for univ intro: | | 2. a=a arbitrary object intro | | Goal: ~Pa open a box for neg. intro: | | | 3. Pa subpremise | | | Goal: contradiction | | | 4. (Ex.Px) exist. intro. line 3 | | | 5. (Ex.Px) & ~(Ex.Px) c.i. lines 1,4 | | 6. ~Pa neg. intro. lines 3-5 | 7. (Ax.~Px) univ. intro. lines 2-6 8. ~(Ex.Px)->(Ax.~Px) imp. intro. lines 1-7 We return to the second subgoal of our proof of a biconditional. Goal: (Ax.~Px)->~(Ex.Px) Open a box for imp. intro. | 9. (Ax.~Px) subpremise | Goal: ~(Ex.Px) open a box for neg intro | | 10. (Ex.Px) subpremise introduce a witness | | | 11. Pb witness intro line 10 | | | 12. ~Pb univ elim line 9 Mr. Egbert originally wrote Pb & ~Pb here, then looked at it and realized that he couldn't finish the neg intro at this point because he was one box too deep... | | | 13. A & ~A neg. elim. lines 11,12 | | 14. A & ~A exist. elim. lines 11-13 The funny looking contradiction proved is because we couldn't get out of the ``witness box'' with the obvious Pb & ~Pb. I omitted the line with Pb & ~Pb found in the original board proof because neg. elim. also works with two previous lines as shown. It is worth noting that a proof by exist.elim. always ends by copying the last line inside the box to the outside -- that last line cannot mention the witness declared in the box. | 15. ~(Ex.Px) neg. intro. lines 10-14 16. (Ax.~Px)->~(Ex.Px) imp. intro. lines 9-15 17. ~(Ex.Px)<->(Ax.~Px) biconditional intro lines 8,16 Here is the proof as a finished product without my remarks between the lines. Goal: ~(Ex.Px)<->(Ax.~Px) Goal: ~(Ex.Px)->(Ax.~Px) | 1. ~(Ex.Px) subpremise | Goal: (Ax.~Px) | | 2. a=a arbitrary object intro | | Goal: ~Pa | | | 3. Pa subpremise | | | Goal: contradiction | | | 4. (Ex.Px) exist. intro. line 3 | | | 5. (Ex.Px) & ~(Ex.Px) c.i. lines 1,4 | | 6. ~Pa neg. intro. lines 3-5 | 7. (Ax.~Px) univ. intro. lines 2-6 8. ~(Ex.Px)->(Ax.~Px) imp. intro. lines 1-7 Goal: (Ax.~Px)->~(Ex.Px) | 9. (Ax.~Px) subpremise | Goal: ~(Ex.Px) | | 10. (Ex.Px) subpremise | | | 11. Pb witness intro line 10 | | | 12. ~Pb univ elim line 9 | | | 13. A & ~A neg. elim. lines 11,12 | | 14. A & ~A exist. elim. lines 11-13 | 15. ~(Ex.Px) neg. intro. lines 10-14 16. (Ax.~Px)->~(Ex.Px) imp. intro. lines 9-15 17. ~(Ex.Px)<->(Ax.~Px) biconditional intro lines 8,16 Here's the second statement we proved in class: Goal: (Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx) open a box for imp. intro: | 1. (Ax.Px & Qx) subpremise Goal: (Ax.Px) & (Ax.Qx) This breaks into two subgoals: Goal: (Ax.Px) Open a box for univ. intro: | | 2. a = a arbitrary object intro | | Goal: Pa | | 3. Pa & Qa univ. elim. line 1 | | 4. Pa c.e. line 3 | 5. (Ax.Px) univ. intro. 2-4 Now someone observed that the rest of the proof would look essentially the same; one could use one's editor to copy it and make a few changes to prove (Ax.Qx), like this: Goal: (Ax.Qx) | | B2. a = a arbitrary object intro | | Goal: Pa | | B3. Pa & Qa univ. elim. line 1 | | B4. Qa c.e. line 3 | B5. (Ax.Qx) univ. intro. 2-4 Notice that all I had to do was tag the line numbers and change the conjunct in line B4 to Qa and the conclusion. The proof would be completed with | 6. (Ax.Px)& (Ax.Qx) c.i. 5,B5 7.(Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx) imp. intro lines 1-6. One can do this even more economically by reusing the same box for the two univ. intro. subproofs, as follows: Goal: (Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx) | 1. (Ax.Px & Qx) subpremise Goal: (Ax.Px) & (Ax.Qx) Goal: (Ax.Px) | | 2. a = a arbitrary object intro | | Goal: Pa | | 3. Pa & Qa univ. elim. line 1 | | 4. Pa c.e. line 3 | | 5. Qa | 6. (Ax.Px) univ. intro. 2-4 Goal: (Ax.Qx) | 7. (Ax.Qx) univ. intro. 2-5 (reusing the box) | 8. (Ax.Px)& (Ax.Qx) c.i. 6,7 9.(Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx) imp. intro lines 1-8. If this makes you queasy, don't do it in your proofs! But I know that some of you can carry this off correctly.