1. |
Premise |
|
1 |
|
(^w)(Bw&Cw) |
1 ^E |
|
2 |
|
Ba&Ca |
2 &E |
|
3 |
|
Ba |
3 ^I |
|
4 |
|
(^w)Bw |
2 &E |
|
5 |
|
Ca |
5 ^I |
|
6 |
|
(^y)Cy |
|
|
7 |
|
|
4,6 &I |
|
8 |
|
(^w)Bw&(^y)Cy |
~~~~ |
|
9 |
|
~Part II~~~~ |
Premise |
|
10 |
|
(^w)Bw&(^y)Cy |
10 &E |
|
11 |
|
(^w)Bw |
11 ^E |
|
12 |
|
Ba |
10 &E |
|
13 |
|
(^y)Cy |
13 ^E |
|
14 |
|
Ca |
12,14 &I |
|
15 |
|
Ba&Ca |
|
|
16 |
|
|
15 ^I |
|
17 |
|
(^w)(Bw&Cw) |
|
2. |
Premise |
|
1 |
|
Na>(^x)Tx |
|
Assumption |
|
2 |
|
....what if |
Na |
1,2 >E |
|
3 |
|
....then... |
(^x)Tx |
3 ^E |
|
4 |
|
....then... |
Tb |
|
|
5 |
|
|
|
|
|
6 |
|
|
|
2-4 >I |
|
7 |
|
Na>Tb |
|
7 ^I |
|
8 |
|
(^x)(Na>Tx) |
|
~~~~ |
|
9 |
|
~ Part II ~ |
~~~~ |
Premise |
|
10 |
|
(^x)(Na>Tx) |
|
Assumption |
|
11 |
|
....what if |
Na |
10 ^E |
|
12 |
|
....then... |
Na>Tb |
11,12 >E |
|
13 |
|
....then... |
Tb |
13 ^I |
|
14 |
|
....then... |
(^x)Tx |
|
|
15 |
|
|
|
|
|
16 |
|
|
|
11-14 >I |
|
17 |
|
Na>(^x)Tx |
|
|
4. |
Premise |
|
1 |
|
(%y)My>Ma |
|
|
Assumption |
|
2 |
|
....what if |
Mb |
|
2 %I |
|
3 |
|
....then... |
(%y)My |
|
1,3 >E |
|
4 |
|
....then... |
Ma |
|
|
|
5 |
|
|
|
|
|
|
6 |
|
|
|
|
2-4 >I |
|
7 |
|
Mb>Ma |
|
|
7 ^I |
|
8 |
|
(^y)(My>Ma) |
|
|
~~~~ |
|
9 |
|
~ Part II ~ |
~~~~ |
~~~~ |
Premise |
|
10 |
|
(^y)(My>Ma) |
|
|
Assumption |
|
11 |
|
....what if |
(%y)My |
|
Assumption |
|
12 |
|
....then... |
....what if |
Mt |
10 ^E |
|
13 |
|
....then... |
....then... |
Mt>Ma |
12,13 >E |
|
14 |
|
....then... |
....then... |
Ma |
11,12-14 %E |
|
15 |
|
....then... |
Ma |
|
|
|
16 |
|
|
|
|
11-15 >I |
|
17 |
|
(%y)My>Ma |
|
|
|
1. |
Premise |
|
1 |
|
(^x)(Ax&~Ax) |
1 ^E |
|
2 |
|
Aa&~Aa |
2 &E |
|
3 |
|
Aa |
2 &E |
|
4 |
|
~Aa |
|
2. |
Premise |
|
1 |
|
(%x)(Ax&~Ax) |
|
|
Assumption |
|
2 |
|
....what if |
At&~At |
|
Assumption |
|
3 |
|
....then... |
....what if |
~(X&~X) |
2 &E |
|
4 |
|
....then... |
....then... |
At |
2 &E |
|
5 |
|
....then... |
....then... |
~At |
3-5 ~E |
|
6 |
|
....then... |
X&~X |
|
1,2-6 %E |
|
7 |
|
X&~X |
|
|
7 &E |
|
8 |
|
X |
|
|
7 &E |
|
9 |
|
~X |
|
|
|
3. |
Premise |
|
1 |
|
(%x)Axv(%x)Bx |
|
|
Premise |
|
2 |
|
~(%y)(AyvBy) |
|
|
Assumption |
|
3 |
|
....what if |
(%x)Ax |
|
Assumption |
|
4 |
|
....then... |
....what if |
At |
4 vI |
|
5 |
|
....then... |
....then... |
At v Bt |
5 %I |
|
6 |
|
....then... |
....then... |
(%y)(Ay v By) |
3,4-6 %E |
|
7 |
|
....then... |
(%y)(Ay v By) |
|
3-7 >I |
|
8 |
|
(%x)Ax>(%y)(AyvBy) |
|
|
Assumption |
|
9 |
|
....what if |
(%x)Bx |
|
Assumption |
|
10 |
|
....then... |
....what if |
Bt |
10 vI |
|
11 |
|
....then... |
....then... |
At v Bt |
11 %I |
|
12 |
|
....then... |
....then... |
(%y)(Ay v By) |
9,10-12 %E |
|
13 |
|
....then... |
(%y)(Ay v By) |
|
9-13 >I |
|
14 |
|
(%x)Bx>(%y)(AyvBy) |
|
|
1,8,14 vE |
|
15 |
|
(%y)(AyvBy) |
|
|
|
4. |
Premise |
|
1 |
|
(^x)(%y)(Txy>Bx) |
|
|
Premise |
|
2 |
|
(%y)(^x)(Tyx&~By) |
|
|
Assumption |
|
3 |
|
....what if |
(^x)(Ttx&~Bt) |
|
1 ^E |
|
4 |
|
....then... |
(%y)(Tty>Bt) |
|
Assumption |
|
5 |
|
....then... |
....what if |
Ttu>Bt |
3 ^E |
|
6 |
|
....then... |
....then... |
Ttu&~Bt |
6 &E |
|
7 |
|
....then... |
....then... |
Ttu |
5,7 >E |
|
8 |
|
....then... |
....then... |
Bt |
6 &E |
|
9 |
|
....then... |
....then... |
~Bt |
8,9 &I |
|
10 |
|
....then... |
....then... |
Bt&~Bt |
4,5-10 %E |
|
11 |
|
....then... |
Bt&~Bt |
|
Assumption |
|
12 |
|
....then... |
....what if |
~(X&~X) |
11 &E |
|
13 |
|
....then... |
....then... |
Bt |
11 &E |
|
14 |
|
....then... |
....then... |
~Bt |
12-14 ~E |
|
15 |
|
....then... |
X&~X |
|
2,3-15 %E |
|
16 |
|
X&~X |
|
|
16 &E |
|
17 |
|
X |
|
|
16 &E |
|
18 |
|
~X |
|
|
|