Prove that the disjunctions of all conjucts is a disjunctive normal form

Question

Question:

I am attempting the following exercise from An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof by Peter B. Andrews:

X1408. Prove that if $\mathbf{A}$ is a wff in negation normal form, then the disjunction of all wffs of $\mathscr{C}(\mathbf{A})$ is a disjunctive normal form of $\mathbf{A}$.

My proof starts as follows:

Let $\mathbf{X}$ be the disjunction of all wffs in $\mathscr{C}(\mathbf{A})$. Clearly $\mathbf{X}$ is a dijunction of conjunctions. We only need to show that $\mathbf{X}$ is equivalent to $\mathbf{A}$. We proceed by induction on the construction of A:

Case 1. $\mathbf{A}$ is a literal Then $\mathscr{C}(\mathbf{A})=\{\mathbf{A}\}$ and $\mathbf{X}$ is $\mathbf{A}$.

Case 2. $\mathbf{A}$ has the form $\mathbf{B} \vee \mathbf{C}$. Then $\mathscr{C}(\mathbf{A}) = \mathscr{C}(\mathbf{B}) \cup \mathscr{C}(\mathbf{C})$. By the inductive hypothesis, $\mathbf{B} \equiv \mathbf{Y}$ and $\mathbf{C} \equiv \mathbf{Z}$ where $\mathbf{Y}$ is the disjunction of all wffs in $\mathscr{C}(\mathbf{B})$ and $\mathbf{Z}$ is the disjunction of all wffs in $\mathscr{C}(\mathbf{C})$. Therefore, $\mathbf{A} \equiv \mathbf{X}$ since $\mathbf{X}$ is $\mathbf{Y} \vee \mathbf{Z}$.

Up to this point, I think I have a pretty solid proof, although, I may have missed some details. Mostly I am struggling with Case 3:

Case 3. $\mathbf{A}$ has the form $\mathbf{B} \wedge \mathbf{C}$. Then $\mathscr{C}(\mathbf{A}) = \{ \mathbf{P} \wedge \mathbf{Q} | \mathbf{P} \in \mathscr{C}(\mathbf{B})$ and $\mathbf{Q} \in \mathscr{C}(\mathbf{C})\}$.

I'm stuck as to how to continue from here. Can someone provide some hints?

---

Definitions

A literal is a wff of the form $\mathbf{p}$ or $\mathord{\sim}\mathbf{p}$.

A wff of propositional calculus is in negation normal form iff it contains no propositional connectives other than $\wedge$, $\vee$, or $\mathord{\sim}$, and the scope of each occurrence of $\mathord{\sim}$ is a propositional variable.

The set of conjuncts of a wff $\mathbf{A}$, denoted $\mathscr{C}(\mathbf{A})$, is defined by induction on the construction of $\mathbf{A}$:

1. If $\mathbf{A}$, is a literal, $\mathscr{C}(\mathbf{A}) = \{\mathbf{A}\}.$

2. If $\mathbf{A}$ has the form $\mathbf{B} \vee \mathbf{C}$, $\mathscr{C}(\mathbf{A}) = \mathscr{C}(\mathbf{B}) \cup \mathscr{C}(\mathbf{C})$.

3. If $\mathbf{A}$ has the form $\mathbf{B} \wedge \mathbf{C}$, $\mathscr{C}(\mathbf{A}) = \{ \mathbf{P} \wedge \mathbf{Q} | \mathbf{P} \in \mathscr{C}(\mathbf{B})$ and $\mathbf{Q} \in \mathscr{C}(\mathbf{C})\}$.

EXAMPLE

Let $\mathbf{A}$ be $[[p \vee q] \wedge \mathord{\sim} r] \vee [\mathord{\sim} p \wedge s]$. Then $\mathscr{C}(\mathbf{A}) = \{p \wedge \mathord{\sim} r, q \wedge \mathord{\sim} r, \mathord{\sim} p \wedge s \}$.

Answer 1

Also in the Case 3, i.e. $\mathbf A \equiv \mathbf B \land \mathbf C$, we have to apply the Induction Hypotheses.

We have that, by IH both $\mathbf B$ and $\mathbf C$ satisfy the theorem, i.e. :

$\mathbf B \equiv (B_1 \lor \ldots \lor B_n)$

and

$\mathbf C \equiv (C_1 \lor \ldots \lor C_k)$

where the RHS are DNF (disjunctions of conjuncts of literals) with the "additional" property that both disjunctions contain all wffs of the corresponding $\mathscr C(...)$.

Thus :

$\mathbf A \equiv \mathbf B \land \mathbf C \equiv (B_1 \lor \ldots \lor B_n) \land (C_1 \lor \ldots \lor C_k)$

which, by distributivity, boils down to :

(*) --- $\mathbf A \equiv (B_1 \land C_1) \lor (B_1 \land C_2) \lor \ldots (B_1 \land C_k) \lor \ldots \lor (B_n \land C_k)$.

All $B_i$ and $C_j$ are conjunctions of literals; thus the formula is in DNF.

But the "additional" property assures us that the $B_i$ ara all formulae in $\mathscr C(\mathbf B)$, and the same for $\mathscr C(\mathbf C)$.

Thus the formula (*) is a DNF of $\mathbf A$ which is "made with" the disjunction of all formulae in $\mathscr{C}(\mathbf{A}) = \{ \mathbf{P} \wedge \mathbf{Q} | \mathbf{P} \in \mathscr{C}(\mathbf{B})$ and $\mathbf{Q} \in \mathscr{C}(\mathbf{C})\}$.