next up previous
Next: Friday, February 25 - Up: Lecture Notes Previous: February 16, 2000

Tuesday, February 22 and Wednesday, February 23

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).



Randall Holmes
2000-05-05