I found that resolution is not complete: what do I miss?

Question

I am a newbie in propositional logic and I am learning by myself. I am reading the book A First Course in Logic : An Introduction to Model Theory, Proof Theory, Computability, and Complexity by Hedman. In this book, it is said that the proof system based on the resolution rule is sound (formula derived using repeatedly the resolution rule are consequence) and complete (any consequence can be derived using repeatedly the resolution rule) for propositional logic with formula in conjunctive normal form. I toyed with some simple examples and found a formula for which a consequence is not derived with the use of the resolution rule. What did I miss?

The example is a formula in conjunctive normal form with two variables $x_1$ and $x_2$. The clauses are $\{ x_1 \}$ and $\{ x_2 \}$. A consequence is $\{ x_1, x_2 \}$ but I cannot see how this can derived with the resolution rule.

The definitions of the book are.

Assignment: let $S = \{ x_1, \dots, x_n \}$ be a set of atomic formulas. An assignment of $S$ is a function $A : S \rightarrow \{ 0, 1 \}$. (Basically, an assignment assign true or false to the atomic formulas.)

The notion of assignment extends to formula. Let $F$ be a formula and $A$ be an assignment. $A(F)$ is the truth value of $F$ when valuated with the assignment. $A$ is said to model $F$ when $A(F) = true$; this denoted $A \vDash F$.

Consequence: Formula $G$ is a consequence of formula $F$ if for every assignment $A$, if $A$ models $F$, then $A$ models $G$ (if $A \vDash F$, then $A \vDash G$). It is denoted $F \vDash G$.

Resolution rule: let $C_1$ and $C_2$ be two clauses. Suppose $x_i\in C_1$ and $\lnot x_i \in C_2$ for some atomic formula $x_i$. The resolvent $R$ is $R = (C_1-\{ x_i \}) \cup (C_2 - \{ \lnot x_i \})$. Then $R$ is derived from $C_1$ and $C_2$. It is denoted $\{ C_1, C_2 \} \vdash R$.

Answer 1

Using different symbols for readibility.

We want to show that:

$P_1, P_2 \vDash P_1 \land P_2$

using Resolution.

We have to consider the premises and the negation of the conclusion, i.e. the three clauses:

$\{ P_1 \}, \{ P_2 \}$ and $\{ \lnot P_1 \lor \lnot P_2 \}$.

Two applications of the resolution rule are sufficient to produce the empty clause.

Resolution is a proof procedure that is complete meaning that:

for every set of premises $Γ$, any formula that semantically follows from $Γ$ is derivable from $Γ$.

In the example above, conclusion $P_1 \land P_2$ follows from premises $P_1$ and $P_2$. Applying the procedure we have derived the empty clause, showing that the set of clauses with the premises and the negation of the original conlusion is unsatisfiable, which amounts to saying that the original conclusion is a consequence of the premises.