Negation of if and only if?
Solution 1:
$X\leftrightarrow Y$ is the conjunction of $X\leftarrow Y$ and $X\rightarrow Y$. The negation of a conjunction is the disjunction of the negations; the negation of $P\rightarrow Q$ is $P\wedge \neg Q$. So we have: \begin{align*} \neg(X\leftrightarrow Y) &\Longleftrightarrow \neg\Bigl( (X\rightarrow Y)\wedge (Y\rightarrow X)\Bigr)\\ &\Longleftrightarrow \neg(X\rightarrow Y)\vee \neg(Y\rightarrow X)\\ &\Longleftrightarrow (X\wedge \neg Y) \vee (Y\wedge \neg X). \end{align*} So the negation of "$X$ is true if and only if $Y$ is true" is "Either $X$ is true and $Y$ is false, or $X$ is false and $Y$ is true." Added: as it happens, as noted by Rahul Narain in his comment, this is in turn equivalent to "$X$ is true if and only if $Y$ is false" (just compare the cases when they are each true). So you also get that $$\neg(X\leftrightarrow Y) \Longleftrightarrow X\leftrightarrow \neg Y \Longleftrightarrow \neg X\leftrightarrow Y.$$
Solution 2:
The digital equivalent is P = X XNOR Y, and thus the negation is (not P) = X XOR Y. In other words, P is false when X is true but Y is false, or when X is false but Y is true.
Solution 3:
Yes, but you have to be very precise here, because the negation of implication is exclusive (not inclusive) OR. So the answer is "Either $X$ or $Y$ is false, but not both".
In general, if you are confused, start with a truth table for implication and then negate it. Resulting table matches XOR (exclusive OR).
Solution 4:
You are not right. Let $X = (\ell$ is even) and $Y = (\ell$ is not odd). Then clearly $X \Leftrightarrow Y$, but "($\ell$ is not even) or ($\ell$ is odd)" is strictly weaker; you want "($\ell$ is not even) $\Leftrightarrow$ ($\ell$ is odd)" to be true.