# Equivalence within Predicate Logic + Identity

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)

• Yes, they are all logically equivalent. Needless to say, the equivalence doesn't depend on that particular interpretation of 'D'; whatever 'D' means, (1-4) are equivalent. Sep 25, 2013 at 20:19

1) ∃x∀y(Dy ↔ y=x)
There is somethingx such that: everythingy is a dog just in case ity is identical to itx.

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.

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.

• Thanks a lot! Very detailed and explanatory answer, but unfortunately it is beyond my current understanding of Logic (looks pretty straightforward, though). Reminds me of PC + Identity proofs a little; this is metalogical (Sequent Calculus?) stuff, right? I'll come back to this post when I'm more fluent.
– Kas
Sep 29, 2013 at 14:16