normal form, prenex, disjunctive, conjunctive, form, normal, DNF, CNF, prenex normal form, Skolem normal form, disjunctive normal form, conjunctive normal form, Skolem

Back to title page

5. Normal Forms. Resolution Method

In this section, we will try to produce a practical method allowing to prove theorems by using computers. In general, this task is not feasible because of its enormous computational complexity (see Section 6). Still, for problems of a "practical size" (arising, for example, in deductive databases and other artificial intelligence systems, or, trying to formalize real mathematical proofs), such methods are possible and some of them are already successfully implemented.

Mizar project QED project

Classical logic only...

Main Ideas

If F₁, ..., F_n is the set of our assumptions (facts, rules, axioms, hypotheses etc.), does the assertion G follow from this set? One of the well known approaches to proving theorems in mathematics are the so-called refutation proofs (reductio ad absurdum) - proofs by deriving a contradiction: assume ~G, and derive a contradiction. I.e. prove that F₁, ..., F_n, ~G is an inconsistent set of assumptions.

Idea #1: let us prove theorems only in this way. Let us try developing the best possible method of deriving contradictions from inconsistent sets of assumptions. This (at first glance - trivial) decision is one of the most important steps in the whole history - it will allow (see below) conversion of the formulas F₁, ..., F_n, ~G into a form that does not contain existential quantifiers. And after this, having universal quantifier only, we may simply drop them all, and continue working with quantifier-free formulas (see below).

Idea #2: "normalize" assumptions as far as possible.

The first step (idea #2a) is here reducing to the so-called prenex normal form - moving all the quantifiers to left. For example, the formula

[(ExB(x) -> ExC(x)) -> ExD(x)] -> ExF(x)

is equivalent (in the classical logic!) to the following formula in prenex normal form:

Ax₁Ex₂Ax₃Ex₄[[(B(x₁) -> C(x₂)) ->D(x₃)] -> F(x₄)].

(When moving quantifiers to left, some of them are changing from E to A, or from A to E, see Section 5.1.)

The second step (idea #2b, due to Thoralf Skolem) allows elimination of existential quantifiers. Indeed, Ax₁Ex₂ means that x₂=f(x₁), and Ax₁Ex₂Ax₃Ex₄ means that x₄=g(x₁, x₃), where f and g are some functions (see Section 5.3). In this way we obtain the so-called Skolem normal form, containing universal quantifiers only:

Ax₁Ax₃[[(B(x₁) -> C(f(x₁))) ->D(x₃)] -> F(g(x₁, x₃))].

If our formulas contain universal quantifiers only, we may drop these quantifiers (simply by assuming that all free variables are universally quantified):

[(B(x₁) -> C(f(x₁))) ->D(x₃)] -> F(g(x₁, x₃)).

Note that a formula and its Skolem normal form are not equivalent (even in the classical logic!), they are only a kind of "semi-equivalent": a set of formulas is inconsistent, iff so is the set of their Skolem normal forms.

The third step (idea #2c) - reduction of quantifier-free formulas to the so-called conjunctive normal form (a conjunction of disjunctions of atomic formulas - with or without negations, see Section 5.2). For example, the above formula can be reduced to the following form:

(~B(x₁) v C(f(x₁)) v F(g(x₁, x₃))) & (~D(x₃) v F(g(x₁, x₃))).

By assuming that a set of formulas is equivalent to their conjunction, we can drop the conjunction(s) obtaining a set of the so-called clauses:

~B(x₁) v C(f(x₁)) v F(g(x₁, x₃)),

~D(x₃) v F(g(x₁, x₃)).

Each clause is a disjunctions of atomic formulas - with or without negations.

In this way, instead of our initial set of assumptions F₁, ..., F_n, ~G, we can obtain a set of clauses, which is inconsistent, iff so the set F₁, ..., F_n, ~G.

Idea #3 (due to John Alan Robinson, see Section 5.5 and 5.7) - a set of clauses is inconsistent, iff a contradiction can be derived from it by using term substitution and the so-called resolution rule:

F v C, ~C v G
----------------.
F v G

...

To be continued.

5.1. Prenex Normal Form

Let us consider an interpretation J of some first order language L, such that the domain D_J contains an infinite set of "objects". Under such interpretation, the "meaning" of formulas containing quantifiers may be more or less non-constructive, or, at least, "constructively difficult".

For example, the formula AxB(x) will be true, if B(x) will be true for all "objects" x in the (infinite!) set D_J. Thus, it is impossible to verify directly (i.e. "empirically"), is AxB(x) true or not. Saying that AxAy(x+y=y+x) is true under the standard interpretation of first order arithmetic, does not mean that we have verified this fact empirically - by checking x+y=y+x for all pairs of natural numbers x, y. Then, how do we know that AxAy(x+y=y+x) is true? Of course, we either postulated this feature of natural numbers directly (i.e. derived it from "empirical evidence"), or proved it by using some set of axioms (i.e. derived it from other postulates). But, in general, formulas having the form AxB(x), are "constructively difficult".

The formula AxEyC(x, y) may be even more difficult: it will be true, if for each x in D_J we will be able to find y in D_J such that C(x, y) is true. Thus, thinking constructively, we could say that AxEyC(x, y) is true, only, if there is an algorithm, which, for each x in D_J can find y in D_J such that C(x, y) is true. For example, under the standard interpretation of first order arithmetic, the formula

AxEy(x<y & y is prime number)

is true (i.e. "there are infinitely many prime numbers"). How do we know this? This fact has been proved in VI century BC. But the (similarly quantified) formula

AxEy(x<y & y is prime number & y+2 is prime number),

i.e. the famous twin prime conjecture, is it true or not? Nobody knows the answer.

Exercise 5.1.1. Verify that the "meaning" of AxEyAzD(x, y, z) and AxEyAzEuF(x, y, z, u) may be even more non-constructive.

But how about the formula ExG(x)->EyH(y)? Is it constructively more difficult than AxEyC(x, y), or less? In general, we could prove that ExG(x)->EyH(y) is true, if we had an algorithm, which, for each x in D_J such that G(x) is true, could find y in D_I such that G( y) is true, i.e. if AxEy(G(x)->H(y)) would be true. We will establish below, that, in the classical logic, if G does not contain y, and H does not contain x, then the formula ExG(x)->EyH(y) is equivalent to AxEy(G(x)->H(y)). Thus, in general, the formula ExG(x)->EyH(y) is constructively as difficult as is the formula AxEyC(x, y)!

To generalize this approach to comparing "constructive difficulty" of formulas, the so-called prenex normal forms have been introduced:

a) If a formula does not contain quantifiers, then it is in the prenex normal form.

b) If x is any variable, and the formula F is in the prenex normal form, then AxF and ExF also are in the prenex normal form.

c) (If you wish so,) there are no other formulas in the prenex normal form.

I.e. a formula is in the prenex normal form, iff it has all its quantifiers gathered in front of a formula that does not contain quantifiers. It appears, that in the classical logic, each formula cane be "reduced" to an appropriate equivalent formula in the prenex normal form. To obtain this normal form, the following lemmas may be used.

Lemma 5.1.1. If the formula G does not contain x as a free variable, then:

a) [L₁, L₂, L₅, L₁₂, L₁₄, MP, Gen]: G->AxF(x) <-> Ax(G->F(x)).

b) [L₁, L₂, L₅, L₁₂-L₁₅, MP, Gen]: ExF(x)->G <-> Ax(F(x)->G).

c) [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: G->ExF(x) <-> Ex(G->F(x)). More precisely:

[L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: G->ExF(x) -> Ex(G->F(x)). This formula cannot be proved constructively! Why? See Section 4.5. But the converse formula can be proved constructively:

[L₁, L₂, L₁₃-L₁₅, MP, Gen]: Ex(G->F(x)) -> (G->ExF(x)).

d) [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: (AxF(x)->G) <-> Ex(F(x)->G). More precisely:

[L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: (AxF(x)->G) -> Ex(F(x)->G). This formula cannot be proved constructively! Why? See Section 4.5. But the converse formula can be proved constructively:

[L₁, L₂, L₁₃-L₁₅, MP, Gen]: Ex(F(x)->G) -> (AxF(x)->G).

Proof.

First, let us note that (a)<- is an instance of the axiom L₁₄: Ax(G->F(x))->(G->AxF(x)), and that (b)<- is an instance of the axiom L₁₅.

Prove (a)-> and (b)-> as the Exercise 5.1.2 below.

Let us prove (c)<-: Ex(G->F(x))->(G->ExF(x)).

Let us prove (d)<-: Ex(F(x)->G) ->(AxF(x)->G) .

Now, let us prove (c)->: (G->ExF(x)) -> Ex(G->F(x)) in the classical logic (a constructive proof is impossible, see Section 4.5).

Finally, let us prove (d)->: (AxF(x)->G) -> Ex(F(x)->G) in the classical logic(a constructive proof is impossible, see Section 4.5). Let us denote this formula by H.

Q.E.D.

Exercise 5.1.2. a) Prove (a)-> of Lemma 5.1.1, [L₁, L₂, L₅, L₁₂, L₁₄, MP, Gen]: (G->AxF(x)) -> Ax(G->F(x)).

b) Prove (b)-> of Lemma 5.1.1, [L₁, L₂, L₅, L₁₂-L₁₅, MP, Gen]: (ExF(x)->G) -> Ax(F(x)->G).

Lemma 5.1.2. If the formula G does not contain x as a free variable, then

a) [L₁-L₅, L₁₂-L₁₅, MP, Gen]: ExF(x)&G <-> Ex(F(x)&G).

b) [L₁-L₅, L₁₂, L₁₄, MP, Gen]: AxF(x)&G<->Ax(F(x)&G).

c) [L₁, L₂, L₅, L₆-L₈, L₁₂-L₁₅, MP, Gen]: ExF(x)vG<->Ex(F(x)vG).

d) [L₁-L₁₁, L₁₂, L₁₄, MP, Gen]: AxF(x)vG <-> Ax(F(x)vG). More precisely:

[L₁, L₂, L₅, L₆-L₈, L₁₂, L₁₄, MP, Gen]: AxF(x)vG -> Ax(F(x)vG), i.e. this part of the equivalence can be proved constructively. But,

[L₁-L₁₁, L₁₂, L₁₄, MP, Gen]: Ax(F(x)vG) -> AxF(x)vG. This formula cannot be proved constructively! Why? See Section 4.5.

Proof.

Prove (a, b, c) as the Exercise 5.1.3 below.

Let us prove (d)->: AxF(x)vG -> Ax(F(x)vG).

Finally, let us prove (d)<-: Ax(F(x)vG) -> AxF(x)vG in the classical logic (a constructive proof is impossible, see Section 4.5).

Q.E.D

Exercise 5.1.3. Prove Lemma 5.1.2(a, b, c).

.Lemma 5.1.3. a) [L₁-L₁₀, L₁₂-L₁₅, MP, Gen]: ~ExF(x) <-> Ax~F(x).

b) [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: ~AxF(x) <-> Ex~F(x). More precisely:

[L₁-L₁₁, L₁₃, L₁₄, MP, Gen]: ~AxF(x) -> Ex~F(x). This formula cannot be proved constructively! Why? See Section 4.5. But,

[L₁-L₁₀, L₁₃, L₁₄, MP, Gen]: Ex~F(x) -> ~AxF(x).

Proof.

a) See Section 3.2, Group IV.

b)->. This is exactly Section 3.2, III-4.

b)<-. See Section 3.2, Group III.

Q.E.D.

Let us recall that a formula is in the prenex normal form, iff it has all its quantifiers gathered in front of a formula that does not contain quantifiers.

Theorem 5.1.4. (Author?) In the classical logic, each formula is equivalent to an appropriate formula in the prenex normal form. More precisely, if F is a formula, then, following a simple algorithm, a formula F' can be constructed such that: a) F' is in a prenex normal form, b) F' has the same free variables as F, c) [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: F<->F'.

Proof. Let us start by an example:

ExG(x)->EyH(y).

If H did not contain x as a free variable, then, by Lemma 5.1.1(b): ExF(x)->G <-> Ax(F(x)->G), i.e. this formula would be equivalent to Ax(G(x)->EyH(y)). Now, let us consider the sub-formula G(x)->EyH(y). If G did not contain y as a free variable, then, by Lemma 5.1.1(c): G->ExF(x) <-> Ex(G->F(x)), the sub-formula would be equivalent to Ey(G(x)->H(y)). Hence, by Replacement Theorem 2, Ax(G(x)->EyH(y)) would be equivalent to AxEy(G(x)->H(y)).

But, if H would contain x as a free variable, and/or G would contain y as a free variable? Then our "shifting quantifiers up" would be wrong - the formula AxEy(G(x)->H(y)) would not be equivalent to ExG(x)->EyH(y).

To avoid this problem, let us use Replacement Theorem 3, which says that the meaning of a formula does not depend on the names of bound variables used in it. Thus, as the first step, in ExG(x), let us replace x by another variable letter x₁ that does not appear neither in G, nor in H. Then, by Replacement Theorem 3, ExG(x) is equivalent to Ex₁G(x₁), and by Replacement Theorem 2, ExG(x)->EyH(y) is equivalent to Ex₁G(x₁)->EyH(y). Now, Ax₁(G(x₁)->EyH(y)) is really equivalent to Ex₁G(x₁)->EyH(y). As the next step, in EyH(y), let us replace y by another variable letter y₁ that does not appear neither in G, nor in H. Then, by Replacement Theorem 3, EyH(y) is equivalent to Ey₁H(y₁), and by Replacement Theorem 2, G(x₁)->Ey₁H(y₁) is equivalent to Ey₁(G(x₁)->H(y₁)). And, finally, ExG(x)->EyH(y) is equivalent to Ax₁Ey₁(G(x₁)->H(y₁)).

Now, we can start the general proof. In a formula F, let us find the leftmost quantifier having a propositional connective over it. If such a quantifier does not exist, the formula is in the prenex normal form. If such a quantifier exists, then F is in one of the following forms:

Q_qQ_q...Q_q(...(~QxG)...), or Q_qQ_q...Q_q(...(QxGooH)...), or Q_qQ_q...Q_q(...(GooQxH)...),

where Q_qQ_q...Q_q are the quantifiers "already in prefix", Q is the quantifier in question, and oo is the propositional connective standing directly over Q.

In the first case, by Lemma 5.1.3, ~QxG is equivalent to Q'x~G, where Q' is the quantifier opposite to Q. By Replacement Theorem 2, Q_qQ_q...Q_q(...(~QxG)...) is then equivalent to Q_qQ_q...Q_q(...(Q'x~G)...), i.e. Q' has now one propositional connective less over it ( (than had Q).

In the second case, as the first step, in QxG, let us replace x by another variable letter x₁ that does not appear in the entire formula F at all. Then, by Replacement Theorem 3, QxG is equivalent to Qx₁G₁, and by Replacement Theorem 2, Q_qQ_q...Q_q(...(QxGooH)...) is equivalent to Q_qQ_q...Q_q(...(Qx₁G₁ooH)...). Now, we can apply the appropriate case of Lemma 5.1.1 or Lemma 5.1.2, obtaining that Qx₁G₁ooH is equivalent to Q'x₁(G₁ooH), where Q' is the quantifier determined by the lemma applied. Then , by Replacement Theorem 2, Q_qQ_q...Q_q(...(Qx₁G₁ooH)...) is equivalent to Q_qQ_q...Q_q(...(Q'x₁(G₁ooH))...), i.e. Q' has now one propositional connective less over it (than had Q).

In the third case, the argument is similar.

By iterating this operation a finite number of times, we arrive at a formula F' which is in the prenex normal form, and which is (in the classical logic) equivalent to F. Q.E.D.

Note. Most formulas admit many different prenex normal forms. For example, the above formula ExG(x)->EyH(y) is equivalent not only to Ax₁Ey₁(G(x₁)->H(y₁)), but also to Ey₁Ax₁(G(x₁)->H(y₁)) (verify).

As an example, let us obtain a prenex normal form of the following formula:

ExB(x) v AxC(x) -> AxD(x) & (~AxF(x)).

Assign unique names to bound variables: Ex₁B(x₁) v Ax₂C(x₂) -> Ax₃D(x₃) & (~Ax₄F(x₄)).

Process disjunction: Ex₁Ax₂(B(x₁) v C(x₂)) -> Ax₃D(x₃) & (~Ax₄F(x₄)).

Process negation (A-E): Ex₁Ax₂(B(x₁) v C(x₂)) -> Ax₃D(x₃) & Ex₄~F(x₄))

Process conjunction: Ex₁Ax₂(B(x₁) v C(x₂)) -> Ax₃Ex₄(D(x₃) & ~F(x₄)).

Process implication premise: (E-A, A-E): Ax₁Ex₂( B(x₁) v C(x₂) -> Ax₃Ex₄(D(x₃) & ~F(x₄)).

Process implication consequent: Ax₁Ex₂Ax₃Ex₄( B(x₁) v C(x₂) -> D(x₃) & ~F(x₄)).

The last two steps could be performed in the reverse order as well.

Exercise 5.1.4. Transform each of the following formulas into a prenex normal form. Write down every single step of the process. (Hint: the algorithm is explained in the proof of Theorem 5.1.4.)

a) ExB(x)->(ExC(x)->ExD(x)),

b) AxEyB(x, y) & ExC(x) -> AyExD(x, y),

c) ExB(x, y, z) -> AxC(x, y) v EyD(y, z),

d) AxB(x) -> (AxC(x) -> (AxD(x) -> AxF(x))),

e) ((ExB(x) -> ExC(x)) -> ExD(x)) -> ExF(x).

Note. From a programmer's point of view, prenex normal forms are, in a sense, a crazy invention. In computer programming, you always try to reduce loop bodies, not to extend them as much as possible!

Exercise 5.1.5. We may use reduction to prenex normal forms in proofs. More precisely, let us try extending the classical logic by introducing of the following additional inference rule (let us call it PNF-rule): given a formula F, replace it by some its prenex normal form F'. Verify, that, in fact, this rule does not extend the classical logic, i.e. if there is a proof of F₁, F₂, ..., F_n |- G in [L₁-L₁₅, MP, Gen, PNF-rule], then there is a proof of the same in [L₁-L₁₅, MP, Gen]. (In some other texts, such rules are called admissible. Thus, the PNF-rule is admissible in the classical logic.)

5.2. Conjunctive and Disjunctive Normal Forms

Let us continue the "normalization" process that we started in Section 5.1 by reducing formulas to their prenex normal forms, where all quantifiers are gathered in front of a formula that does not contain quantifiers. How could we further "normalize" this "formula that does not contain quantifiers"?

Step 1: eliminate equivalence

First of all, we can eliminate all equivalence connectives because B<->C is only a shortcut for (B->C)&(C->B). Why should we? Because, proving of B<->C includes proving of B->C and proving of C->B. Using the shortcut simplifies the appearance of the formula, not its proof.

Step 2: eliminate implication

After this, our formula will contain only implication, conjunction, disjunction and negation connectives. As the next step, we could try to eliminate one (or two?) of these connectives. The classical logic allows this. For example, by Theorem 2.6.4(b),

[L₁-L₁₁, MP]: |- (A->B)<->~AvB.

By using this equivalence, we can eliminate implication connectives. For example, the formula B->(C->D) is equivalent (in the classical logic only!) to ~Bv(~CvD).

But, instead of implications, we could try eliminating disjunctions or conjunctions as well. Indeed,

Exercise 5.2.1. In the classical logic [L₁-L₁₁, MP], prove the following:

a) |- (A->B)<->~(A&~B).

b) |- (AvB)<->(~A->B).

c) |- (AvB)<->~(~A&~B).

d) |- (A&B)<->~(A->~B).

e) |- (A&B)<->~(~Av~B).

(For smart students) Determine, which parts of these equivalencies can be proved in the constructive logic [L₁-L₁₀, MP]. End of Exercise 5.2.1.

By using these results, we could eliminate from our formulas any one (or any two) of the three connectives - implication, conjunction, or disjunction.

However, the best decision would be eliminating only implications. Why? Because conjunction and disjunction are associative and commutative operations - and very much like addition (disjunction) and multiplication (conjunction)! For example, after reducing the formula B->(C->B) to ~Bv(~CvB), we can further transform it to ~Bv~CvB and Bv~BvC - and conclude that it is "true and provable" (no surprise, it is Axiom L₁).

Step 3: move negations down to atoms

Thus, after Step 2, our formula contains only conjunction, disjunction and negation connectives. Now, let us recall the two de Morgan laws:

Theorem 2.6.3, [L₁-L₁₁, MP]: |- ~(A&B) <-> ~Av~B.
Theorem 2.4.10(b), [L₁-L₉, MP] |- ~(AvB) <-> ~A&~B.

By using these equivalencies, we can shift negations down - until the atoms of the formula. For example, let us transform the formula ((A->B)->C)->(C->B):

((A->B)->C)->(C->B)
~((A->B)->C)v(C->B)
~((A->B)->C)v(~CvB)
~(~(A->B)vC)v(~CvB)
~(~(~AvB)vC)v(~CvB) - after Step 2
(~~(~AvB)&~C)v(~CvB)
(~(~~A&~B)&~C)v(~CvB)
((~~~Av~~B)&~C)v(~CvB)

Now, let us recall the Double Negation Law:

Theorem 2.6.1, [L₁-L₁₁, MP]: |- ~~A <-> A.

It allows dropping the ugly excessive negations - we can replace ~~~A by ~A and ~~B - by B:

((~AvB)&~C)v(~CvB)

Step 4: algebra

After Step 3, our formula is built up by using:

a) atoms,

b) atoms preceded by a negation,

c) conjunction and disjunction connectives.

Conjunction and disjunction are associative and commutative operations. By the behavior of "truth values", conjunction is a kind of multiplication (0&0=0, 0&1=1&0=0, 1&1=1), and disjunction - a kind of addition (0v0=0, 0v1=1v0=1, 1v1=1). However, for these operations two distributive laws are valid (Theorem 2.3.1) - conjunction is distributive to disjunction, and disjunction is distributive to conjunction:

[L₁-L₈, MP]: |- (A&B)vC<->(AvC)&(BvC).
[L₁-L₈, MP]: |- (AvB)&C<->(A&C)v(B&C).

Thus, both of the two decisions could be justified:

1) (Our first "algebra") Treat conjunction as multiplication and disjunction - as addition (+). Then the above formula ((~AvB)&~C)v(~CvB) takes the form ((A'+B)C')+(C'+B) (let us replace ~A by a "more algebraic" A'). After this, the usual algebraic transformations yield the formula A'C'+BC'+C'+B.

2) (Our second "algebra") Treat conjunction as addition (+) and disjunction - as multiplication. Then the above formula ((~AvB)&~C)v(~CvB) takes the form ((A'B)+C')(C'B). After this, the usual algebraic transformations yield the formula A'BBC'+BC'C'.

Additional rules can be applied in these "algebras".

First rule - conjunction and disjunction are idempotent operations:

[L₁- L₅, MP]: |- A&A<->A (see Section 2.2).
[L₁, L₂, L₅, L₆-L₈, MP]: |- AvA<->A (Exercise 2.3.1(c)).

Thus, in both of our "algebras": A+A = AA = A.

Second rule - A&~A (i.e. "false") is a kind of "zero" in the first "algebra", and a kind of "one" - in the second "algebra":

[L₁-L₁₀, MP]: |- Bv(A&~A) <-> B (Exercise 2.5.1(a)).
[L₁-L₁₀, MP]: |- ((A&~A)&B)vC <-> C (Exercise 2.5.1(b)).

Indeed, in the first "algebra", these formulas mean B+AA' = B and AA'B+C = C, i.e. we may think that AA'=0, B0=0, C+0=C. In the second "algebra", these formulas mean B(A+A') = B and (A+A'+B)C = C, i.e. we may think that A+A'=1, B1=B, C+1=1.

Third rule - Av~A (i.e. "true") is a kind of "one" in the first "algebra", and a kind of "zero" - in the second "algebra":

[L₁-L₁₁, MP]: |- B&(Av~A) <-> B (Exercise 2.6.2(a)).
[L₁-L₁₁, MP]: |-( (Av~A)vB)&C <-> C (Exercise 2.6.2(b)).

Indeed, in the first "algebra", these formulas mean B(A+A') = B and (A+A'+B)C = C, i.e. we may think that A+A'=1, C1=1, B+1=1. In the second "algebra". these formulas mean B+AA' = B and AA'B+C = C, i.e. we may think that AA'=0, B0=0, C+0=C.

So, let us continue:

1) (The first "algebra") Nothing new for the formula A'C'+BC'+C'+B, or, if we return to logic: (~A&~C)v(B&~C)v(~C)v(B). Such disjunctions consisting of conjunctions are called disjunctive normal forms (DNFs). In a DNF, each conjunction contains each atom no more than once - either without negation, or with it. Indeed, if it contains some atom X twice, then: a) replace XX by X, b) replace X'X' by X', c) replace XX' by 0 and drop the entire conjunction from the expression. In this way, for some formulas, we may obtain an empty DNF. Of course, such formulas take only false values ("false" is "zero" in the first "algebra").

2) (The second "algebra") The formula A'BBC'+BC'C' is equivalent to A'BC'+BC', or, if we return to logic: (~AvBv~C)&(Bv~C). Such conjunctions consisting of disjunctions are called conjunctive normal forms (CNFs). In a CNF, each disjunction contains each atom no more than once - either without negation, or with it. Indeed, if it contains some atom X twice, then: a) replace XX by X, b) replace X'X' by X', c) replace XX' by 0 and drop the entire disjunction from the expression. In this way, for some formulas, we may obtain an empty CNF. Of course, such formulas take only true values ("true" is "zero" in the second "algebra").

Thus, we have proved the following

Theorem 5.2.1. (Authors?) In the classical logic, every propositional formula can be reduced to DNF and to CNF. More precisely, assume, the formula F has been built of formulas B₁, B₂, ..., B_n by using propositional connectives only. Then:

a) There is a formula F₁, which is in a (possibly empty) disjunctive normal form over B₁, B₂, ..., B_n such that [L₁-L₁₁, MP]: |- F <-> F₁.

b) There is a formula F₂, which is in a (possibly empty) conjunctive normal form over B₁, B₂, ..., B_n such that [L₁-L₁₁, MP]: |- F <-> F₂.

Exercise 5.2.2. a) Build DNFs and CNFs of the following formulas. (Hint: the algorithm is explained in the above Steps 1-4.)

~(A&B->C),
(A->B)<->(C->D),
AvB<->CvD,
A&B<->C&D.

b) Build DNFs and CNFs of the following formulas:

~(Av~A),
((A->B)->A)->A,
(A->B)->((~A->B)->B).

Exercise 5.2.3. a) Verify that, under the classical truth tables, a formula takes only false values, iff: a₁) in the first "algebra", it can be reduced to 0, i.e. to B_i&~B_i (for some i), a₂) in the second "algebra", it can be reduced to 1, i.e. to B_i&~B_i (for some i).

b) Verify that, under the classical truth tables, a formula takes only true values, iff: b₁) in the first "algebra", it can be reduced to 1, i.e. to B_iv ~B_i (for some i), b₂) in the second "algebra", it can be reduced to 0, i.e. to B_iv ~B_i (for some i).

Appendix. Complexity Considerations (do not read)

Assume, the formula F has been built of formulas B₁, B₂, ..., B_n by using propositional connectives only. We wish to determine, takes F only true values, or not. How many time may this task require?

You could take, one by one, all the possible 2ⁿ combinations of n atomic truth values: 0...00, 0...01, 0...10, 0...11, ..., 1...11. And compute the truth value of F for each of these combinations. If you obtain a false value, print the corresponding combination as the negative result. Otherwise, you will spend at least 2ⁿ units of time to establish that F takes only true values (at least one unit per each evaluation of F). Thus, the straightforward algorithm takes "exponential time".

Could reducing to DNFs (or CNFs) make this task easier?

As you established in Exercise 5.2.3(b), a formula takes only true values, iff, in the first "algebra", it can be reduced to 1, i.e. to B_iv ~B_i (for some i). How many time may this reduction process require?

Assume, the formula F contains: k₀ occurrences of atoms, k₁ negations, k₂ conjunctions, k₃ disjunctions and k₄ implications (verify that k₀ <= k₂+k₃+k₄+1).

In Step 2, we eliminate implications by replacing A->B by ~AvB. Thus, after this step, our formula will contain k₁+k₄ negations, k₂ conjunctions and k₃+k₄ disjunctions (and the same number k₀ of occurrences of atoms).

In Step 3, we move negations down to atoms by replacing: ~(A&B) - by ~Av~B, and ~(AvB) - by ~A&~B, and finally, we reduce negations by replacing ~~A by A. Thus, after this step, we can have a somewhat larger number of negations, but the total number of conjunctions and disjunction will remain the same - k₂+k₃+k₄. The number of occurrences of atoms also will remain the same - k₀.

Suppose, in Step 4, we wish to use our two "algebras" to obtain a DNF or CNF (let's say simply NF). I.e. we will always replace (A+B)C by AC+BC. Each of such operations not only adds one more conjunction (in the first "algebra", or disjunction - in the second "algebra") - it is doubling the entire formula C! Which size will we have at the end? If the formulas F₁ and F₂ are already in the NF containing d₁ and d₂ members accordingly, then:

a) For the formula F₁+F₂, we can obtain a NF containing d₁+d₂ members. For example,

(C₁+C₂+C₃+C₄)+(C₅+C₆+C₇) = C₁+C₂+C₃+C₄+C₅+C₆+C₇.

b) For the formula F₁F₂, we can obtain a NF containing d₁d₂ members (each member of F₁ is combined with each member of F₂). For example,

(C₁+C₂+C₃)(C₄+C₅) = C₁C₄+C₂C₄+C₃C₄+C₁C₅+C₂C₅+C₃C₅.

So, let us denote by D(m) the "worst case" size (number of disjunction members) of the NF obtained by Steps 2-4 from a formula containing m propositional connectives (conjunctions, disjunctions and implications). As e established above, after Step 3, the formula will contain m conjunctions and disjunctions.

Of course, D(0) = 1 - NF of the formula X₁ consists of 1 member (X₁ is an atom, or negation of an atom).

Of course, D(1) = 2 - NF of the formula X₁X₂ consists of 1 member, and NF of the formula X₁+X₂ - of 2 members. The worst case is X₁+X₂.

Now, let us calculate D(2). A formula containing 2 connectives, is a conjunction or disjunction of two formulas - one of them contains 0 connectives, the other - 1 connective. In this way we can obtain NFs consisting of D(0)+D(1) = 3 and D(0)D(1) = 2 members. Hence, D(2) = 3. The worst case is X₁+X₂+X₃.

The next step: D(3) is the maximum of

D(0)+D(2) = 4, D(0)D(2) = 3,
D(1)+D(1) = 4, D(1)D(1) = 4,

i.e. D(3) = 4. The worst cases are (X₁+X₂)(X₃+X₄) and X₁+X₂+X₃+X₄.

D(4) is the maximum of

D(0)+D(3) = 5, D(0)D(3) = 4,
D(1)+D(2) = 5, D(1)D(2) = 6,

i.e. D(4) = 6. The worst case is (X₁+X₂+X₃)(X₄+X₅).

D(5) is the maximum of

D(0)+D(4) = 7, D(0)D(4) = 6,
D(1)+D(3) = 6, D(1)D(3) = 8,
D(2)+D(2) = 6, D(2)D(2) = 9,

i.e. D(5) = 9. The worst case is (X₁+X₂+X₃)(X₄+X₅+X₆).

Exercise 5.2.4. Verify that:
- D(6) = 12 - the worst case are (X₁+X₂+X₃)(X₄+X₅)(X₆+X₇) and (X₁+X₂+X₃)(X₄+X₅+X₆+X₇),
- D(7) = 18 - the worst case is (X₁+X₂+X₃)(X₄+X₅+X₆)(X₇+X₈),
- D(8) = 27 - the worst case is (X₁+X₂+X₃)(X₄+X₅+X₆)(X₇+X₈+X₉),
- D(9) = 36 - the worst cases are (X₁+X₂+X₃)(X₄+X₅+X₆)(X₇+X₈)(X₉+X₁₀) and (X₁+X₂+X₃)(X₄+X₅+X₆)(X₇+X₈+X₉+X₁₀),
- D(10) = 54- the worst case is (X₁+X₂+X₃)(X₄+X₅+X₆)(X₇+X₈+X₉)(X₁₀+X₁₁),
- D(11) = 81- the worst case is (X₁+X₂+X₃)(X₄+X₅+X₆)(X₇+X₈+X₉)(X₁₀+X₁₁+X₁₂).

This should be enough to propose a formula allowing to calculate D(m), Indeed,

Theorem 5.2.2. If a formula has been built by using m propositional connectives (conjunctions, disjunctions and implications) and any number of negations and atoms, then, after Step4 of the above method, it will be in a DNF (or CNF) consisting of no more than D(m) disjunction (or conjunction) members, where D(m) < 2*3^m/3 = 2*2^m*0.52832.... More precisely, D(0) = 1, and for any k>=0:

- D(3k+1) = 2*3^k - the worst case is (X+X+X)^k(X+X),
- D(3k+2) = 3*3^k - the worst case is (X+X+X)^k(X+X+X),
- D(3k+3) = 4*3^k - the worst cases are (X+X+X)^k(X+X)(X+X) and (X+X+X)^k(X+X+X+X).

Or, for any k>=0 and 1<=r<=3: D(3k+r) = (r+1)*3^k.

Proof. By induction: let us assume, that m>=3, and that the formula is true for all numbers less than m, and let us verify it for m.

Let m = x +y+1.

If x=0 and y=0, then D(0)+D(0) = 2 = D(1), and D(0)*D(0) = 1 < D(1).

If x=0 and y>0, then y = 3v+q and and D(y) = (q+1)*3^v .

If x>0 and y>0, then x = 3u+p and y = 3v+q, and, D(x) = (p+1)*3^u and D(y) = (q+1)*3^v. Since D(x)>=2 and D(y)>=2, we may use the fact that D(x)+D(y)<=D(x)D(y) (verify!), i.e. we may ignore cases D(x)+D(y).

To complete the proof, we must verify that for all m: D(m) < 2*3^m/3 = 2*2^m*0.52832.... Indeed:

1) m = 3k+1: D(m) = 2*3^k = 2*(3^-1/3)*3^(3k+1)/3 < 2*3^m/3.

2) m = 3k+2: D(m) = 3*3^k = 3*(3^-2/3)*3^(3k+2)/3 < 2*3^m/3.

3) m = 3k+3: D(m) = 4*3^k = 4*(3^-1)*3^(3k+3)/3 < 2*3^m/3.

Q.E.D.

To be continued.

5.3. Skolem Normal Form

It was first introduced by Thoralf Skolem (1887-1963) in 1928:

Th.Skolem. Ueber die mathematische Logik. "Norsk matematisk tidsskrift", 1928, vol.10, pp.125-142 (see online comments: Clarification: Skolem by Stanley N.Burris, and Thoralf Skolem: Pioneer of Computational Logic by Herman R.Jervell).

The first very important idea was proposed by Skolem already in 1920:

Th. Skolem. Logisch-kombinatorische Untersuchungen �ber die Erf�llbarkeit und Beweisbarkeit mathematischen S�tze nebst einem Theoreme �ber dichte Mengen. Videnskabsakademiet i Kristiania, Skrifter I, No. 4, 1920, pp. 1-36

Namely, further "normalization" becomes possible, if we drop the requirement that the "normal form" must be equivalent to the initial formula, and replace it by the requirement: "normal form" must be logically valid; iff the initial formula is logically valid. It appears, that in this way we can "reduce" any closed formula to a closed formula containing only one kind of quantifiers - Ex₁Ex₂...Ex_n H(x₁, x₂, ..., x_n), where H does not contain quantifiers at all (see Theorem 5.3.4 below).

Still, in his original formulation, instead of logical validity, Skolem was interested in a more technical notion - satisfiability. Let us recall that, in a first order language L, a formula F is called satisfiable, iff there is an interpretation of the language L such that F is true for some values of its free variables.

Skolem' s second main idea (proposed in his 1928 paper): allow introduction of new constant and function letters. It can be demonstrated on the following example: how could we "simplify" the formula AxEy F(x, y)? It asserts that for each x there is y such that F(x, y) is true. Thus, it asserts, that there is a function g, which selects for each value of x a value of y such that F(x, y) is true. Thus, in a sense, AxEy F(x, y) is "equivalent" to Ax F(x, g(x)). In which sense? In the sense that

AxEy F(x, y) is satisfiable, iff Ax F(x, g(x)) is satisfiable.

Indeed,

1. If AxEy F(x, y) is satisfiable, then there is an interpretation J where it is true, i.e. for each value of x there is a value of y such that F(x, y) is true. This allows us to define the following interpretation of the function letter g: g(x) is one of y-s such that F(x, y) is true in J. If we extend J by adding this interpretation of the letter g, we obtain an interpretation J', where Ax F(x, g(x)) is true, i.e. this formula is satisfiable.

2. If Ax F(x, g(x)) is satisfiable, then there is an interpretation J where it is true, i.e. for each value of x the formula F(x, g(x)) is true. Hence, in this interpretation, for each value of x there is a value of y (namely, g(x)) such that F(x, y) is true in J. Thus, AxEy F(x, y) is true in J, i.e. this formula is satisfiable.

Note. In the first part of this proof, to define the function g, we need, in general, the Axiom of Choice. Indeed, if there is a non-empty set Y_x of y-s such that F(x, y) is true, to define g(x), we must choose a single element of Y_x. If we know nothing else about the interpretation J, we are forced to use the Axiom of Choice. But, if we know that the interpretation J has a countable domain, then we can define g(x) as the "least" y from the set Y_x. In this way we can avoid using the Axiom of Choice.

The third idea is even simpler: the formula Ex F(x) asserts that there is x such that F(x) is true, so, let us denote by (a constant letter) c one of these x-s, thus obtaining F(c) as a "normal form" of Ex F(x). Of course (verify),

Ex F(x) is satisfiable, iff F(c) is satisfiable.

These two ideas allow "reducing" of any quantifier prefix Qx₁Qx₂...Qx_n to a sequence of universal quantifiers only:

Theorem 5.3.1 (Th.Skolem). Let L be a first order language. There is an algorithm allowing to construct, for each closed formula F of this language, a closed formula F' (in a language L' obtained from L by adding a finite set of new constant letters and new function letters - depending on F) such that:

a) F' is satisfiable, iff F is satisfiable,

b) F' is in form Ax₁Ax₂...Ax_n G, where n>=0, and G does not contain quantifiers.

If a formula is in form Ax₁Ax₂...Ax_n G, where n>=0, and G does not contain quantifiers, let us call it Skolem normal form. Thus, each closed formula can be reduced to a Skolem normal form in the following sense: for each closed formula F of a language L there is a Skolem normal form |F|_Sk (in the language L extended by a finite set of Skolem constants and Skolem functions), which is satisfiable, iff so is F.

Note. Theorem 5.3.1 does not assert that a formula and its Skolem normal form are equivalent. It asserts only that the satisfiability problem of the first formula is equivalent to the satisfiability problem of the second formula.

Thus, if we would be interested in determining the satisfiability of formulas, then reducing to Skolem normal forms would be a promising method. Indeed, formulas Ax₁Ax₂...Ax_n G (where G does not contain quantifiers) are, perhaps, easier to analyze...

Proof of Theorem 5.3.1 First, let us obtain a prenex normal form F₁ of the formula F (see Section 5.1). Indeed, by Theorem 5.1.4, there is a simple algorithm, allowing to construct a closed formula F₁ such that F₁ is a prenex normal form, and, in the classical logic, |- F<->F₁. Of course, F₁ is satisfiable; iff so is F.

If the quantifier prefix of F₁ starts with a sequence of existential quantifiers (EE...EA...), we will need the following lemma to "reduce" these quantifiers:

Lemma 5.3.2 . A closed formula Ex₁Ex₂...Ex_n H(x₁, x₂, ..., x_n) is satisfiable, iff H(c₁, c₂, ..., c_n) is satisfiable, where c₁, c₂, ..., c_n are new constant letters that do not appear in H.

After this operation, we have a closed prenex formula H(c₁, c₂, ..., c_n) (in a language obtained from L by adding a finite set of new constant letters, called Skolem constants), which is satisfiable, iff so is F₁ (and F). The the quantifier prefix of H(c₁, c₂, ..., c_n) (if any) starts with a sequence of universal quantifiers (AA...AE...).

To proceed, we will need the following

Lemma 5.3.3. A closed formula Ax₁Ax₂...Ax_nEy K(x₁, x₂, ..., x_n, y) is satisfiable, iff Ax₁Ax₂...Ax_n K(x₁, x₂, ..., x_n, g(x₁, x₂, ..., x_n)) is satisfiable, where g is a new n-ry function letter (called Skolem function), which does not appear in K.

By iterating this lemma, we can "reduce" the entire quantifier prefix of H(c₁, c₂, ..., c_n) to a sequence of universal quantifiers only (AA...A).

For example, the formula AxAyEzAuEw F(x, y, z, u, w) is satisfiable, iff so is

AxAyAuEw F(x, y, g(x, y), u, w),

and so is

AxAyAu F(x, y, g(x, y), u, h(x, y, u)),

where g and h are Skolem functions that do not appear in F.

Exercise 5.3.1. a) Prove Lemma 5.3.2. b) Prove Lemma 5.3.3.

How many new constant letters and new function letters (Skolem constants and functions) do we need to obtain the final formula F'? The number of new letters is determined by the number of existential quantifiers in the quantifier prefix of the prenex formula F₁. Indeed, a) the number of new constant letters is determined by the number of existential quantifiers in front of the prefix, and b) the number of new function letters is determined by the number of existential quantifiers that follow after the universal ones.

This completes the proof of Theorem 5.3.1.

Exercise 5.3.2. Obtain Skolem normal forms of the formulas mentioned in Exercise 5.1.4.

Still, if we are interested in determining the logical validity of formulas, then we should apply the result of Exercise 4.1.3 together with Theorem 5.3.1:

F is logically valid, iff ~F is not satisfiable, iff a Skolem normal form of ~F is not satisfiable, iff Ax₁Ax₂...Ax_n G (where n>=0, and G does not contain quantifiers) is not satisfiable, iff ~Ax₁Ax₂...Ax_n G is logically valid, iff Ex₁Ex₂...Ex_n ~G is logically valid.

Thus we have proved the following

Theorem 5.3.4. Let L be a first order language. There is an algorithm allowing to construct, for each closed formula F of this language, a closed formula F' (in a language L' obtained from L by adding a finite set of new constant letters and new function letters - depending on F) such that:

a) F' is logically valid (or, provable in the classical logic), iff F is logically valid (or, provable in the classical logic),

b) F' is in form Ex₁Ex₂...Ex_n G, where n>=0, and G does not contain quantifiers.

The objects of artificial intelligence and of deductive databases are, as a rule, large sets of formulas, i.e., in fact, large conjunctions of formulas. Thus, the following extension of Theorem 5.3.1 will be very useful - it will allow separate reducing to Skolem normal form of each conjunction member (instead of reducing the entire conjunction as a single very long formula):

Theorem 5.3.5. Let L be a first order language. There is an algorithm allowing to construct, for each finite set of closed formulas F₁, F₂, ..., F_n of this language, a set of closed formula |F₁|_Sk, |F₂|_Sk, ..., |F_n|_Sk (in a language L' obtained from L by adding a finite set of new constant letters and new function letters) such that:

a) |F₁|_Sk, |F₂|_Sk, ..., |F_n|_Sk are all Skolem normal forms of F₁, F₂, ..., F_n respectively,

b) the conjunction F₁&F₂& ...&F_n is satisfiable, iff so is the conjunction |F₁|_Sk& |F₂|_Sk& ... &|F_n|_Sk.

Proof.

...

To be continued.

Exercise 5.3.3 (for smart students). In his above-mentioned 1920 paper, for quantifier elimination, Skolem proposed introduction of new predicate letters (to the idea that function letters will do better, he arrived only in the 1928 paper). Do not read neither Skolem's papers, nor the above-mentioned online comments, and prove yourself that by introduction of new predicate letters, the satisfiability problem of any closed formula can be reduced to the satisfiability problem of a formula having the form Ax₁Ax₂...Ax_mEy₁Ey₂...Ey_n G, where m, n>=0, and G does not contain quantifiers. Thus, function letters "will do better" - see Theorem 5.3.1.

Exercise 5.3.4 (compare with Exercise 5.1.5). Since, in general, Skolem normal form is not equivalent to the initial formula, we cannot use reduction to Skolem normal forms in the usual ("positive", or affirmative) proofs. But we may use it in "negative" (or, refutation) proofs, i.e. in proofs aimed at deriving a contradiction! More precisely, let us try extending the classical logic by introducing of the following additional inference rule (let us call it SNF-rule): given a formula F, replace it by some its Skolem normal form F' (such that the newly introduced constants and function letters do not appear in the proof before F'). Verify, that, in fact, this rule does not extend the classical logic for refutation proofs, i.e. if, from a set of formulas F₁, F₂, ..., F_n, one can derive a contradiction by using [L₁-L₁₅, MP, Gen, SNF-rule], then one can do the same by using [L₁-L₁₅, MP, Gen]. (Thus, the SNF-rule is admissible for refutation proofs in the classical logic.)

Back to title page

normal form, prenex, disjunctive, conjunctive, form, normal, DNF, CNF, prenex normal form, Skolem normal form, disjunctive normal form, conjunctive normal form, Skolem