This is sometimes called predicate calculus. Unitl now, we could have these totally correct interpretations:
Note that the dot between 
and 
means that the universal quantifier applies to what comes after the dot, i.e. the whole formula. It is alternative to using the parenthesis.
We notice that different interpretations can lead to totally different meanings! We now want to understand which is the meaning of a formula written in FOL. The presence of variables makes this a little bit more different than propositional logic. We need to fix a universe (a domain from which we take the values, like numbers, graphs, apples...), an interpretation of function and predicate symbols (if I take a predicate, what is the meaning of this predicate? We have to fix a meaning for any predicate symbol) and a valuation for variables (a variable needs to have a fixed value).
Now, formalizing these concepts, an interpretation 
of 
(which is a signature, i.e. set of functions+set of symbols) consists of:
- A universe
, a non empty set - A function
, for every n-ary function symbol 
of - A relation
for every n-ary predicate symbol 
of
Once we have defined an interpretation, how can we interpret a term? We simply apply in a recursive way the definition of interpretation.
Our goal is being able to say, formally, when a formula is true or false.
Given interpretation of , 
variable valuation, 
which means that it satisfies 
, is defined as follows:
We want to define, for example, when 
, we need to know the meaning of the terms, for example 
, then we need to check if these values belong to the interpretation: 
?.
Given a signature , an interpretation , and a formula 
, we say that:
model of 
or satisfies (written 
) when 
for every possible valuation 
- is a model of theory
when is a model of each formula in
A sentence S can be valid (
for every ), falsifiable ( for some ), satisfiable(
for some ), unsatisfiable ( for every ).
These are provided without proof, we trust those. The notion of logical consequence is the same we always see. A sentence/theory 
is a logical consequence of a sentence/theory 
if every model of is also a model of , i.e. 
implies 
.
Two sentences/theories are equivalent 
if they are logical consequences of each other. Given that, it is undecidable whether a FOL formula is true under all possible interpretations, i.e. 
. We cannot list all the possible cases through the truthness table anymore, as we could do in propositional logic. In fact, we should now consider all possible universes of interpretations, domains... and this can't be done.
The idea is the same as for propositional logic: we take a theory, we negate the consequence that we want to prove, and we must show that this theory is unsatisfied. However, we have to transform FOL formulae in clauses, which is more complicated. Then we must define the resolution inference rule for FOL, which requires substitutions and unification.
In Negation Normal Form, if you have a negation, then the negation is in front of an atomic formula. So, for every sentence , there is an equivalent sentence 
in the NNF.
A clause is a disjunction of literals(i.e. either an atomic formula or a negation of one). The part on the left of the arrow is called the body, the head is the part on the right.
An arbitrary theory can be transformed into clausual form by converting to NNF, performing Skolemization (preserves satisfiability) to eliminate all the existential quantifiers, then convert the resulting theory, still in NNF, to clausal form, by moving conjunctions and universal quantifiers outwards.
The substitution is something you may already have seen in functional languages. It is simply a mapping to a function which has the domain 
set of all variables, codomain 
all the possible terms, modifying a finite number of variables in the sense that it replaces the finite number of variables by a finite number of terms.
is a unifier for 
if 
is unifiable if a unifier exists. The most general unifier (mgu) exists if every unifier 
for 
is instance of , i.e. 
for some 