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