I am asked to derive the conclusion $\bot$ from the premise: $P\leftrightarrow \neg P$
This is in the logic system of Fitch, the rules that I am allowed to use can be found here. I may not use tautological consequence to introduce additional premises.
I considered two approaches:
- restating the biconditional as the conjunction of two conditionals, but there isn't any rules in Fitch that allows the restatement, and I am not sure how I can derive a contradiction from a conjunction.
- Create two subproofs, one assuming $P$ and one assuming $\neg P$; by using the rule $\leftrightarrow$Elim, show in each case that the negation of the assumptions can be reached and thus leading to $\bot$ in each subproof. However, I don't know how I would combine the conclusions of these subproofs as a conclusion of the main proof.