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]]]$


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.

  • $\begingroup$ I have added the reasonings that led me to this (mis)understanding. Would you be so kind to take a look at them, Noah? They are based on what I encountered in "Leary and Kristiansen". I am still puzzled. $\endgroup$ – drhab Aug 24 '20 at 19:05
  • $\begingroup$ @drhab See my edit (your definition of $\models$ for formulas has a quantifier-placement error). $\endgroup$ – Noah Schweber Aug 24 '20 at 19:24
  • $\begingroup$ Thank you very much. One of the coming days (now it is time to get some sleep) I will probably add a citation from "Leary and Kristiansen" in order to get things straight. I will let you know. I do understand the difference between $\vDash$ and $\vDash_{?}$ but am still a bit shaky. Good night. $\endgroup$ – drhab Aug 24 '20 at 19:48
  • $\begingroup$ In Leary it is stated that for applying the deduction theorem we must be dealing with a sentence. That seems redundant under your definition. Further a rule of interference is there: $(\{\psi\to\phi\},\psi\to\forall x\phi)$ under condition that $x$ is not free in $\psi$. The soundness of it can be proved with $\vDash_{?}$ but under your $\vDash$ the rule seems not to be sound. Also there is an exercise of the form: "prove that $\phi\vDash\psi$ but not $\vDash\phi\to\psi$. $\endgroup$ – drhab Aug 25 '20 at 8:37
  • $\begingroup$ What I said in my former comment about deduction theorem is a matter of syntax, so might not be relevant here. But the fact remains that your definition does not seem to match with the one practicized by Leary (nor Mendelsohn). $\endgroup$ – drhab Aug 25 '20 at 10:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.