Why don't Standardize variables just violate completeness of resolution

Question

I have been reading some notes on converting first order logic (FOL) sentences to conjunctive normal form (CNF), and then performing resolution.

One of the steps of converting to CNF, is Standardize variables.

I have been searching to find an why complete condition of resolution algorithm violate and soundness doesn't violate, if i don't standardize variables.

anyone could add details why just violate completeness, and soundness is remain?

Answer 1

Here is an example that may help you visualize this. Suppose your theory is

(for all X : nice(X)) or (for all X : smart(X)) (1)

which, if you standardize apart, will result in the CNF:

nice(X) or smart(Y)

that is, everybody in a population is nice, or everybody in a population is smart, or both.

Dropping standardize apart will produce a CNF

nice(X) or smart(X)

which is equivalent to

(for all X : nice(X) or smart(X)) (2)

that is, for each individual in a population, that individual is nice, or smart, or both.

This theory (2) is saying less, it is weaker, than the original theory (1), because it admits a situation in which it is not true that everybody is nice, and it is not true that everybody is smart, but it is true that each individual is one or the other or both. In other words, (2) does not imply (1), but (1) implies (2) (if the whole population is nice, then each individual is nice; if the whole population is smart, then each individual is smart; therefore, each individual is either nice or smart). The set of possible worlds accepted by (2) is strictly larger than the set of possible worlds accepted by (1).

What does this say about completeness and soundness?

Using (2) is not complete because I can show you a counter-example of a true theorem in (1) that is not proven true when using (2). Consider the theorem "If John is not nice but smart, then Liz is smart". This is true given (1) because if the whole population shares one of those two qualities, then it must be "smart" since John is not nice, so Liz (and everyone else) must also be smart. However, given (2) this is not true anymore (it could be that Liz is nice but not smart, and everybody else is one or the other, which still would be ok given (2)). So I can no longer prove a true theorem using (2) (after dropping standardize apart), and therefore my inference is not complete.

Now suppose I prove some theorem T to be true, using (2). This means T holds in every possible world in which (2) holds, including the sub-set of them that hold in (1) (according to the third paragraph above from here). Therefore T is true in (1) as well, so performing inference using (2) is still sound.

In a nutshell: when you do not standardize apart, you "join" statements about entire domains (populations) and make them about individuals, which will be weaker and will not imply some facts that were implied before; they will be lost and your procedure will not be complete.