Russell's "On Denoting," formalization So, I was reading Russell's paper 'On Denoting' and stumbled upon the (in)famous paraphrase\analysis of the definite description "x was the father of Charles II."
As it is known, Russell's paraphrase is as follows:
"It is not always false of x that x begat Charles II and that x was executed and that 'if y begat Charles II, y is identical with x' is always true of y"
Leaving behind the reasons of why Russell would attempt such paraphrasing endeavour, I attempted to offer a literal formalization. Which I would offer to you to see if it is good or wrong.
$\lnot\forall x\lnot((Cx\wedge Ex)\rightarrow(\forall y(Cy\rightarrow(x=y))$
which should be equivalent to
$\exists x((Cx\wedge Ex)\wedge\forall y(Cy\rightarrow(x=y))$
Where "C" is the predicate that stands for "paternity" and "E" means "to be executed."
I don't know where to point the finger, but I believe something is off in these translations.
 A: In "$x$ was the father of Charles II", the definite description is the phrase "the father of Charles II" and it is phrases like this that Russell wants to explicate. "The father of Charles II" should mean something like "that person $x$ who was Charles II's father", but it could be problematic to use a phrase like that as if it were a noun (perhaps there was no such person or perhaps there were more than one). To describe Russell's proposed solution to this problem formally, let me write $\iota x\phi(x)$ for a term that is intended to denote the unique $x$ that satisfies $\phi(x)$. This is a variable binding construct (like $\forall$ or $\exists$): $x$ is a bound variable rather than a free variable in $\iota x\phi(x)$. So "the father of Charles II" translates to $\iota x\phi(x)$ where $\phi(x)$ denotes "$x$ was a male parent of Charles II" (or "$x$ begat Charles II" in Russell's language). Russell's proposal is that these terms $\iota x \phi(x)$ should be explicated by eliminating them by contextual substition: a formula:
$$\psi(\iota x \phi(x))$$ should be replaced by the formula:
$$\exists x(\psi(x) \land \phi(x) \land (\forall y(\phi(y) \Rightarrow y = x)))$$
(I've used Greek letters rather than your $C$ and $E$, because Russell uses $C$ for something else.)
I.e., we replace "$\psi$ holds of the unique $x$ satisfying $\phi$", by "there exists an $x$ that satisfies $\psi$ and $\phi$ and is the only $x$ that satisfies $\phi$".
A: Your
$\exists x((Cx\wedge Ex)\wedge\forall y(Cy\rightarrow(x=y))$
is basically correct 
(... though I am not sure where the execution part comes in ... and I also think you need to say that $x$ is the father of Charles II by either redefining $C(x)$ to '$x$ is father of Charles II' or (better) use $P(x,c)$: for $x$ is father of $c$, where $c$ denotes Charles II ...)
Anyway, the crucial element here is how to symbolize 'the', meaning that you want to say that there is exactly one object satisfying some property.  In general, where that property is formalized by the formula $\varphi(x)$, you would use:
$\exists x (\varphi(x) \land \forall y (\varphi(y) \rightarrow y = x))$ (just as you did)
or:
$\exists x (\varphi(x) \land \neg \exists y (\varphi(y) \land \neg y = x))$
or:
$\exists x \forall y (\varphi(y) \leftrightarrow y = x))$
