4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ You have to formulakte the Ind Hyp carefully ... Let $\varphi$ a formula in NNF with $n$ literals and assume that $P(\varphi)$ holds. Then we consider $\psi$ obtained from $\varphi$ "adding" one more literal and still in NNF : this exclude the case $\psi := \lnot \varphi$ and we are left with $\psi := \varphi \land \ell$ or $\psi := \varphi \lor \ell$. $\endgroup$ – Mauro ALLEGRANZA Apr 23 '15 at 6:39
  • $\begingroup$ Thx for the comment, I've edited my question and included the case for $\psi := \varphi \land \ell$. Is this going in the right direction? $\endgroup$ – user1291235 Apr 23 '15 at 7:32
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Hi thx for your reply. Yes, I understand the principle, but I have problems in formulating a precise (structural) induction proof. $\endgroup$ – user1291235 Apr 23 '15 at 7:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.