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.
You are correct that the first approach, while perfectly logical, is not supported by the Fitch rules.
The second approach could work, if you have $P \lor \neg P$, for then you can use $\lor$ Elim to get $\bot$ from $P \lor \neg P$ and the two subproofs. Now, you can prove $P \lor \neg P$ in Fitch without any further assumptions, but a far easier approach is to just use 1 subproof, and use it as a Proof by Contradiction:
Start a subproof with $P$.
Get $\neg P$ using $\leftrightarrow$ Elim.
Now get $\bot$ between $P$ and $\neg P$.
Close the subproof and conclude $\neg P$ using $\neg $ Intro.
Get $P$ using $\leftrightarrow$ Elim.
Get $\bot$ between $P$ and $\neg P$.