| 1. |
| Assumption |
|
1 |
|
....what if |
~(^y)Gyy |
| 1 QN |
|
2 |
|
....then... |
(%y)~Gyy |
| 2 DN |
|
3 |
|
....then... |
(%y)~~~Gyy |
| 1-3 >I |
|
4 |
|
~(^y)Gyy>(%y)~~~Gyy |
|
|
| 2. |
| Assumption |
|
1 |
|
....what if |
(^y)~Py |
|
|
|
| Assumption |
|
2 |
|
....then... |
....what if |
(%z)Pz |
|
|
| Assumption |
|
3 |
|
....then... |
....then... |
....what if |
Pt |
|
| Assumption |
|
4 |
|
....then... |
....then... |
....then... |
....what if |
~(Q&~Q) |
| 3 R |
|
5 |
|
....then... |
....then... |
....then... |
....then... |
Pt |
| 1 ^E |
|
6 |
|
....then... |
....then... |
....then... |
....then... |
~Pt |
| 4-6 ~E |
|
7 |
|
....then... |
....then... |
....then... |
Q&~Q |
|
| 2,3-7 %E |
|
8 |
|
....then... |
....then... |
Q&~Q |
|
|
| 8 &E |
|
9 |
|
....then... |
....then... |
Q |
|
|
| 8 &E |
|
10 |
|
....then... |
....then... |
~Q |
|
|
| 2-10 ~I |
|
11 |
|
....then... |
~(%z)Pz |
|
|
|
| 1-11 >I |
|
12 |
|
(^y)~Py>~(%z)Pz |
|
|
|
|
|
| 3. |
| Assumption |
|
1 |
|
....what if |
~[(^x)Ax v (%x)~Ax] |
| 1 DM |
|
2 |
|
....then... |
~(^x)Ax&~(%x)~Ax |
| 2 &E |
|
3 |
|
....then... |
~(^x)Ax |
| 2 &E |
|
4 |
|
....then... |
~(%x)~Ax |
| 3 QN |
|
5 |
|
....then... |
(%x)~Ax |
| 1-5 ~E |
|
6 |
|
(^x)Axv(%x)~Ax |
|
|
| 4. |
| Assumption |
|
1 |
|
....what if |
~(^x)Ax |
|
| 1 QN |
|
2 |
|
....then... |
(%x)~Ax |
|
| Assumption |
|
3 |
|
....then... |
....what if |
~At |
| 3 vI |
|
4 |
|
....then... |
....then... |
~At v Bt |
| 4 IM |
|
5 |
|
....then... |
....then... |
At>Bt |
| 5 %I |
|
6 |
|
....then... |
....then... |
(%x)(Ax>Bx) |
| 2,3-6 %E |
|
7 |
|
....then... |
(%x)(Ax>Bx) |
|
| 1-7 >I |
|
8 |
|
~(^x)Ax>(%x)(Ax>Bx) |
|
|
|