# Forming empty clause in Resolution in propositional logic.

Let $F$ be a formula in CNF. Let there be a variable in $F$ called $p$ which only comes up positively( there is no $\lnot p$ in any clauses). Show that if the formula is unsatisfiable ,then we can find the empty clause using resolution by ignoring any clause where $p$ occurs.

So my idea basically is that setting $p=1$ wouldnt harm other formulas since it only comes up positively and so those clauses would be satisfied and if the formula would be unsatisfiable it would only depend on the clauses which dont have $p$, but i need some tips on how i could prove this formally.

For any clause set $\Gamma$ and any variable $P$: if $P$ occurs only positively in $\Gamma$, then $\Gamma$ is satisfiable if and only if $\Gamma_P$ is satisfiable, where $\Gamma_P$ is the result of removing all clauses that contain $P$.
But yes, to prove this, you follow your idea: We know that $\Gamma$ is satisfiable if and only if either $\Gamma$ is satisfiable by setting $P$ to True, or $\Gamma$ is satisfiable by setting $P$ to False. Since by setting $P$ to True we satisfy all clauses that contain $P$, and therefore only need to satisfy $\Gamma_P$ in order to satisfy $\Gamma$ as a whole, while by setting $P$ to False we still have all clauses left to satisfy (and those that contain $P$ are now even harder to satisfy), it is strictly harder to satisfy $\Gamma$ by setting $P$ to False as compared to setting $P$ to True (put differently: whatever assignment you give to the variables other than $P$ that will satisfy all clauses in $\Gamma$ with $P$ removed from those clauses will of course also satisfy all clauses in $\Gamma_P$).
So indeed, $\Gamma$ is satisfiable if and only if $\Gamma_P$ is satisfiable, which of course means that $\Gamma$ is unsatisfiable (i.e. Empty set can be derived) if and only if $\Gamma_P$ is unsatisfiable.
By the way, such a $P$ is called a pure literal, so if you do Resolution, it is a good strategy to see if you have any pure literals (a pure literal can of course also be a case where you only have $\neg P$ for some atomic variable $P$ but no $P$'s.