Clarification for the definition of "a term is free for a variable in some wf. of a first order language" 
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!
 A: 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.
A: In your examples regarding substitutability [from Elliott Mendelson, Introduction to mathematical logic (4ed - 1997), Example 2, page 54], we have that :

"the term $f^2_1(x_1,x_3)$ is free for $x_1$ in $(∀x_2)A^2_1(x_1,x_2) ⇒ A^1_1(x_1)$
but is not free for $x_1$ in $(∀x_3)(∀x_2)A^2_1(x_1,x_2) ⇒ A^1_1(x_1)$."

As you says correctly, for the first part, there is no $(∀x_1)$ or $(∀x_3)$ occurring in the formula; thus, there is no possibility that the free occurrences of $x_1$ and $x_3$ in the term $f^2_1(x_1,x_3)$ are "captured" by a quantifier with the substitution, altering the "menaing" of the formula.
Why the substitution is not allowed with :

$(∀x_3)(∀x_2)A^2_1(x_1,x_2) ⇒ A^1_1(x_1)$ ?

Because in this case the free occurrence of $x_3$ in the term $f^2_1(x_1,x_3)$, after substitution, would be "captured" by the quantifier $(∀x_3)$.
The resulting formula would be :

$(∀x_3)(∀x_2)A^2_1(f^2_1(x_1,x_3),x_2) ⇒ A^1_1(x_1)$

generating a "constraint" on the term which is unwanted.
To see what happens without the above restriction, consider as interpretation of our language the set $\mathbb N$ of natural numbers and consider the simple formula [here $\le$ is a binary predicate which takes the place of $A^2_1$] :

$\exists x (x \le y)$.

This formula is always true in $\mathbb N$; if we substitute $y$ with $0, 1, 2, \ldots$ we obtain the formulae :

$\exists x (x \le 0), \exists x (x \le 1), \exists x (x \le 2), \ldots$

which are all satisfied for $x=0$.
Consider now a term $S(x)$ of our language, where $S$ is the function "successor" (thus: $S(x)$ is $x+1$).
Again, if we substitute $S(x)$ in place of $y$ - in spite of the restriction - we get :

$\exists x (x \le S(x))$,

which is still true in $\mathbb N$ [to be precise, it is true for all values of $x$].
But try now with the formula :

$\exists x (x = y)$.

Again, if we substitute $y$ with $0, 1, 2, \ldots$ we obtain the formulae :

$\exists x (x = 0), \exists x (x = 1), \ldots$

which are still satisfiable in $\mathbb N$ : we can always find a "suitable" value for $x$.
What happens now with the "illegal" substitution of $S(x)$ in place of $y$ (recall that $S(x)$ "means" $x+1$) ? We get :


$\exists x (x = S(x))$


which is clearly unsatisfiable in $\mathbb N$.
This is the 'intuition' behind the restriction regarding substitution ...
