There is a statement about dual formula in predicate logic:
If $\mathscr B$ is a well-formed formula without conditionals, and $\mathscr B^*$ is obtained by swapping quantifiers and $\land$, $\lor$ connectives, we have: $\vdash \mathscr B$ if and only if $\vdash \neg \mathscr B^*$.
We assume the result that instances of tautologies are derivable.
And here goes my proof:
Suppose $\vdash \mathscr C \leftrightarrow \neg \mathscr C^*$ holds for $r<q$ number of connectives $\land$, $\lor$ and quantifiers.
Case 1. $\mathscr B$ is $(\forall x) \mathscr C$. Then $\neg \mathscr B^*$ is $\neg (\exists x) \mathscr C^*$. We know that $\vdash (\forall x) \mathscr C \leftrightarrow (\forall x) \neg \mathscr C^*$, by inductive hypothesis and $\vdash (\forall x) (\mathscr C \leftrightarrow \neg \mathscr C^*) \rightarrow ((\forall x) \mathscr C \leftrightarrow (\forall x) \neg \mathscr C^*)$. But then we can derive $\vdash \mathscr B \leftrightarrow \neg \mathscr B^*$ with the replacement theorem, since $\vdash (\forall x) \neg \mathscr C^* \leftrightarrow \neg (\exists x) \mathscr C^*$.
Case 2. $\mathscr B$ is $(\exists x) \mathscr C$. Then $\neg \mathscr B^*$ is $\neg (\forall x) \mathscr C^*$. By inductive hypothesis and $\vdash (\forall x)(\mathscr C \rightarrow \neg \mathscr C^*) \rightarrow ((\exists x) \mathscr C \rightarrow (\exists x) \neg \mathscr C^*)$ applied twice, we have $\vdash (\exists x) \mathscr C \leftrightarrow (\exists x) \neg \mathscr C^*$, from which we can derive $\vdash \mathscr B \leftrightarrow \neg \mathscr B^*$ as in 1.
Case 3. $\mathscr B$ is $\mathscr C_1 \land \mathscr C_2$. Then $\neg \mathscr B^*$ is $\neg (\mathscr C^*_1 \lor \mathscr C^*_2)$. With a tautology $((A_1 \leftrightarrow \neg B_1) \land (A_2 \leftrightarrow \neg B_2)) \rightarrow (A_1 \land A_2 \leftrightarrow \neg (B_1 \lor B_2))$, result follows with conjunction introduction from inductive hypotheses.
Case 4. $\mathscr B$ is $\mathscr C_1 \lor \mathscr C_2$. Then $\neg \mathscr B^*$ is $\neg (\mathscr C^*_1 \land \mathscr C^*_2)$. With a tautology $((A_1 \leftrightarrow \neg B_1) \land (A_2 \leftrightarrow \neg B_2)) \rightarrow (A_1 \lor A_2 \leftrightarrow \neg (B_1 \land B_2))$, result follows as in 3.
As for the negation, we derive a formula without negation, then one of the cases follows.
My question: is this proof enough? As this proves somewhat different result, I feel concerned. But intuitively, the dual formula must be logically equivalent to the original in the circumstances of the theorem; this requires completeness theorems, but my proof does not rely on it and is syntactic in nature, so I wonder if this is the correct argument.
EDIT: The book I am working with is Mendelson's Introduction to Logic; should have mentioned it, since the exposition of logic is very different from author to author, as I understand.
EDIT: As it turned out, the proof is incorrect, since I wrongly held in mind that the induction type you use in logic is a strong one (due to Mendelson's vague representation) and therefore I was "light" on handling a base case for some of my proofs. See the selected answer and comments for clarification.