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


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


can somebody tell me if i misunderstand it or not. thanks


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.