About the predicate logic(first order logic) symbol i'm currently study the f-o logic.
i just want to make sure i dont get the idea wrong.
here is what i have learned:
P(X,Y) is a predicate formula.
the  P(X,Y) itself mean nothing unless you give it a structure(i.e semantics)
all predicate formula can have infinite structure.
you can give it any domain as its ground set(e.g N:natural number,Z=integer,or even 
{1,2,3}...
also you give it any interpretation to its function symbols, predicate symbols, and also 
the free variable.
for example, you can interpret P(X,Y) as X>Y, X>Y+1, X>Y+2,X is on the right side of 
Y...
because of the infinite structures, we can't not check the formula's value under all 
structures. so we have to apply the herbrand theory to reduce the size of the set of the 
structures and to see if the formula is unsatisfiable or valid (so called semi 
decidability).
can somebody tell me if i misunderstand it or not.
thanks
 A: 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 : 


*

*Raymond Smullyan, First-Order Logic (1968 - Dover reprint), 

*Melvin Fitting, First-Order Logic and Automated Theorem Proving (1990), 

*Peter Smith, An Introduction to Formal Logic (2003).
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.
