What does it mean for a variable to be free for something? "If $\mathscr{B}$ is a wf and $t$ is a term, then $t$ is said to be free for $x_i$ in $\mathscr{B}$ if no free occurrence of $x_i$ in $\mathscr{B}$  lies within the scope of any quantifier $(\forall x_j)$, where $x_j$ is a variable in $t$." 
This is how Mendelson defines the expression 'free for $x_i$ in $\mathscr{B}$'. He goes on to say that it means that, if $t$ is substituted for all free occurrences (if any) of
$x_i$ in $\mathscr{B}(x_i)$, no occurrence of a variable in $t$ becomes a bound occurrence in $\mathscr{B}(t)$'. 
I still can't understand what 'free for' means. Could anyone provide examples along with explanations? 
Mendelson also distinguishes between 'free for', 'free' and 'free occurrence', distinctions that I haven't yet fully grasped.
 A: We have formulas $\phi(x)$ with free occurrences of $x$, like e.g. $x=0$.
If we put a quantifier in front, what we get is $\forall x \phi(x)$. The formula $\phi(x)$ will be the scope of the leading quantifier and all occurrences of $x$ in $\phi(x)$ will be bound, because they are in the scope of the quantifier.
We can formalize it through an "operator" $\text {FV}$ that takes in input a formula $\phi$ and gives as output the set of free variables of the formula (see van Dalen, page 62):

if $\phi$ is an atomic formula, like e.g. $x=0$, all variables in $\phi$ are free (in our example, $\text {FV}(x=0)= \{ x \}$).

Things are smooth for formulas with propositional connectives; the only interesting cases are those with quantifiers:

$\text {FV}(∃yψ)=\text {FV}(∀yψ)=\text {FV}(ψ) \setminus \{ y \}$.


The locution “$t$ is free for $x$ in $ϕ$” (where $t$ is a term, $x$ a variable and $\phi$ a formula) comes down to the fact that the (obviously free) variables of $t$ are not going to be bound after substitution in $ϕ$.
Thus, to be "free for" must ensure that a proper substitution is performed, producing a "correct" result $ϕ[t/x]$.
In order to do this, we need a formal defintion:

$t$ is free for $x$ in $ϕ$ if

(i) $ϕ$ is atomic;
(ii) $ϕ$ is $ϕ_1 \lor ϕ_2$ (or is $ϕ_1 \land ϕ_2$, or is $¬ϕ_1$) and $t$ is free for $x$ in $ϕ_1$ and $ϕ_2$;
(iii) $ϕ$ is $∃yψ$ (or $∀yψ$) and if $x ∈ \text{FV}(ϕ)$, then $y \notin \text{FV}(t)$ and $t$ is free for $x$ in $ψ$.



Consider now the simple example of a formula $\phi$:

$\exists y (y+x = 0)$,

and consider as $t$ the term: $y+1$.
The substitution $\phi[t/x]$ will produce:

$\exists y (y+y+1 = 0)$,

that is clearly wrong: $0$ is not the successor of any number.
What has gone wrong ? The fact that $t$ is not free for $x$ in $\phi$.
Why so ? Because we have violated the part (iii) of the above definition: $x \in \text {FV}(\phi)$ but $y \in \text {FV}(t)$, and thus the free occurrence of $y$ in $t$ has been "captured" by the leading quantifier.
Consider now this example in light of Mendelson's definition:

"If $\mathscr{B}$ is a wf and $t$ is a term, then $t$ is said to be free for $x_i$ in $\mathscr{B}$ if no free occurrence of $x_i$ in $\mathscr{B}$  lies within the scope of any quantifier $(\forall x_j)$ [or $(\exists x_j)$], where $x_j$ is a variable in $t$." 

And rewrite our formula as: $\exists x_j (x_j + x_i = 0)$; now the term $t$ is $x_j+1$.
We want to replace $x_i$ with $t$ into $\mathscr{B}$: unfortunately we cannot do it, because $t$ is not free for $x_i$.
In fact we have that the only free occurrence of $x_i$ in $\mathscr{B}$ lies within the scope of a quantifier $\exists x_j$, where $x_j$ is a variable in $t$.
