Prove that any truth function $f$ can be represented by a formula $φ$ in cnf by negating a formula in dnf

Question

Could anyone check if my proof is ok please?

Prove that any truth function $f$ can be represented by a formula $φ$ in cnf by negating a formula in dnf representing a suitably chosen truth function related to $f$ and manipulating the resulting formula. (cnf means conjunctive normal form, likewise for dnf)

In my textbook I have already proven that, the set $\{\lnot, \land, \lor\} $ is functionally complete/adequate if we construct a dnf for any given truth function, so I am going to assume that dnf does represent any given truth function.

Proof by structural induction:

Base case: the most basic dnf is a single propositional variable, let's call it $φ$. Negating $φ$ gives us $\lnot φ$, which is a literal - cnf fulfilled.

Then there are only 3 other forms of cnf we would see. 1) $φ=\phi\land\psi$, 2) $φ=\phi\lor\psi$, 3) $φ=\lnot\phi$. Induction hypothesis (IH): that $\phi$ and $\psi$ can be turned into cnf by negating them.

1) $φ=\phi\land\psi$: negating $φ$ we get $\lnot(\phi\land\psi)$, then by DeMorgan we get $\lnot\phi\lor\lnot\psi$. By IH $\phi$ and $\psi$ can be turned into cnf by negating them, which is exactly what $\lnot\phi$ and $\lnot\psi$ are.

But then $\phi$ and $\psi$ can only be literals since they are within a conjunction in a dnf, thus if $\phi$ and $\psi$ can be transformed into cnf, we have achieved our goal. ie. This is a 1 clause cnf.

2) $φ=\phi\lor\psi$: by negating $φ$ then applying DeMorgan we get $\lnot\phi\land\lnot\psi$. Again by the IH $\phi$ and $\psi$ can be transformed into cnf, cnf fulfilled.

3) $φ=\lnot\phi$: negating $φ$ gives us $\lnot\lnot\phi$, but if $φ$ is a negation then by def of dnf $\lnot\phi$ can only be a literal. By applying double negation $\phi$ is still a literal, cnf fulfilled.

Thus it has been shown that all forms of truth function representing dnf can indeed be transformed into their corresponding cnf.

---

Things I am not sure about:

1. I started off with the basic form of dnf instead of cnf, is this the right way to do structural induction?

2. Is it legit for me to distinguish dnf by only the 3 forms?

3. I am not very comfortable with how I applied IH; especially with 1) and 3).

Answer 1

As an informal proof, it is adequate, but you are right that your use of structural induction is somewhat vague. The issue is that it is not very clear how you are inductively defining the set of DNF formulas.

A naive view on what the inductive structure you're doing structural induction over corresponds to an inductively defined set that looks something like the following:

Let $F$ be the smallest set of formulas $X$ such that 1) $X$ contains the atomic propositions, 2) if $\varphi\in X$ and $\psi\in X$ then $\varphi\land\psi\in X$, 3) if $\varphi\in X$ and $\psi\in X$ then $\varphi\lor\psi\in X$, and 4) if $\varphi\in X$ then $\neg\varphi\in X$.

But this is just the set of all formulas (which is inductively defined).

We could fix the previous definition as follows:

Let $F$ be the smallest set of formulas $X$ such that 1) $X$ contains the atomic propositions, 2) if $\varphi\in X$, $\psi\in X$, and $\varphi$ and $\psi$ are either conjunctions or literals then $\varphi\land\psi\in X$, 3) if $\varphi\in X$ and $\psi\in X$ then $\varphi\lor\psi\in X$, and 4) if $\varphi\in X$ and $\varphi$ is atomic then $\neg\varphi\in X$.

I believe this would work, but this is a more sophisticated form of inductive definition. (From a type theoretic perspective, the first definition corresponds to an algebraic data type, while the second requires a touch of dependent types. You may find this answer which touches on formalizing inductive types in type theories a bit interesting.) With this definition though, you would technically need to explicitly do a case analysis in your $\land$ case since the conjuncts can still be conjunctions, e.g. $((A\land B)\land(C\land D))$, similarly for the $\lor$ case.

If I were going to prove this informally, I'd probably say something like: Any Boolean function can be represented by a DNF formula, so represent the negation of $f$ as a DNF formula $\psi$, then $\varphi=\neg\psi$ is a formula that represents $f$. Let $\psi = \bigvee_{i=0}^m\bigwedge_{j=0}^n p_{i,j}$ where $\{p_{i,j}\}_{i\in \{0,\dots,m\},j\in\{0,\dots,n\}}$ is a collection of literals. (The $p_{i,j}$ arguably need to satisfy some distinctness conditions which I won't bother with. It is perhaps better to talk about a finite set of finite sets of literals and $\bigvee$/$\bigwedge$ operating on finite sets.) Then $$\begin{align} \varphi & = \neg\psi \\ & \equiv \neg\bigvee_{i=0}^m\bigwedge_{j=0}^n p_{i,j} \\ & \equiv \bigwedge_{i=0}^m\neg\bigwedge_{j=0}^n p_{i,j} \\ & \equiv \bigwedge_{i=0}^m\bigvee_{j=0}^n \neg p_{i,j} \end{align}$$ Let $q_{i,j}=\neg p_{i,j} = \begin{cases}a_{i,j}, & \text{if}\ p_{i,j}=\neg a_{i,j}\\ \neg p_{i,j}, & \text{otherwise}\end{cases}$, then $\{q_{i,j}\}_{i\in \{0,\dots,m\},j\in\{0,\dots,n\}}$ is a collection of literals and $\varphi$ is equivalent to a formula in CNF, namely $\bigwedge_{i=0}^m\bigvee_{j=0}^n q_{i,j}$.

In the above proof, the induction is hidden in the uses of De Morgan's law, but in this case it's an induction over a natural number. That said, another use of induction is hidden in the well-definedness of the notation $\bigvee_{i=0}^m$ and $\bigwedge_{j=0}^n$ which requires at least associativity and arguably unit laws as well. (In my opinion, the cleanest way of handling this is via a structural induction over the set of full binary trees aka free magmas.)

In summary, if you want to do structural induction over a collection, you need to make it clear what that structure is and that structure needs to be inductively defined. For DNF/CNF, it is probably simpler to view them as "layered" or "nested" inductively defined structures that should be handled with nested induction.