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.
Best Answer
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$.