Show that $(\forall v_1)\neg(\forall v_2)\neg (v_1 = v_2+v_2)$ is false in $\mathfrak{N}$.

Question

I am self studying 'A Friendly Introduction to Mathematical Logic' by Christopher C. Leary and am struggling to follow Example 1.7.10 which I have simplified as follows:

Let $\mathcal{L}$ be the language $\{+\}$, let $\mathfrak{N}=\langle \mathbb{N}, + \rangle$ be a structure where $+$ is addition of natural numbers, let $s:\text{Vars} \to \mathbb{N}$ be a variable assignment function and let $$\sigma :\equiv (\forall v_1)\neg(\forall v_2)\neg (v_1 = v_2+v_2)$$ be a sentence of $\mathcal{L}$. Then \begin{align} \mathfrak{N} \models \sigma[s] &\iff \text{For every } a \in \mathbb{N}, \mathfrak{N} \models \neg(\forall v_2)\neg (v_1 = v_2+v_2)s[v_1 | a]\\\\ &\iff \text{For every } a \in \mathbb{N}, \mathfrak{N} \not\models (\forall v_2)\neg (v_1 = v_2+v_2)s[v_1 | a]\\\\ &\iff \text{For every } a \in \mathbb{N} \text{ there is a } b \in \mathbb{N}, \mathfrak{N} \models v_1 = v_2+v_2s[v_1 | a][v_2|b]. \end{align}

If we consider the case when $a$ is the number $3$, it is clear that there is no such $b$, so we have shown $\mathfrak{N} \not\models\sigma[s].$ Thus, $\mathfrak{N} \not\models\sigma$. (End of Proof)

The step that I do not understand is how we get from $$\text{For every } a \in \mathbb{N}, \mathfrak{N} \not\models (\forall v_2)\neg (v_1 = v_2+v_2)s[v_1 | a]$$ to $$\text{For every } a \in \mathbb{N} \text{ there is a } b \in \mathbb{N}, \mathfrak{N} \models v_1 = v_2+v_2s[v_1 | a][v_2|b].$$

My attempt is:

\begin{align} \mathfrak{N} \models \sigma[s] &\iff \text{For every } a \in \mathbb{N}, \mathfrak{N} \models \neg(\forall v_2)\neg (v_1 = v_2+v_2)s[v_1 | a]\\\\ &\iff \text{For every } a \in \mathbb{N}, \mathfrak{N} \not\models (\forall v_2)\neg (v_1 = v_2+v_2)s[v_1 | a]\\\\ &\iff \text{For every } a \in \mathbb{N}, \text{ for every } b \in \mathbb{N}, \mathfrak{N} \not\models \neg(v_1 = v_2+v_2)s[v_1 | a][v_2|b]. \end{align}

... and I don't know where to go next. Can I remove the negation symbol that remains and in turn change the $\not\models$ to a $\models$? It would appear that I don't know how to handle multiple instances of the universal quantifier in one sentence. How does the proof come to only requiring that there exist a $b$ instead of requiring that it be true for all $b$. Has the proof given in the book missed out some steps, if so, could someone please let me know what they are?

The following relevant definitions are given in the book:

1. $\mathfrak{A} \models(\neg \alpha)[s] \iff \mathfrak{A} \not\models(\alpha)[s]$

2. $\mathfrak{A} \models(\forall x)(\alpha) \iff \text{ for each element } a \text{ of } A, \mathfrak{A}\models \alpha[s(x|a)].$

Answer 1

In order to be formal, we have to go back to Definition 1.7.4 (page 29 in 2nd edition, 2015).

We have that:

$\text{For every } a \in \mathbb N, \ \ \mathfrak N \not \models (\forall v_2)\neg (v_1 = v_2+v_2)s[v_1 | a]$

and we have to apply clause 5. of the definition, the one regarding the universal quantifier.

It reads (applied to the example): "for each element $a$ of $\mathbb{N}, \ \ \mathfrak{N} \models \alpha [s(v_2|a)]$".

In a nutshell, this means that if we can consider an object $a$ whatever and assign it to variable $v_2$, the "property" expressed by formula $\alpha$ will hold for $a$.

What does it mean that $\vDash$ does not hold? i.e. that $\nvDash$?

We have to consider the denial of the previous clause, i.e. we can find some object $b$ such that the "property" expressed by formula $\alpha$ will not hold for it.

Formally: "for some element $b$ of $\mathbb N, \ \ \mathfrak N \not \models \alpha [s(v_2|b)]$".

Thus, going back to the example:

$\text{For every } a \in \mathbb{N}, \text{ there is a } b \in \mathbb{N}, \ \ \mathfrak{N} \not \models \lnot (v_1 = v_2+v_2s[v_1 | a][v_2|b]).$

Using again clause 3. of the definition (regarding negation):

$\text{For every } a \in \mathbb{N}, \text{ there is a } b \in \mathbb{N}, \ \ \mathfrak{N} \models (v_1 = v_2+v_2s[v_1 | a][v_2|b]).$