First Order Logic

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.

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.