A Question about the Equivalences of First-order Logic

Question

I have read an article in Wikipedia. https://en.wikipedia.org/wiki/Prenex_normal_form

---

$(\forall x\phi)\lor\psi\Leftrightarrow\forall x(\phi\lor\psi)$

$(\exists x\phi)\land\psi\Leftrightarrow\exists x(\phi\land\psi)$

$(\exists x\phi)\rightarrow\psi\Leftrightarrow\forall x(\phi\rightarrow\psi)$

$\psi\rightarrow(\forall x\phi)\Leftrightarrow\forall x(\psi\rightarrow\phi)$

---

$(\forall x\phi)\land\psi\Leftrightarrow\forall x(\phi\land\psi)$

$(\exists x\phi)\lor\psi\Leftrightarrow\exists x(\phi\lor\psi)$

$(\forall x\phi)\rightarrow\psi\Leftrightarrow\exists x(\phi\rightarrow\psi)$

$\psi\rightarrow(\exists x\phi)\Leftrightarrow\exists x(\psi\rightarrow\phi)$

---

I notice that all the equivalences are under the condition that $x$ does not appear as a free variable of $\psi$ , but the last four equivalences need an additional condition that $\exists x\top$.

So my question is what does $\exists x\top$ mean (I couldn't understand the note "meaning that at least one individual exists" in Wikipedia)? If possible, please tell me why the last four equivalences need the additional condition while the previous four don't need.

Answer 1

Since $\top$ always holds, the condition $\exists x \top$ just states that the ambiant structure is not empty. You can safely replace it with $\exists x \ x = x$.

The fact that the structure is not empty is relevant because in an empty structure, any statement of the form $\forall x \, \varphi (x)$ is (vacuously) true.

eg. for the equivalence $(\forall x\phi)\land\psi\Leftrightarrow\forall x(\phi\land\psi)$ you run into problem if you set $\psi := \bot$ since in the empty structure the right hand side holds while the left hand side does not.

Answer 2

This condition is to avoid empty models, but you should look at the question What's the deal with empty models in first order logic for a more detailed discussion.

Answer 3

There are two commonly-used semantics for first-order logic. I'll avoid calling either of them the standard semantics.

The traditional semantics prohibits empty domains.

The modern semantics permits empty domains.

If you're using the traditional semantics, you get $\exists x \mathop. \top$ for free.

If you're using the modern semantics, you can prove these facts for yourself by characterizing truth in the empty model.

Lemma 101: If $M$ is empty and $\varphi$ is headed by a quantifier, then $M \models \varphi$ if and only if $\text{FV}(\varphi)$ is nonempty or $\varphi$ is headed by $\forall$.

$M \models \varphi$ is defined to hold if and only if $M, v \models \varphi$ holds for all variable mappings $v$.

If $\varphi$ has free variables, then $M \models \varphi$ is vacuously true.

Suppose $\varphi$ is closed.

If $\varphi$ is of the form $\forall x \mathop. \psi(x)$, then $M \models \varphi$ holds if and only if $M \models \psi(x)$ holds. Since $\psi(x)$ contains free variables, we are done.

If $\varphi$ is of the form $\exists x \mathop. \psi(x)$, then $M \models \varphi$ holds if and only if there exists a $w$ in $M$ such that $M \models \varphi(w)$. There doesn't, so we're done.

This completes the proof of Lemma 101.

Let's look at the rule $(\forall x \mathop. \varphi) \land \psi \iff \forall x \mathop. \varphi \land \psi$

Suppose $\varphi =\!= \psi =\!= \bot $.

The value on the left $(\forall x \mathop. \bot) \land \bot$ is false.

The value on the right $\forall x \mathop. \bot \land \bot$, however, is true.