I am trying to prove the following theorem: Every proposition formula is logically equivalent to a formula in CNF.
As a hint, they say that this can by proven by an induction on the structure of the formula, this is what I have done so far:
Basis: A formula with just one symbol (propositional variable) is already in CNF.
Inductive step: A formula with more than 1 symbol has to be in one of these cases:
1) $$\varphi_1 \land \varphi_2$$ 2) $$\varphi_1 \lor \varphi_2$$ 3) $$\varphi_1 \rightarrow\varphi_2$$ 4) $$¬ \varphi_2$$
Let's consider case 1: $\varphi = \varphi_1 \land \varphi_2$, as $\varphi_1$ and $\varphi_2$ have a CNF equivalent formula(by hypothesis, and let's call them $\varphi_1'$ and $\varphi_2'$), then:
$$\varphi = \varphi_1' \land \varphi_2'$$
Which is CNF, and this proves case 1.
Let's consider a formula with the following structure $\varphi = \varphi_1 \lor \varphi_2$. By hypothesis: $\varphi_1$ y $\varphi_2$ have CNF equivalents ($\varphi_1'$ and $\varphi_2'$), then:
$$\varphi = \varphi_1' \lor \varphi_2'$$
where:
$$ \varphi_1' = \psi_1 \land \psi_2 \land ... \land \psi_m$$ $$ \varphi_2' = \delta_1 \land \delta_2 \land ... \land \delta_n$$
And $\psi$ and $\delta$ are clauses of the form: $$\psi_i = L_1 \lor L_2 \lor ... \lor L_{k_i}$$
Applying distributive property on $\varphi_1'$:
$$\varphi_1' \lor (\delta_1 \land \delta_2 \land ... \land \delta_n)$$ $$= (\varphi_1' \lor \delta_1) \land (\varphi_1' \lor \delta_2) \land ... \land (\varphi_1' \lor \delta_n)$$
Doing the following on each $\delta_i$: $$\delta_i \lor \varphi_1' = \delta_i \lor ( \psi_1 \land \psi_2 \land ... \land \psi_m) = (\delta_i \lor \psi_1) \land ... \land (\delta_i \lor \psi_m)$$
Thus, we get
$$ (\delta_1 \lor \psi_1) \land ... \land (\delta_1 \lor \psi_m) \land$$ $$ (\delta_2 \lor \psi_1) \land ... \land (\delta_2 \lor \psi_m) \land$$ $$.$$ $$.$$ $$.$$ $$ (\delta_n \lor \psi_1) \land ... \land (\delta_n \lor \psi_m)$$
This expression is in CNF, which proves case 2.
For case 3, we have $\varphi = ¬\varphi_1$. By hypothesis $\varphi_1$ has a CNF equivalent(which we'll define $\varphi_1'$).
$$ \varphi_1' = \psi_1 \land \psi_2 \land ... \land \psi_m$$
$$\psi_i = L_{i1} \lor L_{i2} \lor ... \lor L_{ik_i}$$
Then:
$$¬\varphi_1=¬(\psi_1 \land \psi_2 \land ... \land \psi_m)$$
$$= ¬\psi_1 \lor ... \lor ¬\psi_m$$
$$ = (¬L_{11} \land ... \land ¬L_{1k_1}) \lor$$ $$ \ \ (¬L_{21} \land ... \land ¬L_{2k_2}) \lor$$ $$.$$ $$.$$ $$.$$ $$ \ \lor (¬L_{m1} \land ... \land ¬L_{mk_m})$$
And here is where I am stuck. I was thinking on rewritting the last term, to get: $\varphi_1''\lor \varphi_2'' \lor ... \lor \varphi_m''$, and using case 2 to end this proof, however I don't know if I can do this. How should I proceed? (and what about the formalisms?)
best regards
