Next: Notes for March 1, Up: Lecture Notes Previous: Monday, February 28

## Tuesday, February 29

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

Randall Holmes
2000-05-05