How would I go about showing this? Intuitively this is very simple, but I've never been asked to prove an $\iff$ relation with $\iff$ inside of it:
$(A \iff B) \iff (\lnot A \iff \lnot B)$
How would I go about showing this? Intuitively this is very simple, but I've never been asked to prove an $\iff$ relation with $\iff$ inside of it:
$(A \iff B) \iff (\lnot A \iff \lnot B)$
Rewrite $A\iff B$ as $(A \wedge B)\vee(\lnot A \wedge \lnot B)$ then you will get
$$\begin{array}{rcl}&& (A\iff B) \\ &\iff& \left( (A \wedge B)\vee(\lnot A \wedge \lnot B) \right)\\ &\iff& \left( (\lnot A \wedge \lnot B)\vee( A \wedge B)\right) \\ &\iff& \left(( \lnot A \wedge \lnot B)\vee( \lnot(\lnot A) \wedge \lnot(\lnot B))\right) \\ &\iff& (\lnot A\iff \lnot B) \end{array}$$
It depends on what the basic rules about $\;A \iff B\;$ that you are allowed to use: Is it considered a primitive (as in the 'equational logic' of Dijkstra and Gries-Schneider), or is it an abbreviation for $\;(A \implies B) \land (B \implies A)\;$, as $\;(A \land B) \lor (\lnot A \land \lnot B)\;$, or yet another variation?
If $\;\iff\;$ is a primitive, or in general if you are allowed to use the fact that $\;\iff\;$ is associative (in addition to some other properties), then you can just leave out the parentheses, and calculate \begin{align} & A \iff B \;\iff\; \lnot A \iff \lnot B \\ = & \qquad \text{"use symmetry of the middle $\;\iff\;$"} \\ & A \iff \lnot A \;\iff\; B \iff \lnot B \\ = & \qquad \text{"$\;P \iff \lnot P\;$ is always false"} \\ & \text{false} \;\iff\; \text{false} \\ = & \qquad \text{"$\;P \iff P\;$ is always true"} \\ & \text{true} \\ \end{align}
Otherwise, you can use an approach as in the first answer.
$(A \iff B)$
$\iff ([A\implies B] \wedge [B \implies A])$ (Definition of $\iff$)
$\iff ([\lnot A \vee B] \wedge [\lnot B \vee A])$ (Equivalence of $\implies$)
$\iff ([\lnot B \vee A] \wedge [\lnot A \vee B])$ (Commutativity of $\wedge$)
$\iff ([A \vee \lnot B] \wedge [B \vee \lnot A])$ (Commutativity of $\vee$)
$\iff ([\lnot A \implies \lnot B] \wedge [\lnot B \implies \lnot A])$ (Equivalence of $\implies$)
$\iff (\lnot A \iff \lnot B)$ (Definition of $\iff$)