Definition:
$\varphi$ a formula, $t$ a term. We say "$t$ is free for $x_i$ in $\varphi$ if no free occurence of $x_i$ in $\varphi$ lies within the scope of $\forall x_j$ where $x_j$ is a variable appearing in $t$
I somehow couldn't understand this definition fully.
Can anyone help me with this by an example:
Let $f(x_1, x_2)$ be a term in a first order language $L$; call this term $t$. Decide if $t$ is free for $x_1$ in the following formula of $L$:
$R(x_1, x_2) \rightarrow (\forall x_2)S(x_2)$
I think $t$ is free for $x_1$ here, because the occurrence of $x_1$ does not lie in the scope of any quantifier of the form $\exists x_j$ or $\forall x_j$
Am I right?
You are correct, although you should say that the occurrence of $x_1$ only occurs in the scope of quantifiers $\forall x_j$ where $j \neq 1$.
I have always found this terminology a bit counter-intuitive, but the idea is that "$t$ is free for $x_i$ in $\phi$" means that you can simply replace each free occurrence of $x_i$ in $\phi$ by $t$ and get a new formula that "says the same thing about $t$ as $\phi$ said about $x_i$". This means that no free variable $x_j$ of $t$ is allowed to be "captured" by a quantifier in $\phi$.
For example, if $t$ is $x_1 + x_2$ and $\phi$ is $$(\forall x_2(x_3 \ge x_2)) \lor (\forall x_4(x_5 \ge x_4)$$ $t$ is not free for $x_3$ in $\phi$, but $t$ is free for $x_5$ in $\phi$. If you replace $x_3$ by $t$, you get:
$$(\forall x_2(x_1 + x_2 \ge x_2)) \lor (\forall x_4(x_5 \ge x_4)$$
which (over the natural numbers) is true, while $\phi$ is false for any values of its free variables $x_3$ and $x_5$. So the replacement isn't making the same statement about $t$ as $\phi$ makes about $x_3$. However, if you replace $x_5$ by $t$, you get
$$(\forall x_2(x_3 \ge x_2)) \lor (\forall x_4(x_1 + x_2 \ge x_4)$$
which is making the same (false) statement about $t$ that $\phi$ makes about $x_5$.