The statement:
If $\mathscr B$ is a formula without conditionals and $\mathscr B^*$ is obtained by exchanging quantifiers and exchanging $\land$, $\lor$ connectives, then $\vdash \mathscr B$ if and only if $\vdash \neg \mathscr B^*$.
I have been bashing my head with the syntactical proof of this theorem. On this site there is a question about it, but the answerer proves the trivial case of conjunction only. The usual approach is with induction. The base case is easy: we don't have $\vdash P$ and we don't have $\vdash \neg P$, so it holds. As for the inductive step; the cases of conjunction and universal quantifier are easy. But the existential quantifier and disjunction cases are not so obvious! Indeed, if we have $\mathscr B$ to be $(\exists x) \mathscr C$, assuming $\vdash \mathscr B$, what is anything we can do? We could get rid of the quantifier, if we knew $x$ is not free in $\mathscr C$, but it is not the case... assuming not $\vdash (\exists x) \neg \mathscr C^*$ for a contradictory argument does not point to anything interesting.
So I constructed some lemmas that seem to prove the statement. It uses the intuitive idea that the negated dual with negated atomics is actually the same as the original formula.
Lemma 1. If $\mathscr B$ is a formula without conditionals, $\mathscr B^*$ is its dual, and $\mathscr B'$ denotes the variant of $\mathscr B$ with a negation sign put before each atomic formula, then $\vdash \neg \mathscr B^* \leftrightarrow \mathscr B'$, so that $\vdash \neg \mathscr B^*$ if and only if $\vdash \mathscr B'$.
Proof. If $\mathscr B$ is an atomic $P$, then its dual is $P$ and its negation is $\neg P$, which is $\mathscr B'$. So it's trivial to see $\vdash \neg P \leftrightarrow \neg P$. Assume the claim holds for $r < q$ connectives and quantifiers.
Case 1. $\mathscr B$ is $(\forall x) \mathscr C$. The negated dual is $\neg (\exists x) \mathscr C^*$. By definition, it's $\neg \neg (\forall x) \neg \mathscr C^*$, which is equivalent to $(\forall x) \neg \mathscr C^*$. Have $\vdash \neg \mathscr C^* \leftrightarrow \mathscr C'$, so $\vdash (\forall x) \neg \mathscr C^* \leftrightarrow (\forall x) \mathscr C'$, so $\vdash \neg \mathscr B^* \leftrightarrow \mathscr B'$.
Case 2. $\mathscr B$ is $(\exists x) \mathscr C$. The negated dual is $\neg (\forall x) \mathscr C^*$, which is equivalent to $(\exists x) \neg \mathscr C^*$. Have $\vdash \neg \mathscr C^* \leftrightarrow \mathscr C'$, so $(\exists x) \neg \mathscr C^* \leftrightarrow (\exists x) \mathscr C'$, so $\vdash \neg \mathscr B^* \leftrightarrow \mathscr B'$.
Case 3. $\mathscr B$ is $\mathscr C_1 \land \mathscr C_2$. The negated dual is $\neg (\mathscr C_1^* \lor \mathscr C_2^*)$, which is equivalent to $\neg \mathscr C_1^* \land \neg \mathscr C_2^*$. Have $\vdash \neg \mathscr C_1^* \leftrightarrow \mathscr C_1'$ and $\vdash \neg \mathscr C_2^* \leftrightarrow \mathscr C_2'$, from which $\vdash \neg \mathscr C_1^* \land \neg \mathscr C_2^* \leftrightarrow \mathscr C_1' \land \mathscr C_2'$ and therefore $\vdash \neg \mathscr B^* \leftrightarrow \mathscr B'$.
Case 4. $\mathscr B$ is $\mathscr C_1 \lor \mathscr C_2$. The negated dual is $\neg (\mathscr C_1^* \land \mathscr C_2^*)$, which is equivalent to $\neg \mathscr C_1^* \lor \neg \mathscr C_2^*$. Have $\vdash \neg \mathscr C_1^* \leftrightarrow \mathscr C_1'$ and $\vdash \neg \mathscr C_2^* \leftrightarrow \mathscr C_2'$. Again $\vdash \neg \mathscr C_1^* \lor \neg \mathscr C_2^* \leftrightarrow \mathscr C_1' \lor \mathscr C_2'$, which is $\vdash \neg \mathscr B^* \leftrightarrow \mathscr B'$.
Case 5. $\mathscr B$ is $\neg \mathscr C$. The negated dual is $\neg \neg \mathscr C^*$. Have $\vdash \neg \mathscr C^* \leftrightarrow \mathscr C'$, which is to say $\vdash \neg \neg \mathscr C^* \leftrightarrow \neg \mathscr C'$, so $\vdash \neg \mathscr B^* \leftrightarrow \mathscr B'$.
Lemma 2. If $\mathscr B'$ denotes a variant of $\mathscr B$ with a negation sign placed before each atomic formula, then $\vdash \mathscr B$ if and only if $\vdash \mathscr B'$.
Proof. We assume that $\mathscr B$ has atomics. Assume $\vdash \mathscr B$. In the proof $\mathscr D_1,\dots,\mathscr D_n$ of $\mathscr B$, each $\mathscr D_i$ is either an axiom, or obtained with MP or Gen. Put a negation sign before each atomic formula, now we obtain a proof of $\vdash \mathscr B'$. Assume $\vdash \mathscr B'$. In the proof of this formula, erase a negation sign from each occurrence of an atomic.
NOTE: I am working with Mendelson's Introduction to Logic. He does not introduce the completeness theorem at this point, so the proof must be syntactial. The theory I use is the basic predicate calculus without equality notion.
Questions:
- These two lemmas seem to prove the statement. Are the lemmas correct, and do they prove the statement about duals in the question?
- If my findings are not correct, could you point me to a correct direction and provide with information what could I do with the disjunction and existential quantifier cases? These seem hopeless to me.
- I am a bit suspicious of rigorousness of the proof of Lemma 2. Could it be improved?