Does $\phi\vDash\bot$ imply that $\vDash\phi\to\bot$ if $\phi$ is a formula that has free variables?

Question

This question is a sequel of this one where I asked the same thing with $\vDash$ replaced by $\vdash$.

Inspired by comments received on that question I switched from syntax to semantics.

---

Let $\mathcal{L}$ be a first order language.

Let $\phi$ denote a $\mathcal L$-formula that has at least one free variables.

Purely for convenience let us only look at the case where it has exactly one free variable $x$.

If my understanding is okay then:

• $\phi\vDash\bot$ iff every $\mathcal L$-structure $\mathfrak{A}$ has some element $a$ in its domain such that $\phi\left[a\right]$ is false in $\mathfrak{A}$. This because only in that situation no $\mathcal L$-structure $\mathfrak A$ exists that satisfies $\mathfrak A\vDash\phi$.

• $\vDash\phi\to\bot$ iff for every $\mathcal L$-structure $\mathfrak{A}$ and every element $a$ in its domain statement $\phi\left[a\right]$ is false in $\mathfrak{A}$. This because only in that situation $\mathfrak A\vDash\phi\to\bot$ for every $\mathcal L$-structure $\mathfrak A$.

Unfortunately it is not clear that $\phi\vDash\bot$ implies that $\vDash\phi\to\bot$ and I even wonder whether that's true.

Could you set straight wrong understandings or take away a blind spot (if there is any) please?

Thank you in advance.

---

Addendum to make clear where my understanding of $\phi\vDash\bot$ comes from.

• $\mathfrak A\vDash\phi\iff\forall a\in\mathsf{dom}\mathfrak A[\mathfrak A\vDash\phi[a]]$ (1.7.9 Leary)
• $\phi\vDash\psi\iff\forall\mathfrak A[\mathfrak A\vDash\phi\implies\mathfrak A\vDash\psi]$ (1.9.1 Leary)

Taking $\bot$ for $\psi$ in the last bullet we get:

$\phi\vDash\bot\iff\forall\mathfrak A[\mathfrak A\nvDash\phi]$

Then applying the first bullet we arrive at:

$\phi\vDash\bot\iff\forall\mathfrak A[\exists a\in\mathsf{dom}\mathfrak A[\mathfrak A\nvDash\phi[a]]]$

Answer 1

We do indeed have $$\phi\models\perp\quad\iff\quad\models\phi\rightarrow\perp.$$

Your understanding of $\phi\models\perp$ is incorrect: we have $\phi\models\perp$ iff for every structure $\mathcal{M}$, every variable assignment which makes $\phi$ true makes $\perp$ true. Since no assignment can make $\perp$ true, this means that there is no structure $\mathcal{M}$ and variable assignment making $\phi$ true - or in other words, no structure has any tuple satisfying $\phi$.

And this clearly matches up with $\models\phi\rightarrow\perp$ (your analysis of this is correct).

---

EDIT: Specifically, the issue is that your definition of $\phi\models\psi$ in the variables-allowed context is incorrect: the "quantification over valuations" has to happen outside the $\models$-part on the right hand side.

The right definition is $$\forall \mathfrak{A}, a\in\mathfrak{A}(\mathfrak{A}\models\phi[a]\implies\mathfrak{A}\models\psi[a]).$$ On the other hand, the relation you've defined - which I'll call "$\models_?$" for clarity - is equivalent to the following: $$\forall\mathfrak{A}[\forall a\in\mathfrak{A}(\mathfrak{A}\models\phi[a])\implies \forall a\in\mathfrak{A}(\mathfrak{A}\models\psi[a])].$$ To see the difference between these, consider the following formula in the language consisting of a single unary relation symbol $U$:

$\phi(x):\quad$ If $U$ describes a nonempty proper subset of the domain, then $U(x)$.

You can check that we have $\phi(x)\models_?\phi(y)$, which clearly should not hold.

And this accounts for the apparent discrepancy in the OP. Using the right definition, we have $\phi\models\perp$ iff $$\forall \mathfrak{A},a\in\mathfrak{A}(\mathfrak{A}\models\phi[a]\implies \mathfrak{A}\models\perp)$$ iff $$\forall \mathfrak{A}\color{red}{\forall} a\in\mathfrak{A}(\neg\mathfrak{A}\models\phi[a])$$ as desired.