¿Cómo simbolizo esta declaración con una descripción definida en lógica de primer orden?

Lo que has escrito no es correcto, porque la x al final no está ligada.

Tu oración es algo difícil de entender, porque es algo raro de decir. Si quiere decir, "Si hay exactamente un Rey de Francia presente, entonces hay exactamente un Rey de Francia presente que es un Rey de Francia presente", entonces podría simbolizarse como:

(∃x)(Px & (∀y)(Py → x = y)) → (∃x)(Px & (∀y)(Py → x = y) & Px)

Esta es una tautología y no implica la existencia de ningún rey, ya sea único o no.

Si cambiamos la descripción indefinida por algún otro predicado, como 'mono', entonces tendríamos, "Si hay exactamente un Rey de Francia actual, entonces el Rey de Francia actual es un mono", entonces simbolizaría como :

(∃x)(Px & (∀y)(Py → x = y)) → (∃x)(Px & (∀y)(Py → x = y) & Mx)

Esto no es una tautología, pero aún así no implica la existencia de reyes o monos.

Es posible que quiera decir algo como "Si en cualquier circunstancia hipotética en la que hay exactamente un Rey de Francia actual, la persona que es en realidad el Rey de Francia actual es el Rey de Francia actual". Entonces, la descripción definitiva en el consecuente implicaría la existencia de un actual Rey de Francia, pero esta sería una construcción bastante extraña. Es más plausible entender la oración como diciendo: "Si hay exactamente un Rey de Francia actual, entonces esa persona es un Rey de Francia actual".

Lo que ha formalizado tal vez podría traducirse en inglés de manera más simple como "El actual rey de Francia es un actual rey de Francia", si desea una oración más complicada, tal vez debería repetir su descripción definitiva dos veces:

∃x(Px & ∀y(Py - -> x = y)) - -> ∃x(Px & ∀y(Py - -> x = y) & Px)

Por supuesto, la oración anterior y la suya son lógicamente equivalentes, y ambas lógicamente equivalentes a

∃x(Px & ∀y(Py - -> x = y))

así que el punto es un poco discutible.