Am I using this particular definition of a free variable correctly to identify a free variable?

Question

The definition:

We use this definition for a free variable.

Suppose that $v$ is a variable and $\phi$ is a formula. We will say that $v$ is free in $\phi$ if:

1. $\phi$ is atomic and $v$ occurs in (is a symbol in) $\phi$, or
2. $\phi := (\lnot \alpha)$ and $v$ is free in $\alpha$, or
3. $\phi :=$ $(\alpha \lor \beta)$ and $v$ is free in at least one of $\beta$ or $\alpha$, or
4. $\phi :=$ $(\forall u)(\alpha)$ and $v$ is not $u$ and $v$ is free in $\alpha$.

The formula:

Now, the task is to explain, using the definition above, how $v_2$ is a free variable in the formula below: $$\phi = (\forall v_1)(\lnot(\forall v_5) (v_2 = v_1 + v_5))$$

The answer:

We say that $v_2$ is a free variable in the $\phi$ above since first, our $\phi$ matches clause $(4)$ of the definition, where $(\forall u) = (\forall v_1)$ and $(\alpha) = (\lnot(\forall v_5) (v_2 = v_1 + v_5))$, which tells us that $v_1$ is not a free variable in this expression. We then take to looking for a free variable in $(\alpha) = (\lnot(\forall v_5) (v_2 = v_1 + v_5))$ as per the definition.

So, we define $\phi$ recursively by replacing the value of $\alpha$:

$$\phi = \lnot(\forall v_5) (v_2 = v_1 + v_5)$$

Further, we try to find a free variable in $\phi= \lnot(\forall v_5) (v_2 = v_1 + v_5)$, and realize that it matches clause $(2)$ of the definition provided to us such that $\phi = \lnot(\forall v_5) (v_2 = v_1 + v_5)$, where $\alpha = (\forall v_5) (v_2 = v_1 + v_5)$. We then take to looking for a free variable in $\alpha = (\forall v_5) (v_2 = v_1 + v_5)$ as per the definition.

So, we define $\phi$ recursively by replacing the value of $\alpha$:

$$\phi = (\forall v_5) (v_2 = v_1 + v_5)$$

Finally, when we have $\phi = (\forall v_5) (v_2 = v_1 + v_5)$, it recursively matches clause $(4)$ of the definition such that $(\forall u) (\alpha) = (\forall v_5) (v_2 = v_1 + v_5)$, which tells us that per the definition, $v_5$ not the free variable, and that it must be in $(v_2 = v_1 + v_5)$. We then take to looking for a free variable in $(v_2 = v_1 + v_5)$ as per the definition. So, we define $\phi$ recursively by replacing the value of $\alpha$:

$$\phi = (v_2 = v_1 + v_5)$$

Conclusively, we identify that within $(v_2 = v_1 + v_5)$ as $\phi$ and hitting clause $(1)$ of our definition, it is $v_2$ that occurs in $\phi$, and since $\phi$ as $(v_2 = v_1 + v_5)$ is atomic, it must be that $v_2$ is the free variable in $\phi$.

Answer 1

Why not answer the question directly? It only asks whether $v_2$ is free, it doesn't ask you to identify all the free variables.

I would write no more than this:

$v_2$ is free in $$ v_2 = v_1 + v_5$$ by clause (1).

Hence $v_2$ is free in $$(\forall v_5) (v_2 = v_1 + v_5)$$ by clause (4).

Hence $v_2$ is free in $$\phi = (\lnot(\forall v_5) (v_2 = v_1 + v_5))$$ by clause (2).

Hence $v_2$ is free in $$\phi = (\forall v_1)((\lnot(\forall v_5) (v_2 = v_1 + v_5)))$$ by clause (4).

[I have repaired the bracketing to match the bracketing used by the rules.]