Does $\phi\vDash\bot$ imply that $\vDash\phi\to\bot$ if $\phi$ is a formula that has free variables? 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]]]$
 A: 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.
