# Formal proof in Fitch - How to prove contradiction in a biconditional?

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:

1. 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.
2. 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$.