Assume the following predicate definition is true: $N(x)$: $x$ is a natural number.
Which occurrences of the underlined variables $x$ and $y$ are free and which are bound in each of the following?
$a)$ $\underline x = 2 * \underline y$
$b)$ $\forall x (N(x) \rightarrow \exists y(N(y) \rightarrow \underline y > \underline x) \wedge \underline x = 2 * \underline y)$
My thoughts: I am very confused in both these problems. Especially, in part $b)$, it is very hard for me to decide whether variable $x$ is free or not (first $y$ is bound, second $y$ is most probably free, though). Would appreciate to hear your ideas about it.
Intuitively, given a formula of the form $\forall x (\dots)$ or $\exists x (\dots)$, consider only the dots: each free occurrence of $x$ inside the dots is bound to the quantifier $\forall x$ or $\exists x$, respectively; we then say that such an occurrence of $x$ is in the scope of that quantifier. $%by the quantifier \forall x or \exists x, respectively; $ While each occurrence of the variable $x$ outside the dots (suppose that $\forall x (\dots)$ or $\exists x (\dots)$ is a subformula plugged into a bigger formula) is not bound to that quantifier $\forall x$ or $\exists x$, but it can be possibly bound to other quantifiers, if any.
Note that in a formula $\forall x (\dots)$ or $\exists x (\dots)$, the quantifier $\forall x$ or $\exists x$ binds the free occurrences of $x$ in the dots, but it does not bind the free occurrences of other variables ($y, z, \dots$).
Coming to your questions:
a) Since there are no quantifiers, all the occurrences of $x$ of $y$ are free in this formula.
b) Since the formula has the form $\forall x (\dots)$, each occurrence of $x$ in this formula is bound. The dots in $\forall x (\dots)$ have the form $N(x) \to \exists y (\dots) \land x = 2 \cdot y$, hence the two occurrences of $y$ inside the dots in $\exists y (\dots)$ are bound, while the occurrence of $y$ in $x = 2 \cdot y$ is free, because it is outside the scope of any quantifier binding $y$.
Note that the same variable might have some free occurrences and some bound occurrences in the same formula. This is the case of $y$ in formula b).