First Order Logic and Some Validity Checking I'm sorry for put an image insted of typing it...
infact this is an 2012-exam on Logic. i found the solution of this quiz that wrote by one TA. he wrote just the second line is not valid logically in First Order Logic, but i think this answer is false and the just forth line is the correct one. anyone could judge me and help me?
$$\begin{align*}\rm\tag{1}\forall x\;\neg A(x) \to \exists x\;\big(A(x)\to\bot\big)
\\\rm\tag{2}
\forall x\;\big(A(x)\leftrightarrow B(x)\big)\leftrightarrow\big(\neg\forall x\;A(x)\leftrightarrow\neg\forall x\; B(x)\big)
\\\rm\tag{3}
\exists x\;\neg\big(A(x)\vee B(x)\big)\to\big(\exists x\;A(x)\vee \exists x\; B(x)\big)
\\\rm\tag{4}
\exists x\;\big(A(x)\to B(x)\big)\to\big(\exists x\;A(x)\vee \exists x\; B(x)\big) 
\end{align*}$$
 A: \begin{align*}\rm\tag{1}\forall x\;\neg A(x) \to \exists x\;\big(A(x)\to\bot\big)
\\\forall x \neg A(x)\to \exists\neg A(x)\tag{$\checkmark$}
\\[3ex]\rm\tag{2}
\forall x\;\big(A(x)\leftrightarrow B(x)\big)\leftrightarrow\big(\neg\forall x\;A(x)\leftrightarrow\neg\forall x\; B(x)\big)
\\ \text{see below}
\\[2ex]\rm\tag{3}
\exists x\;\neg\big(A(x)\vee B(x)\big)\to\big(\exists x\;A(x)\vee \exists x\; B(x)\big)
\\\neg \forall x\;\big(A(x)\vee B(x)\big)\to \exists x\;\big(A(x)\vee B(x)\big)
\tag{$\color{green}{\checkmark}$}
\\[2ex]\rm\tag{4}
\exists x\;\big(A(x)\to B(x)\big)\to\big(\exists x\;A(x)\vee \exists x\; B(x)\big) 
\\ \exists x\;\big(\neg A(x)\vee B(x)\big)\to \big(\exists x\;\neg A(x) \vee \exists x\; B(x)\big) \tag{$\color{red}{\times}$}
\end{align*}
The second one takes a little more work to show that you could not get to the consequent from the antecedent.
$\newcommand{\fro}{\leftarrow}\newcommand{\tofro}{\leftrightarrow}
\begin{align}
\forall x (A\tofro B) & \iff \forall x((A \wedge B)\vee (\neg A\wedge \neg B))
\\ & \implies (\exists x(A) \wedge \exists x(B))\vee(\exists x(\neg A) \wedge \exists x(\neg B))
\\ & \implies (\neg \forall x(\neg A) \wedge \neg\forall x(\neg B))\vee(\neg\forall x( A) \wedge \neg\forall x(B))
\\ 
\\ \neg\forall x \,A \tofro \neg\forall x\, B & \iff (\neg\forall x\, A\wedge \neg \forall x\, B )\vee(\forall x\, A\wedge \forall x\, B)
\end{align}$
