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

---

• (1) first order logic formula
• (2) logic proofs solver
• (3) first order logic generator
• (4) first order logic calculator

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


• Second-order Logic - Open Logic Project
• Resolution in Propositional and First-Order Logic
• Axiom Systems for Classical 16 First-Order Logic
• First-order Proofs - The College of Engineering at the …
• First-Order Logic and Proofs - Stanford University