If, from an assumption ¬P in some subproof, you can infer { } in that subproof
Then you can infer P in that subproof
1. F <=> (M ^ P)
2. M
3. P
4. Therefore, F
1a. | ¬FM | // assumption, from 1 |
1b. | ¬FP | // assumption, from 1 |
1c. | ¬M¬PF | // assumption, from 1 |
2. | M | // assumption, from 2 |
3. | P | // assumption, from 3 |
* 4. | ¬F | // temporary assumption, from 4 |
* 5. | ¬M¬PF | // send 1c |
* 6. | ¬M¬P | // 1c, 4, Resolution |
* 7. | M | // send 2 |
* 8. | ¬P | // 6, 7, Resolution |
* 9. | P | // send 3 |
*10. | { } | // 8, 9, Resolution |
*11. | F | // 4, 10, ¬Elimination |
12. | F | // return 11 |