Clausifying Description Theorem 1

In this document, we work our way step by step to the set of six clauses to which this theorem gets converted by PROVER9 during the preprocessing stage.

As a first step in clausifying Description Theorem 1, consider the following intermediate form, which results from renaming the bound variables used in our first-order representation. The variable x is renamed to y and the variable F is renamed to x.


 all x (Relation1(x) -> 
   ((exists y (Object(y) & Ex1(x,y) & 
      (all z (Object(z) -> (Ex1(x,z) -> z=y))))) -> 
         (exists w (Object(w) & Is_the(w,x))))).

Next, the formula is rewritten in prenex normal form. This form is semantically equivalent to the previous form, and thus to the original formula.


 all x exists w exists y all z (Relation1(x) -> 
   (( (Object(y) & Ex1(x,y) & 
      ( (Object(z) -> (Ex1(x,z) -> z=y))))) -> 
         ( (Object(w) & Is_the(w,x))))).

The next step is to transform the matrix of this formula into conjunctive normal form by truth-functional equivalence transformations.


 all x exists w exists y all z (
   (-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(z) | Object(w)) &
   (-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(z) | Is_the(w,x)) &
   (-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,z) | Object(w)) &
   (-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,z) | Is_the(w,x)) &
   (-Relation1(x) | -Object(y) | -Ex1(x,y) | z != y | Object(w)) &
   (-Relation1(x) | -Object(y) | -Ex1(x,y) | z != y | Is_the(w,x)) ).

Next PROVER9 eliminates the universal and existential quantifiers. An universal quantifier can simply be dropped. For an existential quantifier, a Skolem function is introduced. This is a function that takes as arguments the variables bound by the universal quantifiers preceding that existential quantifier. In general, the Skolemization results in formulas that are not equivalent to the original. However, the formula that results from Skolemization is satisfiable if and only if the original formula is. Since the automated proof amounts to an indirect proof showing the unsatisfiability of the set of formulas containing the premises and the denial of the conclusion, it is sufficient to preserve satisfiability in the transformations of the formulas. There is no requirement to preserve equivalence. Some of the transformations used in clausifying do preserve equivalence; Skolemization may not.


(-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Object(f2(x))) &
(-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Is_the(f2(x),x)) &
(-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Object(f2(x))) &
(-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Is_the(f2(x),x)) &
(-Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Object(f2(x))) &
(-Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Is_the(f2(x),x)).

As the last step, the conjuncts of the above formula, which is in conjunctive normal form, are separated, yielding the following set of clauses:


-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Object(f2(x)).
-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Is_the(f2(x),x).
-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Object(f2(x)).
-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Is_the(f2(x),x).
-Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Object(f2(x)).
-Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Is_the(f2(x),x).

These are the clauses that PROVER9 will have to draw on when it searches for a proof.