Satisfiability proof of formulas with pure literals Let $\varphi$ be any propositional formula in negation normal form (NNF). A literal $\ell$ is pure in a formula $\varphi$, if the complement of $\ell$, $\ell^c$, does not occur in $\varphi$, where $\ell^c$ is $b$ if $\ell$ is $\neg b$ and $\ell^c$ is $\neg b$ if $\ell$ is $b$. 
I have to prove that: If $\varphi$ contains only pure literals, then $\varphi$ is satisfiable.
I decided to prove this by structural induction over the definition of well formed NNF formulas:
Let $P(\varphi)$ denote the statement that $\varphi$ is satisfiable.
Base Case: $\varphi = a$. Then $P(\varphi)$ holds trivially because a formula which only consists of a single literal is trivially satisfiable.
Induction Hyp.: Let $\varphi$ be a formula in NNF with $n$ literals and assume $P(\varphi)$ holds.
Step Cases:
$\psi := \varphi \land \ell$: By induction hyp, $\varphi$ does only contain pure litarals and $P(\varphi)$ holds. If we add another pure literal as conjuct to $\varphi$, $\psi$ stays satisfiable, since  $\ell$ is a pure literal (i.e. $\ell^c$ does not occur in $\varphi$).
I believe that until here my proof structure is correct. However, can anybody help me out with the step cases? I know that I need to show it for formulas of the kind $\neg \psi$,$\psi \land \phi$, and $\psi \lor \phi$ Can anybody explain how to proceed with one of the step cases?
 A: Overview: if $\phi$ is a pure formula, in the sense of your question, and $v$ is a propositional variable in $\phi$, define an assignment that makes $v$ true if $v$ is not negated in $\phi$ and makes it false if $v$ is negated. This is possible by the definition of pure formula and will make all the literals in the formula true. As negation only appears in literals in a formula in NNF, your formula is now formed from true literals using conjunction and disjunction, hence it is satisfied by this assignment.
Details of the structural induction: you haven't got the steps in your framework quite right. In the step for $\land$ you have pure formulas $\phi$ and $\psi$ and you have to prove that if $\phi \land \psi$ is pure, then it is satisfiable. You can assume that $\phi$ and $\psi$ are satisfied by the assignment decribed above. Let's say those assignments are $\alpha$ for $\phi$ and $\beta$ for $\psi$. You may also assume that $\phi \land \psi$ is pure, which implies that $\alpha$ and $\beta$ agree on variables that appear free in both $\phi$ and $\psi$, hence $\alpha \cup \beta$ is the assignment described above and it makes both $\phi \land \psi$ hold. Similarly for $\phi \lor \psi$. In the step for $\lnot$, you are given $\phi$ and that $\lnot \phi$ is pure, which means that $\phi$ must be a variable $p$ say. The assignment described above for $\lnot p$, make $p$ false and hence makes $\lnot p$ hold and we are done. 
If you really want to dig into the fine details, my informal description of the satisfying assignment needs to be replaced by a formal definition by recursion over the structure of the formula. That is far more detail than one would usually expect to see in a proof in the literature.
