Today we did more formal proofs at the board.
Goal: (Ex.(Px&S)) <-> (Ex.Px)&S (where x is not free in S) This breaks into two subgoals, (Ex.(Px&S)) -> (Ex.Px)&S and (Ex.Px)&S -> (Ex.(Px&S)), which were done by different groups of students at the board. Goal: (Ex.(Px&S)) -> (Ex.Px)&S This calls for a proof by imp. intro. | 1. (Ex.(Px&S)) subpremise | Goal: (Ex.Px)&S which breaks into two separate goals: | Goal: (Ex.Px) Now we are going to use the existential hypothesis in line 1. | | 2. Pa&S witness intro, line 1 | | 3. Pa c.e. line 2 | | 4. (Ex.Px) exist. intro. line 3 Now we have a statement without the locally declared variable a in it, which we can copy out of the box: | 5. (Ex.Px) exist. elim. lines 2-4 The proof of S is the same. | | 6. Pa & S witness intro, line 1 | | 7. S c.e. line 6 | 8. S exist. elim. lines 6-7 It is important here that we know that S does not contain x. | 9. (Ex.Px)&S c.i. lines 4,8 10. (Ex.(Px&S)) -> (Ex.Px)&S imp. intro. lines 1-9 The proof can also be done with ``box recycling'': Goal: (Ex.(Px&S)) -> (Ex.Px)&S | 1. (Ex.(Px&S)) subpremise | Goal: (Ex.Px)&S | Goals: (Ex.Px), S | | 2. Pa&S witness intro, line 1 | | 3. Pa c.e. line 2 | | 4. (Ex.Px) exist. intro. line 3 | | 5. S c.e. line 2 | 6. (Ex.Px) exist. elim. lines 2-4 | 7. S exist. elim. lines 2-5 | 8. (Ex.Px)&S c.i. lines 6,7 9. (Ex.(Px&S)) -> (Ex.Px)&S imp. intro. lines 1-8 The other half of the proof of equivalence: Goal: (Ex.Px)&S -> (Ex.(Px&S)) | 1. (Ex.Px)&S subpremise | 2. (Ex.Px) c.e. line 1 | | 3. Pa witness intro line 2 | | 4. S c.e. line 1 | | 5. Pa&S c.i. lines 3,4 | | 6. (Ex.Px&S) exist. intro. line 5 | 7. (Ex.Px&S) exist. elim. lines 3-6 8. (Ex.Px)&S -> (Ex.(Px&S)) imp. intro lines 1-7 Both sides of this proof contain examples of this pattern of reasoning from an existential hypothesis to an existential conclusion: n. (Ex.Px) ??? . . . | n+i Pa witness intro, line n | . | . | . | n+i+j Qa ??? | n+i+j+1 (Ex.Qx) exist. intro, line n+i+j. n+i+j+2 (Ex.Qx) exist. elim,. lines (n+i)-(n+i+j+1) This shows the validity of the following derived rule, which students seemed to want: n. (Ex.Px) ??? . . . | n+i Pa witness intro, line n | . | . | . | n+i+j Qa ??? n+i+j+1 (Ex.Qx) ``existential transformation'', lines (n+i)-(n+i+j) This rule is both an introduction and an elimination rule (thus ``transformation''); it avoids the extra ``copying'' step in exist. elim. but it is only usable for existential conclusions. I don't necessarily recommend using it, but I make it available officially... Another example: (Ax.Px->Qx) -> ((Ax.Px)->(Ax.Qx)) | 1. (Ax.Px->Qx) subpremise | Goal: (Ax.Px) -> (Ax.Qx) | | 2. (Ax.Px) subsubpremise | | Goal: (Ax.Qx) | | | 3. a = a arbitrary object intro | | | Goal: Qa | | | 4. Pa->Qa univ. elim. line 1 | | | 5. Pa univ. elim. line 2 | | | 6. Qa m.p. lines 4,5 | | 7. (Ax.Qx) univ. intro. lines 3-6 | 8. (Ax.Px) -> (Ax.Qx) imp. intro. lines 2-7 9. (Ax.Px->Qx) -> ((Ax.Px)->(Ax.Qx)) imp. intro. lines 1-8 This proof almost writes itself if you put the Goal: statements in... One I pulled out of a hat: Goal: ((Ex.Px)->S) <-> (Ax.(Px->S)) where x does not occur free in S This breaks into two implications: Goal: ((Ex.Px)->S) -> (Ax.(Px->S)) | 1. (Ex.Px)->S) subpremise | Goal: (Ax.(Px->S)) | | 2. a = a arbitrary object intro | | Goal: Pa -> S | | | 3. Pa subsubpremise | | | 4. (Ex.Px) exist. intro. line 3 | | | 5. S m.p. lines 1,4 | | 6. Pa -> S imp. intro. lines 3-5 | 7. (Ax.Px->S) univ. intro. lines 2-6 8. ((Ex.Px)->S) -> (Ax.(Px->S)) imp. intro. lines 1-7 Goal: (Ax.(Px->S)) -> ((Ex.Px)->S) | 9. (Ax.(Px->S)) subpremise | Goal: ((Ex.Px)->S) | | 10. (Ex.Px) subsubpremise | | | 11. Pa witness intro, line 10 | | | 12. Pa -> S univ. elim. line 9 | | | 13. S modus ponens, lines 11,12 | | 14. S exist. elim. lines 11-13 | 15. ((Ex.Px)->S) imp. intro. lines 10-14 16. (Ax.(Px->S)) -> ((Ex.Px)->S) imp. intro. lines 9-15 17. ((Ex.Px)->S) <-> (Ax.(Px->S)) biconditional intro, lines 8,16 This is another one which practically writes itself. I was reminded of this proof by a conversation with Dr. Kerr about an argument he had with his students in M187. The English sentence ``Anyone who gives money to a politician is rich'' can be translated into this logical form: (Ax.(Ey.(Gxy & Py))->Rx) where Gxy means ``x gives to y'', Py means ``y is a politician'' and Rx means ``x is rich''. Dr. Kerr's students argued that it should be (Ax.((Gxy & Py)->Rx)) They didn't think that a quantifier was needed: they claimed that ``a politician'' referred to a particular politician y (which seems superficially reasonable). Armed with the proof above, we can observe that (Ey.(Gxy & Py))->Rx is equivalent to (Ay.(Gxy & Py)->Rx), so the whole statement is equivalent to (Ax.(Ay.(Gxy & Py)->Rx)) which is a statement about _all_ politicians! This isn't hard to see in English, either: ``Anyone who gives money to any politician (at all) is rich'' is fairly easily seen to have the same meaning.