Equivalence within Predicate Logic + Identity

Question

Do these 4 formulae stand equivalent when symbolizing the statement: 'There is exactly one dog'?

1) ∃x∀y(Dy ↔ y=x)

2) ∃x(Dx ∧ ∀y(Dy → x=y))

3) ∃x(Dx ∧ ¬∃y(¬y=x ∧ Dy))

4) ∃xDx ∧ ∀x∀y((Dx ∧ Dy) → x=y)

Answer 1

1) ∃x∀y(Dy ↔ y=x)
There is something_x such that: everything_y is a dog just in case it_y is identical to it_x.

2) ∃x(Dx ∧ ∀y(Dy → x=y))
There is a dog and every dog is identical to it.

3) ∃x(Dx ∧ ¬∃y(¬y=x ∧ Dy))
There is a dog and there is nothing else that is a dog.

4) ∃xDx ∧ ∀x∀y((Dx ∧ Dy) → x=y)
There is a dog, and any two things that are dogs are identical.

Answer 2

Here is a sketch of how to prove the equivalence of these four formulae.

• (i) ⇒ (ii)

  1. ∃x∀y(Dy ⇔ y=x) — premise
  2. ∀y[ (Dy ⇒ y=d) & (y=d ⇒ Dy) ] — by exemplar and pre-emptive biconditional elimination
  3. (Dd ⇒ d=d) & (d=d ⇒ Dd) — universal instantiation
  4. d=d — identity
  5. Dd — conjunctive elimination and modus ponens
  6. (Da ⇒ a=d) & (Da ⇒ a=d) — universal instantiation
  7. Dd & (Da ⇒ a=d) — conjunctive elimination/introduction
  8. ∀y [Dd & (Dy ⇒ y=d)] — universal generalization
  9. ∃x∀y [Dx & (Dy ⇒ y=x)] — existential introduction
     
     

• (ii) ⇒ (iv)

  1. ∃x∀y [Dx & (Dy ⇒ y=x)] — premise
  2. ∀y [Dd & (Dy ⇒ y=d)] — by exemplar
  3. Dd & (Da ⇒ a=d) — universal instantiation
  4. Dd & (Db ⇒ b=d) — universal instantiation again
  5. Dd — conjunctive elimination
  6. ∃x (Dx) — existential introduction
  7. Da ⇒ a=d — conjunctive elimination
  8. Db ⇒ b=d — conjunctive elimination again
  9. (Da & Db) ⇒ (a=b) — modus ponens/conditional introduction/conjunctive introduction/transitivity of equality/etc.
  10. ∀x∀y[(Dx & Dy) ⇒ x=y] — universal generalization
  11. ∃x (Dx) & ∀x∀y[(Dx & Dy) ⇒ x=y] — conjunctive introduction
      
      

• (iv) ⇒ (i)

  1. ∃x (Dx) & ∀x∀y[(Dx & Dy) ⇒ x=y] — premise
  2. ∃x (Dx) — conjunctive elimination
  3. Dd — by exemplar
  4. a=d ⇒ Da — by modus ponens, substitution rule of equality, etc.
  5. ∀x∀y [(Dx & Dy) ⇒ x=y] — conjunctive elimination
  6. (Dd & Da) ⇒ a=d — universal instantiation, twice
  7. Da ⇒ a=d — modus ponens (applying premise 3) and conditional introduction, etc.
  8. Da ⇔ a=d — biconditional introduction
  9. ∀y (Dy ⇔ y=d) — universal generalization
  10. &exists;x ∀y (Dy ⇔ y=x) — existential introduction
      
      

• (ii) ⇔ (iii)
  — essentially by de Morgan's Law, involving some existential/universal quantifier juggling.