Why Does Order of Negation Matter in First Order Logic Resolution?

Question

Consider the situation in which we have $f(A)$ as a given and are attempting to show that $\exists x f(x)$.

Using resolution, we negate the conclusion, convert everything to CNF, and attempt to derive a contradiction.

This can be done as follows:

$$\neg \exists x f(x)$$ $$\forall x \neg f(x)$$

We can then use the resolution rule, using $[x/A]$ as a unifier, to derive a contradiction. Thus we have proved that our premise logically entails our conclusion, using resolution.

This all makes sense to me. What does not make sense is why if we convert to CNF BEFORE negating, we end up with an un-provable conclusion. Consider the following steps:

$$f(B)$$ $$\neg f(B)$$ Where B is a skolem constant derived using existential instantiation. Clearly, we now cannot derive a contradiction using solely $f(A)$ and $\neg f(B)$

Does this stem from the fact that the conversion from FoL to CNF does not result in a logically equivalent statement, but rather results in an equisatisfiable statement?

My intuition tells me that the second method is wrong, and that we must negate the conclusion before the translation to CNF. If possible, I'm looking for an explanation of WHY this is, and if possible, further literature on the subject.

Answer 1

This has been an interesting question, though figuring out how to formulate an answer wasn't trivial to me. I would be glad to see a more formal answer. But here it goes:

Let me first clarify that my answer regards formulas in prenex normal form (PNF). But that's ok, because every formula can be converted to an equivalent PNF and back.

A skolem normal form, $\text{Sk}(\phi)$, of a formula $\phi$ which is in PNF, is not equivalent to $\phi$, but is equi-satisfiable with it. The reason why they are not equivalent is because the two formulas "live" in different "worlds" (models). Skolemization eliminates existentials by introducing new uninterpreted constants. They are uninterpreted in the sense that they do not make sense in the original model. So in a way, they are new abstract objects, but they accept an interpretation (a "mapping" to objects of the original model) so that the skolemized formulas hold in a model if there is a (possibly different) model in which the original formula holds.

As a side note, here $\text{Sk}(-)$ denotes conversion of the input into skolem normal form (SNF). However, this is not exactly a function, because there are many SNFs of a formula in PNF. But which SNF we take does not matter, so I will abuse notation and write $\text{Sk}(-)$.

So, we want to prove $\{\Sigma,\neg\phi\}$ inconsistent (and hence not satisfiable). For technical reasons, we decide that it's better to first convert these formulas into CNF (a process that, among other transformations that it applies, it also skolemizes the input formulas). In my abusive notation, this would mean that we "move" to this extended model and try to prove inconsistent the set $\text{Sk}(\{\Sigma,\neg\phi\}) = \{\text{Sk}(\Sigma),\text{Sk}(\neg\phi)\}$. Here it becomes clear why negation is applied first and then skolemization comes.

The resolution part of the algorithm works with $\text{Sk}(\{\Sigma,\neg\phi\})$ and the result will hold for $\{\Sigma,\neg\phi\}$. These two sets of formulas are connected with a specific relation: equi-satisfiability. So, if the latter is inconsistent (and hence unsatisfiable), the first is also unsatisfiable.

Now, note that $\text{Sk}(\neg\phi)\not\equiv\neg\text{Sk}(\phi)$. In mathematical terminology, negation and skolemization are neither commutative nor congruent with respect to logical equivalence, if viewed as operations over PNF formulas. Put differently, it matters which of the two operations we apply first, because one order might return a different formula that is not even logically equivalent to the formula you'd get with another order.

Therefore, you cannot apply resolution on $\{\text{Sk}(\Sigma),\neg\text{Sk}(\phi)\}$ and expect that you will get correct results. This is because $\{\text{Sk}(\Sigma),\neg\text{Sk}(\phi)\}$ does not retain equisatisfiability with the original set $\{\Sigma,\neg\phi\}$. In other words, in the general case, $\{\text{Sk}(\Sigma),\neg\text{Sk}(\phi)\} \neq \text{Sk}(\{\Sigma,\neg\phi\})$.

Informally, negating a skolemized formula is not equivalent with negation of the original formula. The skolemized formula lives in a different model and therefore, with this order of application, you negate a formula that possibly refers to some alien constant which is not part of the original model.

Another problem that arises if you negate after skolemizing: Negation might result in some variables to become existentially quantified. These variables stay un-skolemized, since the skolemization phase happened just before. How should the algorithm handle these existentials?

Answer 2

The existential quantifier is effectively an arbitrary disjunction over all entities in the domain.   $\exists x~f(x)$ can be considered to be saying $(f(a)\vee f(b)\vee\cdots)$.   Likewise the universal quantifier is an arbitrary conjunction, and quantifier duality is thus an extension of deMorgan's Rules.

So when we use this concept to express $f(a)\wedge \neg\exists x~f(x)$ in conjunctive normal form we obtain:

$$f(a)\wedge \neg \exists x~f(x)\\f(a)\wedge\neg(f(a)\vee f(b)\vee\cdots)\\f(a)\wedge(\neg f(a)\wedge\neg f(b)\wedge\cdots)\\f(a)\wedge\forall x~\neg f(x)$$

Which allows you to represent this by the clause $\{f(a),\neg f(a)\}$ using the skolem function rules.

Using the resolution technique, first the conjunction of antecedents and the negated consequent, must be converted to conjunctive normal form (CNF). In this form, all quantification becomes implicit: universal quantifiers on variables (X, Y, ...) are simply omitted as understood, while existentially-quantified variables are replaced by Skolem functions.

In short $f(a)\wedge\neg\exists x~f(x)$ is not in CNF, so trying to apply skolem replacement will yield invalid results.