# Proof that propositional resolution is refutation complete

I am studying theoretical computer science and I am in the part about resolution in propositional calculus. I was reading a theorem (and its proof) that propositional resolution is refutation complete, but I could not fill a particular detail.

The theorem is:

Refutational Completeness of Propositional Resolution. The resolution method in propositional calculus is refutation complete, i.e., a set of propositional clauses $$S$$ is unsatisfiable if and only if the empty clause can be deduced from $$S$$ by application of the cut rule and the simplification rule.

The sketch of the proof given is:

Proof Sketch.

($$\Leftarrow$$). By correction we have that if $$\square$$ is deduced from $$S$$ then $$S$$ is unsatisfiable.

($$\Rightarrow$$). First you need to show that if $$S$$ is inconsistent and the set of propositional symbols that occur in the clauses of $$S$$ are $$\{p_1, \ldots, p_n \}$$, then it is possible to obtain from $$S$$ by resolution a set of clauses $$S'$$ such that only the propositional symbols $$\{p_1, \ldots, p_{n-1} \}$$ occur in $$S'$$. The proof will then follow by induction on the number of propositional symbols that occur in $$S$$. Details are left as exercise.

The cut rule and the simplification rule were defined previously as:

Cut Rule. Let $$p \lor l_1 \lor \ldots \lor l_n$$ and $$\lnot p \lor l'_1 \lor \ldots \lor l'_m$$ be two propositional clauses. Then the clause $$l_1 \lor \ldots \lor l_n \lor l'_1 \lor \ldots l'_m$$ is inferred from the two previous ones by the cut rule.

Simplification Rule. Let $$p \lor p \lor l_1 \lor \ldots \lor l_n$$ be a propositional clause. Then, the clause $$p \lor l_1 \lor \ldots \lor l_n$$ is inferred from the one before by the simplification rule. Equally, $$\lnot p \lor l_1 \lor \ldots \lor l_n$$ is inferred from $$\lnot p \lor \lnot p \lor l_1 \lor \ldots \lor l_n$$ by the simplification rule.

To obtain the set $$S'$$ from $$S$$ my idea was to first notice that since $$S$$ is unsatisfiable, there is at least one propositional symbol $$p_i$$ such that both $$p_i$$ and $$\lnot p_i$$ appear in clauses of $$S$$. Without loss of generality, we can assume $$p_i = p_n$$. Then, let $$p_n \lor l_1 \lor \ldots \lor l_n$$ and $$\lnot p_n \lor l'_1 \lor \ldots \lor l'_m$$ be two clauses of $$S$$ and notice that we can apply the cut rule to obtain only $$l_1 \lor \ldots l_n \lor l'_1 \lor \ldots l'_m$$. We can proceed in this way as many times as necessary and obtain a set $$S'$$ such that only the propositional symbols $$\{p_1, \ldots, p_{n-1}\}$$ appear in $$S'$$.

However, I could not prove that the set $$S'$$ obtained this way is inconsistent. For instance, if $$S = \{p_1 \lor p_2, p_1 \lor \lnot p_2 \}$$, then $$S' = \{p_1\}$$ and I don't see how I can derive $$\square$$.

What am I missing? How can I fill the details in this proof? Thanks in advance!

There is an error in the example: $$S = \{p_1 \lor p_2, p_1 \lor \lnot p_2 \}$$ is actually satisfiable. Every interpretation $$I$$ that sends $$p_1$$ to $$true$$ actually works.
With this in mind, notice that if $$S$$ is unsatisfiable, then for every proposition symbol $$p_i$$ we may have both $$p_i$$ and $$\lnot p_i$$ occurring in $$S$$ or only one of them. Construct the unsatisfiable subset $$S_n$$ of $$S$$ that omits the propositional symbols $$p_i$$ such that only one of $$p_i$$ or $$\lnot p_i$$ occur in $$S$$. For instance, if $$S = \{p_1 \lor p_2, p_1 \lor \lnot p_2, \lnot p_1, p_3 \lor p_1 \}$$, then $$S_n = \{p_1 \lor p_2, p_1 \lor \lnot p_2, \lnot p_1\}$$.
We can then proceed as you described, using the cut rule to combine every pair $$p \lor l_1 \lor \ldots \lor l_n$$ and $$\lnot p \lor l'_1 \lor \ldots \lor l'_m$$ and replace them by $$l_1 \lor \ldots \lor l_n \lor l'_1 \lor \ldots \lor l'_m$$. After that we need to apply the simplification rule to the new rules. We can then form the set $$S_{n-1}$$ that only contains the propositional symbols $$\{p_1, \ldots, p_{n-1} \}$$ and also satisfies the property that we have both $$p_i$$ and $$\lnot p_i$$ occuring in the clauses of $$S_{n-1}$$, for every $$1 \leq i \leq n-1$$. This property will allow us to continue this process of eliminating one propositional symbol at a time until we obtain the empty clause $$\square$$.