Is it just that $\forall z$ means that this statement could be true for any element,
Yes, exactly.
...and if so what's the difference between $\forall z$ and $\exists z$?
If we only asserted the existence of some particular $z$ such that if $y$ loves $z$, then that particular person $z$ would thus be $x$. But then we are not ruling out that there might be another person, different from $x$, that is also loved by everyone. And we have already asserted the existence of someone (namely, x) who is loved by all. So in that sense, $\exists z$ such that... is reduntant.
We need the universal quantifier for $z$ (to assert a statement $\forall z$) in the second clause to indicate that if there is any $z$ (which means that the claim that follows - as it relates to $z$, is true for every z) $z$ such that $L(y, z)$, then any/every such $z$ must be $x$, since there is exactly one person, namely $x$, who is loved by all $y$. I.e., for every $z,$ if every y loves z, then z must be x: i.e., that $z$ is not anyone other than $x$. This gives us that $x$ (whose existence we asserted at the start) is therefore the one unique person loved by all.
Now, just one oversight to "clean up" your expression, which you state as:
$$∃x(\forall y L(y,x))\land ∀z(∀y(L(y,z))⟹x=z)$$
But here we have two independent clauses that creates a problem, because in your second clause, you have $x$ appear outside the scope of its quantifier. I.e., it is a free, unquantified varible.
So we want the scope of $\exists x$ to persist over the entire statement, hence the square brackets below.
That is, $$\exists x \big[\forall y(L(y, x))\land \forall z(\forall y(L(y, z)) \rightarrow z = x)\big]$$
Examples and counterexamples.
Consider the following statements:
- All of my fish are ugly and blow bubbles.
- All of my fish are ugly, and all of my fish blow bubbles.
These two statements are clearly equivalent. This is an example of $$\forall x(P(x) \wedge Q(x)) \equiv \forall x P(x) \wedge \forall x Q(x)$$
where here the quantifiers range over my fish, $P(x) \equiv$ "$x$ is ugly" and $Q(x) \equiv$ "$x$ blows bubbles".
Now consider the following two statements:
- All of my fish are either goldfish or koi.
- All of my fish are goldfish, or all of my fish are koi.
So long as not all of my fish are goldfish, and not all of my goldfish are koi, the first statement will be true while the second will be false. This is an example of
$$\forall x(P(x) \vee Q(x)) \not \equiv \forall x P(x) \vee \forall x Q(x)$$
where the quantifiers range over my fish, $P(x) \equiv$ '$x$ is a goldfish' and $Q(x) \equiv$ '$x$ is a koi'.
There are similar statements that illustrate the analogous (in)equivalences for $\exists$.
Proofs.
A proof that $\forall$ distributes over $\wedge$ is as follows:
$$\begin{align}
\forall x(P(x) \wedge Q(x)) & \Leftrightarrow P(x) \wedge Q(x) & (\forall\text{-elimination})\\
& \Leftrightarrow P(x)\ \text{and}\ Q(x) & (\wedge\text{-elimination})\\
& \Leftrightarrow \forall xP(x)\ \text{and}\ \forall xQ(x) & (\forall\text{-introduction})\\
& \Leftrightarrow \forall xP(x) \wedge \forall xQ(x) & (\wedge\text{-introduction})
\end{align}$$
Sometimes $\forall$-elimination is called 'generalisation' or something similar... your notation and terminology may differ, but the steps in the proof should be roughly the same.
There is a similar proof for $\exists$.
Abstract nonsense.
The category theorist in me wants to give another proof: quantifiers are really functors (between preorder categories of formulae with certain free variables, ordered by entailment) which satisfy a string of adjunctions $\exists \dashv {*} \dashv \forall$. Now 'or' is a coproduct and 'and' is a product, and since right-adjoints preserve limits (and left-adjoints preserve colimits), we must have that $\forall$ distributes over $\wedge$ and $\exists$ distributes over $\vee$.
Best Answer
Yes.
One way to prove this is by using a proof tree. You start with the negation of the formula in question then apply a series of contradiction hunting rules to show that, no matter what, that negation is false, like so:
This tree was generated here.