# Can the natural deduction system prove $P \iff ¬P$ to show that it's a contradiction?

I use the Fitch notation for the natural deduction system. More information on https://en.wikipedia.org/wiki/Fitch_notation.

In attempting to derive "$P \iff ¬P$" without any previous assumptions, I can't seem to get anywhere.

My 1st approach is to indirectly prove this (IP), so the proof would begin as a sub-proof $¬(P \iff ¬P)$. but I can't seem to arrive at any sort of useful contradiction.

My second approach is directly proving that $P \Rightarrow ¬P$ and $¬P \Rightarrow P$, but getting the negation of either seems like a dead-end.

Unless the derivational system you use is unsound, you can only derive statements from other statements if they logically follow. Put differently: if you don't have any statements to begin with, the only statements you can prove are tautologies. $P \leftrightarrow \neg P$ is a contradiction, and so cannot be proven without any assumptions.

So, it is no wonder you are not getting anywhere ... you are trying to do the impossible!

Now, if your question is: OK, so I can't prove $P \leftrightarrow \neg P$ ... but can I use a proof system to prove that $P \leftrightarrow \neg P$ is a contradiction? Yes, you can! But to do that, you need to derive a contradiction from $P \leftrightarrow \neg P$, i.e. You need to make $P \leftrightarrow \neg P$ an assumption, and if you can now derive a contradiction, then that shows that $P \leftrightarrow \neg P$ is a contradiction as well, since the only kind of statement from which you can derive a contradiction is a contradiction itself.

My 1st approach is to indirectly prove this (IP), so the proof would begin as a sub-proof $¬(P \iff ¬P)$. but I can't seem to arrive at any sort of useful contradiction.

My second approach is directly proving that $P \Rightarrow ¬P$ and $¬P \Rightarrow P$, but getting the negation of either seems like a dead-end.

Use the first approach and show that $P\to \neg P$ and $\neg P\to P$ contradict each other, so therefore $\neg(P\leftrightarrow\neg P)$.

Hint: $P\to\neg P \vdash \neg P$

$$\def\hideit#1{}\def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}}\hideit{\small\fitch{}{\fitch{P\leftrightarrow\neg P\hspace{16.5ex}\text{Assumption}}{(P\to\neg P)\wedge(\neg P\to P)\hspace{4ex}\text{Biconditional Elimination}\\[1ex]P\to \neg P\hspace{16.5ex}\text{Conjunction Elimination}\\\fitch{P\hspace{21ex}\text{Assumption}}{\neg P\hspace{20ex}\text{Conjunction Elimination}\\\bot\hspace{21.5ex}\text{Contradiction}}\\\neg P\hspace{21.5ex}\text{Negation Introduction}\\[1ex] \neg P\to P\hspace{17ex}\text{Conjunction Elimination}\\ P\hspace{22.75ex}\text{Conditional Elimination}\\[1.5ex]\bot\hspace{22.75ex}\text{Contradiction}}\\\neg(P\leftrightarrow\neg P)\hspace{15.25ex}\text{Negation Introduction}}\\\vdash \neg(P\leftrightarrow\neg P)}$$