How do I symbolise this statement with a definite description in first order logic?

Question

"If there is exactly one present King of France, then the present King of France is a present King of France"

The part I am confused about is the consequent of the conditional which equals the same definite description to its indefinite description.

Is this correct?: ∃x(Px & ∀y(Py - -> x = y)) - -> Px

Answer 1

What you have written is not correct, because the x at the end is unbound.

Your sentence is somewhat difficult to understand, because it is an odd thing to say. If you mean, "If there is exactly one present King of France, then there is exactly one present King of France who is a present King of France", then it could be symbolised as:

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

This is a tautology and does not imply the existence of any kings, whether unique or otherwise.

If we swapped out the indefinite description for some other predicate, such as 'monkey', then we would have, "If there is exactly one present King of France, then the present King of France is a monkey", then it would symbolise as:

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

This is not a tautology, but it still does not imply the existence of any kings, or of any monkeys.

It is just possible that you mean something along the lines of, "If in any hypothetical circumstance in which there is exactly one present King of France, the person who is actually the present King of France is the present King of France". Then the definite description in the consequent would imply the existence of a present King of France, but this would be a rather odd construction. It is more plausible to understand the sentence as saying, "If there is exactly one present King of France, then that person is a present King of France."

Answer 2

What you have formalized could perhaps be rendered in English more simply as "The present King of France is a present King of France", if you want the more complicated sentence then perhaps you should repeat your definite description twice:

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

Of course, the above sentence and yours are logically equivalent, and both logically equivalent to

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

so the point is a bit moot.