1
$\begingroup$

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.

$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

As far as I can tell, there are three issues with your proof.

  1. There is a big difference between "$\vdash \varphi$ if and only if $\vdash \lnot\varphi^*$" and "$\vdash \varphi\leftrightarrow \lnot \varphi^*$". The former is what you're asked to prove, but the latter is what you're trying to prove by induction.
  2. Where is the base case in your induction? The base case (atomic formulas) is not so trivial here...
  3. "As for the negation, we derive a formula without negation, then one of the cases follows." This is not at all clear. What do you mean by "derive a formula without negation"?

In fact, the thing you're trying to prove by induction is false. For example, taking $\varphi$ to be $P$, also $\varphi^*$ is $P$, and we certainly don't have $\vdash P\leftrightarrow \lnot P$.

But the statement of the exercise is true in this case. We do have $\vdash P$ if and only if $\vdash \lnot P$, since neither are provable!

Also: are you working with first-order without equality? Because it seems the dual formula of $x = x$ is $x = x$, and we have $\vdash x = x$ but $\not\vdash \lnot (x = x)$...

$\endgroup$
8
  • $\begingroup$ I should have mentioned that the book I am working with is Mendelson's Introduction to Logic. He does not introduce first-order with equality at this moment. $\endgroup$
    – noballpointpen
    Commented May 14, 2023 at 13:46
  • $\begingroup$ It is indeed clear that my statement does not hold for atomic formulas, as you showed with $P$, if it was for atomic formula. Mendelson actually asks you to show that the result does not hold for arbitrary theories. To (1): I know that the statements are different (and now I am ashamed for "proving" the wrong one), but not speaking about the exact proof, I want to ask you: isn't it, indeed, the case that $\vdash \mathscr C \leftrightarrow \neg \mathscr C^*$, if we can derive at least one of the formulas syntactically? If my hypothesis is correct, couldn't we say I proved a weaker statement? $\endgroup$
    – noballpointpen
    Commented May 14, 2023 at 17:44
  • 1
    $\begingroup$ In general, $\vdash \varphi\leftrightarrow \psi$ implies ($\vdash \varphi$ iff $\vdash \psi$), but not coversely. So in trying to prove $\vdash \mathscr{C}\leftrightarrow \lnot \mathscr{C}^*$, you were trying to prove something stronger than what was required (so strong that it's false, in fact!). On the other hand, yes, if $\vdash \varphi$ and ($\vdash \varphi$ iff $\vdash \psi$), then $\vdash \varphi \leftrightarrow \psi$, just because both are provable. $\endgroup$
    – Alex Kruckman
    Commented May 14, 2023 at 19:45
  • 1
    $\begingroup$ (1) By "in general", I meant "for any formulas $\varphi$ and $\psi$". (2) Yes, if you could prove $\vdash \mathscr{C}\leftrightarrow \lnot\mathscr{C}^*$ by induction, then this would answer the question. And indeed your arguments for the inductive steps (except negation!) are correct. But an induction without a base case doesn't prove anything. $\endgroup$
    – Alex Kruckman
    Commented May 14, 2023 at 20:35
  • 1
    $\begingroup$ You're welcome. Strong induction works too, of course. But that means proving the claim for each formula, assuming that the claim holds for all proper subformulas. Atomic formulas have no proper subformulas, so the induction hypothesis is no help here. $\endgroup$
    – Alex Kruckman
    Commented May 14, 2023 at 20:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .