On these two days, we talked about an example from Grantham which I have been slow about getting out on the web... The problem in Grantham is to show that the conclusion (Ax.(Ey.Ryx)) can be drawn from the premises P1. (Ax.(Ey.(Rxy)) premise P2. (Ex.(Ay.Ay | Rxy)) premise P3. (Ax.(Ay.((Rxy & Ax) -> Ryx))) premise We outline an informal proof in English. Choose an arbitrary object a. Either Aa or ~Aa. There is a witness b to P2 -- i.e., an object b such that (Ay.Ay | Rby) [sorry about the predicate A and the quantifier...] If ~Aa then Rba, and so (Ey.Rya) by the choice of b. If Aa then by P1 there is an object c such that Rac. By P3, (Rac & Aa) -> Rca, and the hypothesis of this implication is true. From Rca follow the desired conclusion (Ey.Rya). By cases, (Ey.Rya) must be true. Since a was chosen arbitrarily, (Ax.(Ey.Ryx)) must be true. Now we do it formally. We take lines P1-3 as beginning our proof. Goal: (Ax.(Ey.Ryx)) | 1. a = a arbitrary object intro | Goal: (Ey.Rya) | 2. Aa | ~Aa excluded middle (for argument by cases) | Goal: Aa -> (Ey.Rya) | | 3. Aa subpremise | | Goal: (Ey.Rya) | | 4. (Ey.Ray) univ. elim, P1 | | | 5. Rac witness intro, line 4 | | | 6. (Rac & Aa) -> Rca univ elim., twice, P3 | | | 7. Rac & Aa c.i. lines 3,5 | | | 8. Rca m.p. lines 6,7 | | | 9. (Ey.Rya) exist. intro 8 | | 10. (Ey.Rya) exist. elim. 5-9 | 11. Aa -> (Ey.Rya) imp. intro lines 3-10 | Goal: ~Aa -> (Ey.Rya) | | 12. ~Aa subpremise | | Goal: (Ey.Rya) | | | 13. (Ay.Ay | Rby) witness intro, P2 | | | 14. Aa | Rba univ. elim. line 13 | | | 15. Rba d.e. lines 12,14 | | | 16. (Ey.Rya) exist. intro line 15 | | 17. (Ey.Rya) exist. elim. lines 13-16 | 18. ~Aa -> (Ey.Rya) imp. intro. lines 12-17 | 19. (Ey.Rya) proof by cases, 2,11,18 20. (Ax.(Ey.Ryx)) univ. intro lines 1-19 That at least puts our in-class proof (though I don't know which case we did first) on record. On Wednesday, I looked at an example of invalid reasoning from Grantham; it also brought out differences between Grantham's system and ours caused by the fact that witness introduction isn't packed in boxes in Grantham's system. On p. 6-21 of Grantham there is a proof fragment which we might try to translate into our terminology as follows: | 3. a = a arbitrary object intro | | 5. Aa subpremise | | 6. (Ey.Ray) univ. elim, line P1 | | | 7. Rab witness intro, line 6 Note: Grantham writes something like b[a] instead of just b; he needs to signal dependence of the witness b on the choice of a. | | | 8. (Rab & Aa) -> Rba univ elim twice, P3 | | | 9. Rba mp and ci, lines 5,7,8 | *10. Aa -> Rba ?imp. intro lines 5-9 Grantham annotates this line as ``perfectly all right'', as in his system it is. But in ours it is bogus; you cannot use imp. intro. on lines 5-9 because 9 is in a further box -- we proved 9 with an additional premise not available at line 5. However, this can be fixed by putting line 5 after line 7 and reversing the order of the boxes, I suppose. I'm actually not convinced that it's really ``perfectly OK'' even in Grantham's system. And finally we have the truly awful line *11. (Ax.Ax->Rbx) *unive intro lines 3-10 which is what Grantham specifically wanted to warn us against. The reason this is detectably wrong in Grantham's system is that b is actually written throughout as b[a], to signal that the choice of the witness b may depend on the arbitrarily chosen object a. In our system, this kind of problem is controlled by the fact that witnesses are introduced inside boxes (they are ``locally declared''). As a result, line 10 is already recognizably wrong -- we cannot terminate the imp. intro. proof in the box beginning on line 5 until we get out of the box beginning on line 7 (which should end with an application of exist. elim, but is instead rudely and incorrectly terminated with line *10).