**Home** / **first order logic proof calculator** / Normal Forms for First-Order Logic - Department of …

Logic and Proof Hilary 2016

Normal Forms for First-Order Logic

James Worrell

In this lecture we show how to transform an arbitrary formula of first-order logic to an equisat-

isfiable formula in Skolem form. This translation is in preparation for our subsequent treatment of

deduction using unification and resolution.

1 Equivalence and Substitution

Two first-order formulas F and G over a signature are logically equivalent, denoted F G, if for

all -assignments A we have A |= F iff A |= G.

All the propositional equivalences carry over to the first-order setting, e.g., we still have De

Morgan's law ?(F G) (?F ?G), etc. Moreover logical equivalence remains a congruence with

respect to the Boolean connectives , and ?, that is, (F1 G1) (F2 G2) if F1 G1 and

F2 G2, etc. In addition we have that that if F G then x F x G and x F x G.

The following equivalences will play an important role in transforming formulas into Skolem

form.

Proposition 1. Let F and G be arbitrary formulas. Then

(A) ?xF x?F

?xF x?F

(B) If x does not occur free in G then:

(xF G) x(F G)

(xF G) x(F G)

(xF G) x(F G)

(xF G) x(F G)

(C) (xF xG) x(F G)

(xF xG) x(F G)

(D) xyF yxF

xyF yxF

Proof. As an example, we prove the first equivalences in (A) and (B). For the former we have

A |= ?xF iff A |= xF

iff A[xa] |= F for some a UA

iff A[xa] |= ?F for some a UA

iff A |= x?F

1

For the first equivalence in (B) we have

A |= (xF G) iff A |= xF and A |= G

iff for all a UA, A[xa] |= F and A |= G

iff for all a UA, A[xa] |= F and A[xa] |= G (by the Relevance Lemma)

iff for all a UA, A[xa] |= F G

iff A |= x(F G) .

A formula is in prenex form if it can be written

Q1y1 Q2y2 . . . Qnyn F,

where Qi {, }, n 0, and F contains no quantifiers. In this case F is called the matrix of the

formula.

Example 2. We use Proposition 1 to transform the formula

?(x P (x, y) z Q(z)) w Q(w) (1)

to prenex form by the following chain of equivalences:

?(x P (x, y) z Q(z)) w Q(w) (?x P (x, y) ?z Q(z)) w Q(w)

(x ?P (x, y) z ?Q(z)) w Q(w)

x z (?P (x, y) ?Q(z)) w Q(w)

x z w ((?P (x, y) ?Q(z)) Q(w)) .

Note that in the above equational reasoning we use the fact that logical equivalence is a congruence

with respect to the Boolean operators (i.e., the Substitution Theorem).

Let F be a formula, x a variable, and t a term. Then F [t/x] (read "F with t for x") denotes

the formula with t substituted for every free occurrence of x in F . For example,

(x P (x, y) Q(x))[t/x] = x P (x, y) Q(t) .

Formally, we define F [t/x] by induction on terms and formulas as follows. On terms we have:

c[t/x] = c for c a constant symbol

y[t/x] = y for y = x a variable

x[t/x] = t

f (t1, . . . , tk)[t/x] = f (t1[t/x], . . . , tk[t/x]) for f a k-ary function symbol

We then extend the definition of [t/x] to formulas as follows:

P (t1, . . . , tk)[t/x] = P (t1[t/x], . . . , tk[t/x])

(?F )[t/x] = ?(F [t/x])

(F G)[t/x] = F [t/x] G[t/x]

(F G)[t/x] = F [t/x] G[t/x]

(Qy F )[t/x] = Qy (F [t/x]) y = x a variable, Q {, }

(Qx F )[t/x] = Qx F Q {, } .

2

Warning! The notation we use for the substitution is the reverse of that used in

Sch?oning's book. The latter uses [x/t] to denote the substitution of t for x. Our use is

more standard.

A key fact about substitution is the following. The proof is in Appendix A.

Lemma 3 (Translation Lemma). If t is term and F is a formula such that no variable in t occurs

bound in F , then A |= F [t/x] iff A[xA[[t]]] |= F .

To illustrate the necessity of the side-condition in the Translation Lemma, let F be the formula

yP (x) and let A be the assignment with UA = {1, 2}, PA = {1}, xA = 1, and yA = 1. Then

F [y/x] = y P (y) and so A |= F [y/x]. But A[[y]] = 1 and so A[xA[[y]]] |= F . The reason we cannot

apply the Translation Lemma in this case is that the variable y in the term to be substituted

becomes bound by the quantifier y in F . This phenomenon is called variable capture.

In first-order logic we can rename bound variables in a formula while preserving logical equiva-

lence. For example, we have x P (x) y P (y). This is similar to the fact that the definite integral

0 f (s)ds denotes the same value as 0 f (t)dt. We make this idea formal as follows:

Proposition 4. Let F = Qx G be a formula where Q {, }. Let y be a variable that does not

occur in G. Then F Qy (G[y/x]).

Proof. We prove the proposition in the case of ; the case for is similar. Let A be an assignment.

Then

A |= y (G[y/x]) iff A[ya] |= G[y/x] for all a UA

iff A[ya][xA[ya](y)] |= G for all a UA (Translation Lemma)

iff A[ya][xa] |= G for all a UA

iff A[xa][ya] |= G for all a UA

iff A[xa] |= G for all a UA (Relevance Lemma)

iff A |= x G .

2 Skolem Form

A formula is rectified if no variable occurs both bound and free and if all quantifiers in the formula

refer to different variables. For example, the formula

x y P (x, f (y)) y (Q(x, y) R(x))

is not rectified since y is bound on two separate occasions and x occurs both free and bound. By

renaming the bound variables we obtain the following equivalent rectified formula:

u v P (u, f (v)) y (Q(x, y) R(x)) .

In general we can always obtain an equivalent rectified formula by renaming bound variables

using Proposition 4.

3

Title:

Subject:

Keywords:

Author:

Creator: LaTeX with hyperref package

Producer: pdfTeX-1.40.14

CreationDate: Tue Feb 16 14:45:41 2016

ModDate: Tue Feb 16 14:45:41 2016

Tagged: no

Form: none

Pages: 6

Encrypted: no

Page size: 612 x 792 pts (letter) (rotated 0 degrees)

File size: 189329 bytes

Optimized: no

PDF version: 1.5