Recursive function to convert DNF to negated CNF form

Question

I am trying to define a recursive function

$g : DNF \rightarrow CNF$

such that for any propositional formula $\varphi$, $g(\varphi)\equiv \neg\varphi$.

I tried to split that into cases, such as follows:

• If $\varphi=p$ then $g(\varphi)=\neg p$     where $p$ is atomic propositional variable
• If $\varphi=\neg p$ then $g(\varphi)=p$     where $p$ is atomic propositional variable
• If $\varphi=\alpha\vee\beta$, then $g(\varphi)=\neg g(\alpha)\wedge\neg g(\beta)$
• If $\varphi=\alpha\wedge\beta$, then $g(\varphi)=\neg g(\alpha)\vee\neg g(\beta)$
• ...

But for the complex binary connective I am not sure the result is actually a CNF form of $\neg \varphi$, nor I know how to prove it.

Please help me to define such a function and help me to prove it's correctness.

Please advise. Thank you.

Answer 1

You can fix your definition just by removing the negations from the clauses for $\alpha \lor \beta$ and $\alpha \land \beta$. If you define: $$ \begin{align*} g(p) &= \lnot p \\ g(\lnot p) &= p\\ g(\alpha \lor \beta) &= g(\alpha) \land g(\beta) \\ g(\alpha \land \beta) &= g(\alpha) \lor g(\beta) \\ \end{align*} $$ where $p$ denotes an atom and $\alpha$ and $\beta$ are any formulas. Then (1) $g(\phi)$ is well-defined for any $\phi$ that is in DNF (because in a DNF negations only occur in literals) and (2) $g(\phi) \equiv \lnot \phi$, for any $\phi$ in DNF, which you can prove by induction on the size of the DNF formula $\phi$: it is clear in the base cases, when $\phi$ is $p$ or $\lnot p$, and in the inductive steps, if $g(\alpha) \equiv \lnot\alpha$ and $g(\beta) \equiv \lnot \beta$, then you have: $$ g(\alpha \lor \beta) = g(\alpha) \land g(\beta) \equiv \lnot \alpha \land \lnot\beta \equiv \lnot(\alpha \lor \beta) $$ and similarly for $g(\alpha \land \beta)$.