Proof: Biconditional is equivalent to biconditional between its negated sides Given that:
$P \leftrightarrow Q$
How can I prove:
$\neg P \leftrightarrow \neg Q$
It's pretty obvious, but the best I can come up with is "well just look at the truth table, damn it". Is there a more formal way to show this? Is there a name for this rule?
 A: $P \leftrightarrow Q \Leftrightarrow$
$(P \rightarrow Q) \land (Q \rightarrow P) \Leftrightarrow$ (contraposition)
$(\neg Q \rightarrow \neg P) \land (\neg P \rightarrow \neg Q) \Leftrightarrow$
$\neg P \leftrightarrow \neg Q$
A: Assuming you are working in classical propositional logic, one way that does not rely on the full truth table of the equivalence, but still relies on some truth table, is as follows:


*

*Decompose $P \iff Q$ in $(P \implies Q) \land (Q \implies P)$ and then show that for all propositions $P$ and $Q$, $(P \implies Q) \implies (\neg Q \implies \neg P)$.

*Remark that $P \implies Q$ and $\neg P \lor Q$ have the same truth table (or you may have $P \implies Q$ defined as $\neg P \lor Q$). From this, $\neg \neg Q \lor \neg P \implies Q \lor \neg P$, since from the law of excluded middle you get $\neg \neg Q \implies Q$. This gives you $(P \implies Q) \implies (\neg Q \implies \neg P)$, which is the building block you needed.
A: Here is a proof using a Fitch-style natural deduction proof checker. I don't know if there is a name for the equivalence.

On the right side of the page displaying the proof checker are definitions of the inference rules used above: biconditional elimination (↔E). biconditional introduction (↔I), negation elimination (¬E) and negation introduction (¬I).

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
