A correct proof does not need to look exactly like the proofs given here. I would appreciate hearing about any mental lapses evident in these proofs, or for that matter anything you don't understand about what I did or why I did it. Theorem H7.1: (Ex.~Px) <-> ~(Ax.Px) Goal 1: (Ex.~Px) -> ~(Ax.Px) | 1. (Ex.~Px) subpremise for imp. intro | Goal: ~(Ax.Px) | | 2. (Ax.Px) subpremise for neg. intro. | | | 3. ~Pa witness intro line 1 | | | 4. Pa univ elim line 2 | | | 5. Z & ~Z neg. elim. lines 3,4 | | 6. Z & ~Z exist. elim. lines 3-5 | 7. ~(Ax.Px) neg. elim. lines 2-6 8. Goal 1 imp. intro. lines 1-7 Goal 2: ~(Ax.Px) -> (Ex.~Px) | 9. ~(Ax.Px) subpremise for imp. intro. | Goal: (Ex.~Px) To prove this directly, we would need some specific object B (not a lucky charm!) for which we could show PB. There isn't any way to get a specific object to talk about from our premises-- a negative premise is totally unhelpful unless one has a disjunction around! All of this suggests a proof by contradiction: | Goal: ~~(Ex.~Px) | | 10. ~(Ex.~Px) subpremise for neg. intro. | | Goal: contradiction | | Goal: (Ax.Px) for a contradiction with line 9 | | | 11. a=a arbitrary object intro | | | Goal: Pa | | | Goal: ~~Pa (once again, there's nothing to help us in the | | | premises, so we try proof by contradiction) | | | | 12. ~Pa subpremise for neg. intro. | | | | 13. (Ex.~Px) exist intro line 12 | | | | 14. (Ex.~Px) & ~(Ex.~Px) c.i. lines 10, 13 | | | 15. ~~Pa neg intro lines 12-14 | | | 16. Pa d.n.e. line 15 | | 17. (Ax.Px) univ. intro. lines 11-16 | | 18. (Ax.Px) & ~(Ax.Px) c.i. lines 9,17 | 19. ~~(Ex. ~Px) neg. intro. lines 10-18 | 20. (Ex. ~Px) d.n.e. line 19 21. Goal 2 imp. intro. lines 9-20 22. Theorem H7.1 biconditional intro, lines 8,21. Theorem H7.2: (Ex.(Px | Qx)) <-> ((Ex.Px) | (Ex.Qx)) Goal 1: (Ex.(Px | Qx)) -> ((Ex.Px) | (Ex.Qx)) | 1. (Ex.(Px | Qx)) subpremise for imp. intro. | Goal: ((Ex.Px) | (Ex.Qx)) | | 2. ~(Ex.Px) subpremise for disj. intro. | | Goal: (Ex.Qx) | | | 3. Pa | Qa witness intro line 1 | | | Goal: Qa (which will allow us to prove (Ex.Qx) by exist intro) | | | Goal: ~Pa (which will allow us to prove Qa by disj. elim.) | | | | 4. Pa subpremise for neg. intro. | | | | 5. (Ex.Px) exist intro line 4 | | | | 6. (Ex.Px) & ~(Ex.Px) c.i. lines 2,5 | | | 7. ~Pa neg. intro. lines 4-6 | | | 8. Qa disj. elim. lines 3,7 | | | 9. (Ex.Qx) exist. intro. line 8 | | 10. (Ex.Qx) exist. elim. lines 3-9 | 11. ((Ex.Px) | (Ex.Qx)) disj. intro. lines 2-10 12. Goal 1 imp. intro. lines 1-11 Goal 2: ((Ex.Px) | (Ex.Qx)) -> (Ex.(Px | Qx)) | 13. ((Ex.Px) | (Ex.Qx)) subpremise for imp. intro. | Goal: (Ex.(Px | Qx)) The disjunctive premise 13 suggests a proof by cases: | | 14. (Ex.Px) subpremise for proof by cases (case 1) | | | 15. Pa witness intro line 14 | | | 16. Pa | Qa disj intro (special) line 15 | | | 17. (Ex.(Px | Qx) exist. intro. line 16 | | 18. (Ex.(Px | Qx) exist. elim. lines 15-17 | (note that this is the end of the first box in the proof by cases-- | don't run these boxes together) | | 19. (Ex.Qx) subpremise for proof by cases (case 1) | | | 20. Qa witness intro line 19 | | | 21. Pa | Qa disj intro (special) line 20 | | | 22. (Ex.(Px | Qx) exist. intro. line 21 | | 23. (Ex.(Px | Qx) exist. elim. lines 20-22 | 24. (Ex.(Px | Qx) proof by cases, lines 13, 14-18, 19-23 25. Goal 2 imp. intro. lines 13-24 26. Theorem H7.2 biconditional intro lines 12, 25. One could also use proof by cases in the proof of Goal 1, but the advantage is not clear, since one of the cases (if we work by cases from the disjunctive premise, which is line 3) is contradictory. Theorem H7.3: (Ax.(Px | S)) <-> ((Ax.Ps) | S) (where x does not occur free in S!) Goal 1: (Ax.(Px | S)) -> ((Ax.Ps) | S) | 1. (Ax.(Px | S)) subpremise for imp. intro. | Goal: (Ax.Px) | S This is a disjunction, not a universal statement, so the next line should NOT be arbitrary intro! | | 2. ~S subpremise for disj. intro. | | Goal: (Ax.Px) NOW we have a universal goal! | | | 3. a=a arbitrary object intro | | | Goal: Pa | | | 4. Pa | S univ elim, line 1 | | | 5. Pa disj. elim. lines 2,4 | | 6. (Ax.Px) univ. intro. lines 3-5 | 7. (Ax.Px) | S disj. intro. lines 2-6 8. Goal 1 imp. intro. lines 1-7 Goal 2: ((Ax.Px) | S) -> (Ax.(Px | S)) | 9. ((Ax.Ps) | S) subpremise for imp. intro. | Goal: (Ax.(Px | S)) This IS a universal statement, so arbitrary object intro follows. | | 10. a=a arbitrary object intro | | Goal: Pa | S The disjunctive premise 9 suggests proof by cases | | | 11. (Ax.Px) subpremise for proof by cases (case 1) | | | 12. Pa univ. elim. line 11 | | | 13. Pa | S disj. elim (special) line 12 | | | | | 14. S subpremise for proof by cases (case 2) | | | 15. Pa | S disj elim (special) line 14 | | 16. Pa | S proof by cases 9, 11-13, 14-15 Notice that as in all proofs by cases 11-13 and 14-15 are separate boxes. | 17. (Ax.Pa|S) univ. elim. lines 10-16 18. Goal 2 imp. intro. lines 9-17 19. Theorem H7.3 biconditional intro, lines 8,18. Theorem H7.4: (Ax.(Px -> Qx)) -> ((Ex.Px) -> (Ex.Qx)) | 1. (Ax.(Px -> Qx)) subpremise for imp. intro. | Goal: ((Ex.Px) -> (Ex.Qx)) | | 2. (Ex.Px) subpremise for imp. intro. | | | 3. Pa witness intro line 3 | | | 4. Pa -> Qa univ. elim. line 1 | | | 5. Qa mp lines 3,4 | | | 6. (Ex.Qx) exist intro line 5 | | 7. (Ex.Qx) exist elim lines 3-6 | 8. ((Ex.Px) -> (Ex.Qx)) imp. intro. lines 2-7 9. Theorem H7.4 imp. intro. lines 1-8 Theorem H7.5: (Ey.(Ax.Rxy)) -> (Ax.(Ey.Rxy)) | 1. (Ey.(Ax.Rxy)) | Goal: (Ax.(Ey.Rxy)) | | 2. a=a arbitrary object intro | | Goal: (Ey.Ray) | | | 3. (Ax.Rxb) witness intro line 1 | | | 4. Rab univ. elim. line 3 | | | 5. (Ey.Ray) exist. intro. line 4 | | 6. (Ey.Ray) exist. elim. line 5 | 7. (Ax.(Ey.Rxy)) univ. intro. lines 2-6 8. Theorem H7.5 imp. intro lines 1-7