1) Yes : $P(x,y)$ is a predicate formula; we can have a lot of it, according to the first-order language we choose.
If we choose the language of arithmetic, with e.g the predicate symbols = and < and the (individual) constant $0$, we can build the formulae :
$x = x$, $x < y$, $x = 0$, $0 < x$, and so on.
As you correctly say, a formula $\mathcal A(x)$ with a free variable $x$ inside has no meaning per se.
In order to "give meaning" to it, we have to choose an interpretation (this is semantics), i.e. we have to select o domain $D$ for the variables.
Now, we consider an instance of it : $\mathcal A[x/a]$, i.e.the formula (without free vars) obtained from $\mathcal A(x)$ by substitution of all occurrences of $x$ with $a$, where $a$ is a constant (a "name" for an object of the domain).
Now the formula $\mathcal A[x/a]$ is a sentence (i.e. a formula without free vars, called also a closed formula), and we are able to "evaluate" its truth-value.
Consider the formula of your example, with $P(x,y)$ as $<(x,y)$, that we abbreviate (as usual) as
$x < y$.
If we substitute to $x$ the (name for the) number $3$, and to $y$ the number $4$, we obtain a true sentence (i.e. $3 < 4$).
If instead we substitute to $x$ the (name for the) number $5$, we obtain a false sentence (i.e. $5 < 4$).
2) I would say : "because in mathematics we are interested into infinite structures", we are not able to "check" in a combinatory way (like truth-tables for propositional logic) for truth (and validity) of formulae.
Thus we need some way to "prove" if a formula is true in a structure :
with a proof in a logic calculus or proof system : Hilbert-style, Natural Deduction, Sequent Calculus, Tableaux method
with "insight" : like $\forall x (x = x)$; we know it is true in every domain (and thus it is valid) only "by inspection"
with some "computer assisted" method (see Automated theorem proving).
3) The resolution method is base on Herbrand's theorem (see your book) and some computer program for "checking" f-o formulae are based on Tableaux method; see :
4) Yes: the resolution method apply Herbrand's theorem to build a particular type of interpretation and it allows us to check only one structure in order to verify if the formula is unsatisfiable.
Due to algorithmically undecidability of first-order logic, this method may prove the satisfiability of a first-order satisfiable formula, but not always, as it is the case for all methods for first-order logic.