0 |__ [assumption, want P iff not not P]
1 | |__ P [assumption, want not not P]
2 | | |__ not P [assumption, for reductio]
3 | | | contradiction [contradiction introduction: 1, 2]
4 | | not not P [negation introduction: 2]
|
5 | |__ not not P [assumption, want P]
6 | | P [negation elimination: 5]
|
7 | P iff not not P [biconditional introduction: 1 - 4, 5 - 6]
ergo go back t
We have placed cookies on your device to help make this website better. You can adjust your cookie settings, otherwise we'll assume you're okay to continue.
