dual formula in predicate calculus

Question

There is an exercise 2.37 in “Introduction to Mathematical Logic” by Elliott Mendelson (6th edition, p. 78).

Let $\mathscr B $ be a wf that does not contain $\Rightarrow $ and $\Leftrightarrow $. Exchange universal and existential quantifiers and exchange $\land $ and $\lor $. The result $\mathscr B^* $ is called the dual of $\mathscr B $. a. In any predicate calculus, prove the following. i. $\vdash\mathscr B $ if and only if $\vdash\lnot\mathscr B^* $. … b. Show that the duality results (a), (i)–(iii), do not hold for arbitrary theories.

I am not sure how to prove (a.i). I proved it using the completeness theorem below. However, the completeness theorem is in further chapters, so I guess I need to prove it by transforming a derivation in the object theory. I have no idea how to do it.

Proof of (a.i). Let $\mathscr B' $ be a wf obtained from $\mathscr B $ by replacing every atomic wf $\mathscr C $ with $\lnot\mathscr C $. Then $\vdash\lnot\mathscr B^* $ is equivalent to $\vdash\mathscr B' $ by De Morgan's laws.

Suppose $\vdash\mathscr B' $. Let $M$ be an interpretation of the predicate calculus and $s$ be a sequence with elements in the domain of $M$. Let $M'$ be an interpretation obtained from $M$ by replacing every relation with its complement. By the soundness theorem, $s $ satisfies $\mathscr B'$ in $M'$, hence $s $ satisfies $\mathscr B$ in $M$. Hence $\mathscr B$ is logically valid. By the completeness theorem, $\vdash\mathscr B$.

By symmetry, $\vdash\mathscr B$ implies $\vdash\mathscr B' $. $\square $

Answer 1

First of all, while you do this in your proof, in your problem description you should define what $\mathscr B' $ stands for, and that you need to show that $\vdash\mathscr B' $ if and only if $\vdash\lnot\mathscr B^* $

Do this by induction on the syntactical structure of $\mathscr B $:

Base: $\mathscr B = A$ for some atomic $A$. Then $\mathscr B' = \neg A$, and $\mathscr B^* = A$, hence $\neg \mathscr B^* = \neg A$, which is exactly $\mathscr B'$, so the claim trivially holds.

Step: We have to consider 4 cases:

1. $\mathscr B = \mathscr B_1 \land \mathscr B_2$ for some formulas $\mathscr B_1$ and $\mathscr B_2$

2. $\mathscr B = \mathscr B_1 \lor \mathscr B_2$ for some formulas $\mathscr B_1$ and $\mathscr B_2$

3. $\mathscr B = \forall x \mathscr B_1$ for some variable $x$ and $\mathscr B_1$

4. $\mathscr B = \exists x \mathscr B_1$ for some variable $x$ and $\mathscr B_1$

By inductive hypothesis, the claim holds for $\mathscr B_1$ and $\mathscr B_2$, i.e we have:

$\vdash\mathscr B_1' $ if and only if $\vdash\lnot\mathscr B_1^* $

and

$\vdash\mathscr B_2' $ if and only if $\vdash\lnot\mathscr B_2^* $

I'll prove 1, so you get the idea, and I'll leave the others to you:

We have:

$\vdash\mathscr B' $ if and only if (since $\mathscr B = \mathscr B_1 \land \mathscr B_2$)

$\vdash (\mathscr B_1 \land \mathscr B_2)' $ if and only if (by definition of $'$)

$\vdash \mathscr B_1' \land \mathscr B_2' $ if and only if (here you'll need some Lemma regarding the power of your syntactical proof system ... completeness would work of course)

$\vdash \mathscr B_1' $ and $\vdash \mathscr B_2' $ if and only if (Inductive hypothesis)

$\vdash\lnot\mathscr B_1^* $ and $\vdash\lnot\mathscr B_2^* $ if and only if (again some Lemma regarding $\vdash$ needed ...)

$\vdash\lnot\mathscr B_1^* \land \lnot\mathscr B_2^* $ if and only if (again some Lemma regarding $\vdash$ needed ...)

$\vdash\lnot(\mathscr B_1^* \lor \mathscr B_2^*) $ if and only if (by definition of $*$)

$\vdash\lnot(\mathscr B_1 \land \mathscr B_2)^* $ if and only if (since $\mathscr B = \mathscr B_1 \land \mathscr B_2$)

$\vdash\lnot\mathscr B^* $

So yes, the fact that they use $\vdash$ makes this annoying, because now you need to know/prove something about your proof system. If it is complete, you're all set of course, but what would have made this problem much more straightforward is if they would have simply asked to prove that $\vDash\mathscr B' $ if and only if $\vDash\lnot\mathscr B^* $, for then every step where I indicated you need a Lemma about the proof system, you can simply refer to the semantics of the operators involved and be done with it: much cleaner!).