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.