First we introduce the grammar of predicate logic. We have the notion of terms, these are variables, constants and functions. That is
Nothing else is a term.
We can now turn our attention to formulas. We have that
Nothing else is a formula. Again a predicate symbol of arity 0 is the same as a propositional atom. However we do not concern our self with these in this grammar. Note that the arguments of a predicate needs be a term. Hence this logic is of first order. If we allow formulas as arguments, the order is higher. We have that $\forall$ and $\exists$ binds as tight as $\neg$. The rest is as for propositional logic. That is
The notion of free and bound variables is closely related to that of a scope. We can visualize the idea by drawing parse trees. However I'm somewhat reluctant to do this. The quantifiers $\forall$ and $\exists$ goes into a single branch in the tree. A predicate $P(t_1,t_2,\dots,t_n)$ goes into $n$ branches. If we from any of these terms, $t_i$, can walk up the tree and reach a quantifier that uses this given term, for example $\forall t_i$, then $t_i$ is said to be bound. Otherwise $t_i$ is said to be free. The scope of a quantifier is just the subtree for which this quantifier is the root.
We mark the scope with parentheses, for example $$ (\forall x . P(x) \land Q(x)) \lor \neg P(x) $$ Here $x$ is in the scope of the forall quantifier for $P,Q$. However $x$ in the formula $\neg P(x)$ is free.
We often want to substitute a free variable with a term. This term can be of any complexity, for example a function that takes other terms as arguments.
Given a formula $\phi$, a term $t$ and a variable $x$, we define $\phi[t/x]$ to be the formula obtained by replacing each free occurrence of $x$ with $t$.
The notion $\phi[t/x]$ is not part of the grammar (and hence not part of the language), however $\phi$ with all free occurrences of $x$ replaced with $t$ is part of the grammar.
Again exemplifying this notion requires drawings of parse trees. Which I'm not doing right now :-).
Problems can arise when substituting. Say we have the term $t = f(y,y)$. Since $t$ is a term, it cannot contain a quantifier, hence $y$ is free. Say we do $(\exists y . P(x) \lor P(y))[t/x]$. The result is $(\exists y . P(f(y,y)) \lor P(y))$. But now the term $y$ in $f(y,y)$ is bound by the quantifier $\exists$. To deal with this we introduce the definition of being free for.
Let $t$ be a term, $x$ be a variable and $\phi$ a formula. We say that $t$ is free for $x$ in $\phi$ if no variable $y$ in $t$ will be bound by a quantifier after substituting $x$ with $t$ in $\phi$. That is after $\phi[t/x]$.