I'm trying to show that $∃xDx ∧ ∀x∀y((Dx ∧ Dy) → x=y) ⇔ ∃x∀y(Dy ↔ x=y)$ using logical equivalences. My attempt is as follows:
\begin{align*} ∃xDx ∧ ∀x∀y((Dx ∧ Dy) → x=y) & ⇔ ∃xDx ∧ ∀x∀y(¬(Dx ∧ Dy) ∨ x=y) &&\text{((α → β) ⇔ (¬α ∨ β))} \\& ⇔ ∃xDx ∧ ∀y∀x(¬(Dx ∧ Dy) ∨ x=y) &&\text{(switched quantifiers ∀x∀y)} \\& ⇔ ∀y(∃xDx ∧ ∀x(¬(Dx ∧ Dy) ∨ x=y)) &&\text{(factored out ∀y since no free y in left conjunct)} \\& ⇔ ∀y(∃xDx ∧ ∀x((¬Dx ∨ ∀x¬Dy) ∨ x=y)) &&\text{(De Morgan's law)} \\& ⇔ ∀y(∃xDx ∧ (∀x¬Dx ∨ ∀x¬Dy ∨ ∀xx=y)) &&\text{(distributed ∀x)} \\& ⇔ ∀y(∃xDx ∧ (∀x¬Dx ∨ ¬Dy ∨ ∀xx=y)) &&\text{(removed vacuous quantifier ∀x)} \\& ⇔ ∀y((∃xDx ∧ ∀x¬Dx) ∨ (∃xDx ∧ (¬Dy ∨ ∀xx=y))) &&\text{(distributed ∃xDx)} \\& ⇔ ∀y((∃xDx ∧ ¬∃xDx) ∨ (∃xDx ∧ (¬Dy ∨ ∀xx=y))) &&\text{(rewriting ∀x¬Dx as ¬∃xDx)} \\& ⇔ ∀y(∃xDx ∧ (¬Dy ∨ ∀xx=y)) &&\text{((⊥ ∨ α) ⇔ α)} \\& ⇔ ∃x∀y(Dx ∧ (¬Dy ∨ ∀xx=y)) &&\text{(factored out ∃x since no free x in right conjunct)} \end{align*}
However, I'm not sure how to proceed from here. The target wff (∃x∀y(Dy ↔ x=y)) does not contain $Dx$, but I can't see how to get rid of it, so it's likely that I've misapplied some rule(s).
N.B. My workings include annotations, but they are hidden by the scroll.
PS As Bram28 pointed out in the comments below, step 5 and the last step are incorrect. Apologies for any confusion. For my future refernce:
- $∀$ does not distribute over $\lor$, i.e. $\forall x(P(x) \lor Q(x)) \not\equiv \forall x P(x) \lor \forall x Q(x)$ - the wff on the left says "for any $x$, either $P(x)$ is true or $Q(x)$ is true, or both" (any given $x$ has either $P$ or $Q$, or both), whereas the wff on the right says "it is either the case that $P(x)$ is true for all $x$ or $Q(x)$ is true for all $x$" (all $x$s are $P$ or all $x$s are $Q$, or all $x$s are both $P$ and $Q$).
- The last step should be $\color{blue}{∀y∃x}(Dx ∧ (¬Dy ∨ ∀xx=y))$, i.e. $∀y(∃x(Dx ∧ (¬Dy ∨ ∀xx=y)))$.
The two statements are equivalent, but it is really hard to demonstrate that using first-order logic equivalence principles. Indeed, the 'typical' set of rules (quantifier negation, quantifier distribution, null quantification, swapping quantifiers, replacing variables, various prenex laws) is not sufficient to transform the one statement into the other.
For propositional logic it is easy to find a set of equivalence rules that, together, can demonstrate any equivalence. If we have such a set, we say the set is complete. Indeed, for most textbooks it turns out that the equivalences rules they list for propositional logic are complete.
This, however, is not true for first-order logic. For example, good luck transforming $$\exists x \ P(x) \land \forall x (P(x) \to Q(x))$$ into $$\exists x \ P(x) \land \forall x (P(x) \to Q(x)) \land \exists x \ Q(x)$$ I am pretty sure the 'usual candidates' listed above are simply not sufficient to make this transformation. Indeed, I am pretty sure that the equivalence principles that textbooks list for first-order logic are not complete.
Is there a complete set of equivalence principles for first-order logic? I am pretty sure there is, given that there is a complete set of inference rules for first-order logic, and I am sure there is some way to turn that into a bunch of equivalence rules. For example: we could take a simple inference rule like Modus Ponens, and turn it into an equivalence rule $P \land (P \to Q) \Leftrightarrow P \land (P \to Q) \land Q$ ... but now tyou have to do this for rules involving quantifiers. And since there all kinds of constraints on the use of quantifier inference rules, you will get similar constraints on the use of the corresponding equivalence rules ... In sum, this is not going to look very nice at all!
Now, maybe there is some relative 'clean and easy' but still complete set of equivalence rules for First-order logic, but is there is, I have never sen one, and a question to that effect that I posted here]1 generated no responses.