Show that $M \models (\exists x) (\alpha) $ if and only if there is an element $a\in A$ such that $M\models \alpha [s[x|a]]$.

Question

Let $M$ be an $L$-structure for some language first order language $L$. Let $(\exists x)(\alpha)$ be an abbreviation for the formula $¬[(\forall x )(¬\alpha)]$.

Show that $M \models (\exists x) (\alpha) $ if and only if there is an element $a\in A$ such that $M\models \alpha [s[x|a]]$.

My attempt :

$M\models (\exists x)(\alpha)[s] \ \leftrightarrow \ M \models ¬(\forall x)(¬\alpha)[s] \ \leftrightarrow \ \text{for each $a\in$ A}\ , M \not\ \not\models (¬\alpha)[s[x|a]] \leftrightarrow \text{there is no $a\in A$ s.t.} \ M\models (¬\alpha)[s[x|a]] \leftrightarrow \text{there is no $a\in A$ s.t.}\ M\not\models \alpha [s[x|a]] $

Now , I don't know where to go to show the required! any help please ?

This is exercise $7$ section $1.7$ page $39$ from friendly introduction to logic by Leary

Answer 1

Your attempt is almost right. By De Morgan's law (in metalanguage) you can prove $$\text{there is no } a\in A \text{ s.t. }M\nvDash \alpha [s[x|a]]\iff \text{there is }a\in A \text{ s.t. } M\vDash \alpha[s[x|a]].$$

---

Oh, I make a mistake. Formalize the proof of given statement then $$ \begin{aligned} M\models (\exists x)(\alpha)[s] &\iff & M\models \lnot(\forall x)\lnot(\alpha)[s] &\qquad(1)\\ & \iff &\text{not}(M\models (\forall x)\lnot(\alpha)[s]) &\qquad(2)\\ & \iff &\text{not}(\text{for all }a\in A,\>\> M\models \lnot(\alpha)[s[x|a]]) &\qquad(3)\\ \end{aligned} $$

Can you find what step in your 'proof' makes the trouble?