First Order Logic

Syntax

Let us first introduce the symbols, or alphabet, being used. Beware that there are all sorts

of slightly different ways to define FOL.

Alphabet

• Logical Symbols: These are symbols that have a standard meaning, like: AND,

OR, NOT, ALL, EXISTS, IMPLIES, IFF, FALSE, =.

• Non-Logical Symbols: divided in:

o Constants:

  Predicates: 1-ary, 2-ary, .., n-ary. These are usually just identifiers.

  Functions: 0-ary, 1-ary, 2-ary, .., n-ary. These are usually just

identifiers. 0-ary functions are also called individual constants.

Where predicates return true or false, functions can return any value.

o Variables: Usually an identifier.

One needs to be able to distinguish the identifiers used for predicates, functions,

and variables by using some appropriate convention, for example, capitals for

function and predicate symbols and lower cases for variables.

Terms

A Term is either an individual constant (a 0-ary function), or a variable, or an n-ary

function applied to n terms: F(t1 t2 ..tn)

[We will use both the notation F(t1 t2 ..tn) and the notation (F t1 t2 .. tn)]

Clauses

A Clause is a disjunction of literals. A Ground Clause is a variable-free clause. A Horn

Clause is a clause with at most one positive literal. A Definite Clause is a Horn Clause

with exactly one positive Literal.

Notice that implications are equivalent to Horn or Definite clauses:

(A IMPLIES B) is equivalent to ( (NOT A) OR B)

(A AND B IMPLIES FALSE) is equivalent to ((NOT A) OR (NOT B)).

Formulae

A Formula is either:

• an atomic formula, or

• a Negation, i.e. the NOT of a formula, or

• a Conjunctive Formula, i.e. the AND of formulae, or

• a Disjunctive Formula, i.e. the OR of formulae, or

• an Implication, that is a formula of the form (formula1 IMPLIES formula2), or

• an Equivalence, that is a formula of the form (formula1 IFF formula2), or

• a Universally Quantified Formula, that is a formula of the form (ALL variable

formula). We say that occurrences of variable are bound in formula [we should

be more precise]. Or

• a Existentially Quantified Formula, that is a formula of the form (EXISTS

variable formula). We say that occurrences of variable are bound in formula [we

should be more precise].

An occurrence of a variable in a formula that is not bound, is said to be free.

A formula where all occurrences of variables are bound is called a closed formula, one

where all variables are free is called an open formula.

A formula that is the disjunction of clauses is said to be in Clausal Form. We shall see

that there is a sense in which every formula is equivalent to a clausal form.

Often it is convenient to refer to terms and formulae with a single name. Form or

Expression is used to this end.

Substitutions

• Given a term s, the result [substitution instance] of substituting a term t in s

for a variable x, s[t/x], is:

o t, if s is the variable x

o y, if s is the variable y different from x

o F(s1[t/x] s2[t/x] .. sn[t/x]), if s is F(s1 s2 .. sn).

Version 1 CSE IIT, Kharagpur

• Given a formula A, the result (substitution instance) of substituting a term t in

A for a variable x, A[t/x], is:

o FALSE, if A is FALSE,

o P(t1[t/x] t2[t/x] .. tn[t/x]), if A is P(t1 t2 .. tn),

o (B[t/x] AND C[t/x]) if A is (B AND C), and similarly for the other

connectives,

o (ALL x B) if A is (ALL x B), (similarly for EXISTS),

o (ALL y B[t/x]), if A is (ALL y B) and y is different from x (similarly for

EXISTS).

The substitution [t/x] can be seen as a map from terms to terms and from formulae to

formulae. We can define similarly [t1/x1 t2/x2 .. tn/xn], where t1 t2 .. tn are terms and x1

x2 .. xn are variables, as a map, the [simultaneous] substitution of x1 by t1, x2 by t2, ..,

of xn by tn. [If all the terms t1 .. tn are variables, the substitution is called an alphabetic

variant, and if they are ground terms, it is called a ground substitution.] Note that a

simultaneous substitution is not the same as a sequential substitution.