Beginner Relational Argument Derivation

Question

I'm getting into relational argument, and I've been trying to derive the statement for a long time. Format might differ a bit.

"The present king of Australia is bad" can be translated as $$ ∃x(Kx \land (∀y(Ky → y = x) \land Bx)) $$ and $$ ∃x(∀y(Ky \Leftrightarrow y = x) \land Bx) $$ Using derivations, show they are equivalent.

My attempt:

1. $ ∃x(Kx \land (∀y(Ky → y = x) \land Bx)) \qquad Premise $
2. $ \qquad ¬∃x(∀y(Ky ↔ y = x) \land Bx) \qquad Reductio $
3. $ \qquad ∀x¬(∀y(Ky ↔ y = x) \land Bx) \qquad 2 \, QN $
4. $ \qquad ¬(∀y(Ky ↔ y = u) \land Bu) \qquad3 \, UI$
5. $ \qquad ¬ ∀y(Ky ↔ y = u) ∨¬Bu \qquad 4\, DeM$
6. $ \qquad ∃y ¬(Ky ↔ y = u) ∨¬Bu \qquad 5 \,QN $
7. $ \qquad Bu → ∃y ¬(Ky ↔ y = u) \qquad 7 \,MI$
8. $\qquad Ki \land (∀y(Ky → y = i) \land Bi) \qquad 1\, EI $
9. $\qquad Ki \qquad 8 \,\land E$
10. $\qquad ∀y(Ky → y = i) \land Bi \qquad 8 \, \land E$
11. $\qquad ∀y(Ky → y = i) \qquad 10\,\land E$
12. $\qquad Bi \qquad 10\, \land E $
13. $ \qquad Kv → v = i \qquad 11\, UI$
14. $ \qquad \qquad Kv \qquad Conditional Proof $
15. $ \qquad \qquad v = i \qquad 13,14 \, E→ $

This is unfinished but how would I complete the derivation?

Answer 1

Long comment

I'm not sure that the Reductio step is necessary...

From premise: $∃x(Kx ∧ (∀y(Ky → y=x) ∧ Bx))$ we may jump directly to step 8) using $(\exists \text I)$ to derive: $Ki ∧ (∀y(Ky → y=i) ∧ Bi)$.

Having $Ki$, by equality axiom, we get $y=i \to Ky$ and thus we have the part: $∀y(Ky \leftrightarrow y=i)$, by $(\leftrightarrow \text I)$.

From it: $∀y(Ky \leftrightarrow y=i) \land Bi$, using $(\land \text I)$.

---

The other direction is similar. From premise: $∃x(∀y(Ky \leftrightarrow y=x) ∧ Bx)$ we get $∀y(Ky \leftrightarrow y=i) ∧ Bi$ and thus from $∀y(Ky \leftrightarrow y=i)$ we get both $∀y(Ky \to y=i)$ and $Ki \leftrightarrow i=i$, from which, using equality axiom: $Ki$.

Now we can put together the parts: $Ki \land (∀y(Ky \to y=i) \land Bi)$.