Propositional logic resolution

Question

Let $\Gamma = \{ \neg A, B \land C \implies (A \iff B), B \implies A, C \lor(B \implies \neg C)\}$ be a set of well formed formulas in propositional logic. Prove that it's satisfiable with resolution.

SOLUTION

We can verify that $B \implies A, C \lor(B \implies \neg C)$ (let's call it $\psi$) is a tautology, so with resolution we must prove that we cannot obtain $\Box$ from $\Gamma'=\Gamma - \psi=\{ \neg A, B \land C \implies (A \iff B), B \implies A\}$ (thus proving that $\Gamma$ isn't a contradiction and thus it must have at least one model).

MY QUESTION

Why am I allowed to remove the tautology from the $\Gamma$ and prove that I cannot obtain $\Box$ from just $\Gamma'$? What are the (rigorous) theorems that let us do this? It would seem logic to me to remove a tautology if we were proving satisfiability by using the truth tables, because I know that, since proving that $\Gamma$ is satisfiable means to prove that there is at least one common model for all its formulas, it's the same to have a tautology or not since it only has models. But I have no clue about why we can do the same for resolution.

Answer 1

Resolution is a proof procedure that check for satisfiability of a set of clauses and the Resolution rule is simply a rule of inference that preserves truth.

Thus, Resolution can be used to prove the validity of an argument, applying it to the set of clauses genereated by the premises and the negation of the conclusion. If, after applying the procedure, we find the empty clause, we conclude that the original set of formulas is unsatisfiable, because the empty clause is equivalent to $\bot$ and thus is unsatisfiable.

The key result is the following:

the resolvent $C$ [the clause that we get applying the rule] is satisfiable if and only if the parent clauses $C_1$ and $C_2$ [the pair of clauses to which we apply the rule] are both satisfiable.

When, during the process, we find a pair $\{ p, ¬p \}$, that is the clause $p \lor ¬p$, we discard it exactly because it is a tautology, and thus cannot be unsatisfiable.

Note: a valid argument $\Gamma \vDash \varphi$ has a set $\Gamma$ of premises and a conclusion $\varphi$; if the set is finite: $\{ A_1, \ldots,A_n \}$, this is the same as $A_ \land \ldots \land A_n \vDash \varphi$, and applying the definition of valid this is equivalent to say that $A_ \land \ldots \land A_n \land \lnot \varphi$ is unsatisfiable.