Which variables are free in $\forall x (\exists y (x < y+z) \to \exists z (x < y+z))$? anyone could explain for me, why $x,y,z$ is bound variable in this formula?
$ \forall x [ \exists y (x < y+z) \to \exists z (x < y+z) ] $
I think $y,z$ is free variable. 
 A: the same var may have both free and bound occurrences in the same formula. 
A quantifier bounds the var that follows it, within the scope of that quantifier. 
So, $x$ is bound by the starting $\forall x$, in the entire formula. 
The first and second occurrence of $y$ (before the $\to$ sign) are bound.
The last occurrence of $y$ is free (it is not within the scope of $\exists y)$. 
The first occurrence of $z$ is free, the second and the third are bound by the 
$\exists z$. 
A: You are right.
We can use the recursive definition of the set $FV(\varphi)$ of free variables of a formula $\varphi$.
See Dirk van Dalen, Logic and Structure (5th ed - 2013), page 59 :

Definition The set $FV(\varphi)$ of free variables of $\varphi$ is defined by

(i) if $\varphi$ is an atomic formula $P(x_1, \ldots, x_n)$, then $FV(\varphi)= \{ x_1, \ldots, x_n \}$;
(ii) if $\varphi$ is an atomic formula $x_1 = x_2$, then $FV(\varphi)= \{ x_1, x_2 \}$;
(iii) $FV(\varphi \to \psi) = FV(\varphi) \cup FV(\psi)$;
(iv) $FV(¬ \varphi) = FV(\varphi)$;
(v) $FV(∀x_i \varphi) = FV(∃x_i \varphi) = FV(\varphi) − \{ x_i \}$.


We can apply the above definition to "compute" $FV$ for your formula :


*

*$FV(x<y+z) = \{ x,y,z \}$

*$FV(∃y(x<y+z)) = \{ x,y,z \} - \{ y \} = \{ x,z \}$
In the same way :


*

*$FV(∃z(x<y+z)) = \{ x,y \}$


and thus :


*

*$FV(∃y(x<y+z)→∃z(x<y+z))= \{ x,z \} \cup \{ x,y \} = \{ x,y,z \}$.


Finally :

$$FV(∀x[∃y(x<y+z)→∃z(x<y+z)]) = $$
$$= \{ x,y,z \} - \{ x \} = \{ y,z \}.$$

