Equivalent way to write existential quantifier?

Question

Let $L(x,y)$ be the statement, "$x$ loves $y$."

If the universe U is the set of all people,

can the statement, "There is exactly one person whom everybody loves."

or, equivalently (according to my textbook): $∃x[∀y(L(y,x)) ∧ ∀z(∀y(L(y,z) → z=x)]$

be written as (my answer):

[($∃x∀yL(y,x)) ∧ (∀z∃y¬L(y,z))] \mbox∣~ x≠z, z∈U$ ?

The original statement is the answer from my textbook, which I think seems pretty weird. That's why I'm trying to rewrite it.
So, if my answer is not a 'better' way to write "There is exactly one person whom everybody loves.", what is the most logical way to write this statement?

Answer 1

The statement from the book $$\exists x [ \forall y L(y,x) \land \forall z ( \forall y L(y,z) \rightarrow z = x ) ]$$

is a good way to express this. To see this you might write the property of a person to be loved by everyone as $$P(x) := \forall y L(y,x)$$

Then the statement becomes $$\exists x [ P(x) \land \forall z ( P(z) \rightarrow z = x ) ]$$

which means that there is a person $x$ with property $P$, and for any person $y$ with property $P$, that person $y$ must already be $x$.

This might further be abbreviated $$\exists! x P(x)$$

Answer 2

I would suggest: ∃x∀yL(y,x) ∧ ∀z((x≠z)→(∃y¬L(y,z)))

sounds right?

Answer 3

$$\color{red}(\exists \color{red}x~\forall y~ Lyx\color{red}) \land (\forall z~\exists y \lnot Lyz) \text{ s.t. } \color{red}x \ne z$$

Look at the red parts. The first $x$ is inside the parenthesis (quantified), the second is outside (unquantified). The second $x$, grammatically, refers to a different variable than the first due to how you wrote it.

(Btw ignore the complaints about s.t., it is well understood and fine to use if done grammatically correctly).

Here are some ways to transform the formula:

$$\exists x~\bigg( (\forall y ~ Lyx) \land (\forall z~\forall y ~Lyz \to z = x)\bigg)$$

First it would appear you'd like to use the contrapositive:

$$\exists x~\bigg( (\forall y ~ Lyx) \land (\forall z~\forall y ~ z \ne x \to \lnot Lyz )\bigg)$$

Since $x \ne z$ doesn't reference $y$, the $\forall y$ can be moved (this is a formula from the prenex technique):

$$\exists x~\bigg( (\forall y ~ Lyx) \land (\forall z~z \ne x \to \forall y ~ \lnot Lyz )\bigg)$$

One thing you can also notice is that you have a formula of the form $\forall a Pa \land \forall b Qb$, which can be written $\forall c Pc \land Qc$ :

$$\exists x~\bigg( (\forall w ~ Lwx) \land (\forall w~w \ne x \to \forall y ~ \lnot Lyw )\bigg)$$

$$\exists x~\bigg( \forall w ~ (Lwx \land (w \ne x \to \forall y ~ \lnot Lyw ))\bigg)$$

There's other manipulations you can do, but more big picture, there are a lot of ways to write "the predicate $P$ is inhabited exactly once". One way attributed to Dijkstra is as $\exists x (\forall y~P(y) \text{ iff } x = y)$, which in your case becomes:

$$\exists x (\forall y~(\forall z ~ Lzy) \text{ iff } y = x)$$