Clarification for the definition of "a term is free for a variable in some wf. of a first order language"

Question

Definition 1 Let $A$ be any wf. of a first order language L and $x$ be any variable. We say $x$ occurs free in $A$ if there is at least one occurrence of $x$ in $A$ which is not the scope of $(\forall x)$.

Definition 2 Let $A$ be any wf. of a first order language L. A term $t$ is free for $x$ in $A$, if $x$ does not occur free in $A$ within the scope of a $(\forall y)$, where $y$ is any variable occurring in $t$.

I feel quite confused about the second definition. I was wondering if there's no $(\forall y)$ occurring in $A$, then how does the definition work?

In the textbook, there's an example, say, "the term $f_1^2(x_1,x_3)$ is free for $x_1$ in $(\forall x_2)A_1^2(x_1,x_2)\Rightarrow A_1^1(x_1)$ but is not free for $x_1$ in $(\forall x_3)(\forall x_2)A_1^2(x_1,x_2)\Rightarrow A_1^1(x_1).$"

For the first part, there is no $(\forall x_1)$ or $(\forall x_3)$ occurring in the wf. $(\forall x_2)A_1^2(x_1,x_2)\Rightarrow A_1^1(x_1)$. (Here $x_1$ occurs free in the wf.) So, for the definition, if there's no $(\forall y)$ in the wf. $A$, where $y$ is any variable occurring in $t$, then "$t$ is free for $x$ in $A$" automatically true? But this rule does not work for the second part of the example.

I can understand that the results of this example are reasonable, since the aim of the second definition is that $t$ may be substituted for every free occurrence of $x$ in $A$ without introducing any interactions with quantifiers in $A$. But I am really confused about how to use this definition.

Could you help me clarify this definition? Thank you so much!

Answer 1

If there is no $(\forall y)$ in the formula, then in particular there is no free $x$ within the scope of such a $(\forall y)$, so the condition is vacuously satisfied.

The textual definition of "free for $x$" is not very carefully worded with respect the use of "a" and "any". What is meant, in pseudo-formal notation, is something like:

Let $A$ be any wf. A term $t$ is free for $x$ in $A$, iff

($\forall$variable "$y$" free in $t$) ($\forall$quantifier "$(\forall y)$" in $A$) $\neg$ ($\exists$appearance of $x$ free in $A$) this "$x$" is in the scope of the "$(\forall y)$").

An universal quantification over an empty set is always true, so if there is no $(\forall y)$ in $A$, then the condition "($\forall$quantifier "$(\forall y)$" in $A$)" is automatically satisfied, without even looking at $x$s.