Next: Tuesday, February 29 Up: Lecture Notes Previous: Friday, February 25 -

## Monday, February 28

Homework 7 handout distributed; due on March 6.

```We're going to talk about some simple logical principles from section 4.3
before continuing with the extended additivity example.

Please see under Homework 7 above for the forms of the sentences to be
formally proved as indicated on the first page of the handout.

I adopt the convention henceforth that ``A'' and ``E'' should not
appear as predicates, in order to avoid confusion with the quantifiers
Ax and Ex in their ``typewriter'' forms.

Here are the things we proved in class:

Goal:  ~(Ex.Px)<->(Ax.~Px)

unpack into two subgoals (implications):

Goal:  ~(Ex.Px)->(Ax.~Px)

open a box for imp intro:

|  1. ~(Ex.Px)             subpremise
|  Goal:  (Ax.~Px)

open a box for univ intro:

| | 2.  a=a                arbitrary object intro
| | Goal:  ~Pa

open a box for neg. intro:

| | | 3.  Pa               subpremise
| | | 4.  (Ex.Px)          exist. intro. line 3
| | | 5.  (Ex.Px) & ~(Ex.Px)    c.i. lines 1,4
| | 6. ~Pa                 neg. intro. lines 3-5
| 7. (Ax.~Px)              univ. intro. lines 2-6
8. ~(Ex.Px)->(Ax.~Px)      imp. intro. lines 1-7

We return to the second subgoal of our proof of a biconditional.

Goal:  (Ax.~Px)->~(Ex.Px)

Open a box for imp. intro.

| 9. (Ax.~Px)              subpremise
| Goal: ~(Ex.Px)

open a box for neg intro

| | 10. (Ex.Px)                subpremise

introduce a witness

| | | 11. Pb                   witness intro line 10
| | | 12. ~Pb                  univ elim line 9

Mr. Egbert originally wrote Pb & ~Pb here, then looked at
it and realized that he couldn't finish the neg intro at
this point because he was one box too deep...

| | | 13. A & ~A               neg. elim. lines 11,12
| | 14. A & ~A                 exist. elim.  lines 11-13

The funny looking contradiction proved is because we couldn't
get out of the ``witness box'' with the obvious Pb & ~Pb.
I omitted the line with Pb & ~Pb found in the original
board proof because neg. elim. also works with two previous lines
as shown.

It is worth noting that a proof by exist.elim. always ends by
copying the last line inside the box to the outside -- that last
line cannot mention the witness declared in the box.

| 15.  ~(Ex.Px)                neg. intro. lines 10-14
16. (Ax.~Px)->~(Ex.Px)         imp. intro. lines 9-15

17. ~(Ex.Px)<->(Ax.~Px)        biconditional intro lines 8,16

Here is the proof as a finished product without my remarks between the
lines.

Goal:  ~(Ex.Px)<->(Ax.~Px)
Goal:  ~(Ex.Px)->(Ax.~Px)
|  1. ~(Ex.Px)             subpremise
|  Goal:  (Ax.~Px)
| | 2.  a=a                arbitrary object intro
| | Goal:  ~Pa
| | | 3.  Pa               subpremise
| | | 4.  (Ex.Px)          exist. intro. line 3
| | | 5.  (Ex.Px) & ~(Ex.Px)    c.i. lines 1,4
| | 6. ~Pa                 neg. intro. lines 3-5
| 7. (Ax.~Px)              univ. intro. lines 2-6
8. ~(Ex.Px)->(Ax.~Px)      imp. intro. lines 1-7
Goal:  (Ax.~Px)->~(Ex.Px)
| 9. (Ax.~Px)              subpremise
| Goal: ~(Ex.Px)
| | 10. (Ex.Px)                subpremise
| | | 11. Pb                   witness intro line 10
| | | 12. ~Pb                  univ elim line 9
| | | 13. A & ~A               neg. elim. lines 11,12
| | 14. A & ~A                 exist. elim.  lines 11-13
| 15.  ~(Ex.Px)                neg. intro. lines 10-14
16. (Ax.~Px)->~(Ex.Px)         imp. intro. lines 9-15
17. ~(Ex.Px)<->(Ax.~Px)        biconditional intro lines 8,16

Here's the second statement we proved in class:

Goal:  (Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx)

open a box for imp. intro:

| 1. (Ax.Px & Qx)              subpremise
Goal: (Ax.Px) & (Ax.Qx)

This breaks into two subgoals:

Goal: (Ax.Px)

Open a box for univ. intro:

| | 2. a = a                      arbitrary object intro
| | Goal:  Pa
| | 3. Pa & Qa                    univ. elim. line 1
| | 4. Pa                         c.e. line 3
| 5. (Ax.Px)                      univ. intro. 2-4

Now someone observed that the rest of the proof would look
essentially the same; one could use one's editor to copy
it and make a few changes to prove (Ax.Qx), like this:

Goal: (Ax.Qx)

| | B2. a = a                      arbitrary object intro
| | Goal:  Pa
| | B3. Pa & Qa                    univ. elim. line 1
| | B4. Qa                         c.e. line 3
| B5. (Ax.Qx)                      univ. intro. 2-4

Notice that all I had to do was tag the line numbers and change the
conjunct in line B4 to Qa and the conclusion.  The proof would be
completed with

| 6.  (Ax.Px)& (Ax.Qx)             c.i. 5,B5
7.(Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx)  imp. intro lines 1-6.

One can do this even more economically by reusing the same box for the
two univ. intro. subproofs, as follows:

Goal:  (Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx)
| 1. (Ax.Px & Qx)              subpremise
Goal: (Ax.Px) & (Ax.Qx)
Goal: (Ax.Px)
| | 2. a = a                      arbitrary object intro
| | Goal:  Pa
| | 3. Pa & Qa                    univ. elim. line 1
| | 4. Pa                         c.e. line 3
| | 5. Qa
| 6. (Ax.Px)                      univ. intro. 2-4
Goal: (Ax.Qx)
| 7. (Ax.Qx)                      univ. intro. 2-5 (reusing the box)
| 8. (Ax.Px)& (Ax.Qx)             c.i. 6,7
9.(Ax.Px & Qx) -> (Ax.Px) & (Ax.Qx)  imp. intro lines 1-8.

If this makes you queasy, don't do it in your proofs!  But I know that
some of you can carry this off correctly.
```

Randall Holmes
2000-05-05