1. |
Premise |
|
1 |
|
(^x)Ax |
1 ^E |
|
2 |
|
Aa |
1 ^E |
|
3 |
|
Ab |
2,3 &I |
|
4 |
|
Aa&Ab |
|
3. |
Assumption |
|
1 |
|
....what if |
(^x)(Tx&~Ux) |
1 ^E |
|
2 |
|
....then... |
Ta&~Ua |
2 &E |
|
3 |
|
....then... |
Ta |
3 %I |
|
4 |
|
....then... |
(%y)Ty |
1-4 >I |
|
5 |
|
(^x)(Tx&~Ux)>(%y)Ty |
|
|
5. |
Premise |
|
1 |
|
(^y)(Ty>Uy) |
Premise |
|
2 |
|
Ta |
1 ^E |
|
3 |
|
Ta>Ua |
2,3 >E |
|
4 |
|
Ua |
2,4 &I |
|
5 |
|
Ua&Ta |
5 %I |
|
6 |
|
(%z)(Uz&Tz) |
|