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


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