The question is pretty much in the title. We are asked to show

$$\models \varphi\rightarrow \forall x\varphi\quad\text{ if $x$ is not a free variable of $\varphi$}.$$

It seems to me that this is pretty obvious, because if $x$ is not free, then the quantifier doesn't change anything and $\varphi,\forall x\varphi$ are logically equivalent. So there isn't really anything left to show.

But what if $x$ is free in $\varphi$? I would have thought the following ($\mathfrak{M}$ is a structure, and $s$ a variable assignment): \begin{align*} \models\forall x\,\varphi \iff&\forall\mathfrak{M},s:\,\mathfrak{M},s\models\forall x\,\varphi\\ \iff&\forall\mathfrak{M},s\mathrm{~and~}\forall d\in\lvert \mathfrak{M}\rvert:\,\mathfrak{M},s\frac{d}{x}\models\varphi\\ \iff&\forall\mathfrak{M},\bar{s}:\,\mathfrak{M},\bar{s}\models\varphi\\ \iff&\models\varphi. \end{align*} For the equivalence of the 2nd and the 3rd line, I use the argument that $s$ is arbitrary, and we could choose another assignment $\bar{s}$ with $\bar{s}(x)=d=s\frac{d}{x}(x)$. We may do that for all $d$ in $\mathfrak{M}$'s domain.

Is my way of thinking terribly flawed here or is this correct?


Edit. To the downvoter:

Use your downvotes whenever you encounter an egregiously sloppy, no-effort-expended post, or an answer that is clearly and perhaps dangerously incorrect.

This does not apply here.


With the definition of $\vDash$ you seem to be working with, it is indeed the case that $\vDash \varphi$ if and only if $\vDash \forall x.\varphi$, whether or not $\varphi$ contains $x$ free.

However, that doesn't mean that $\vDash \varphi\to\forall x.\varphi$.

This does not necessarily have anything to do with quantifiers or even free variables. The underlying point is that the set of valid formulas is a less "nice" set than you appear to think it is. It is closed under logical consequence, but the $\vDash$ relation does not produce a truth assignment for all formulas that respect the truth tables of the connectives.

As a concrete example: We have $\not\vDash x=5$ as well as $\not\vDash x\ne 5$, but we do have $\vDash (x=5)\lor(x\ne 5)$, apparently contradicting the row in the truth table for $\lor$ saying that "false or false makes false".

  • $\begingroup$ My definition of $\models$ seems to coincide with the one in this Wikipedia article. What is your definition? Furthermore, we have shown in the lecture that $\varphi\models\psi\iff\models\varphi\rightarrow\psi$. And by my definition of the double turnstile, $\models\varphi\Rightarrow\models\psi$ is equivalent to $\varphi\models\psi$, i.e. $\models\varphi\rightarrow\psi$. I don't understand what's going on. $\endgroup$ – Jo Be Feb 20 '15 at 19:43
  • 1
    $\begingroup$ @JoBe: Check your definitions again. It is very unlikely that $(\vDash\varphi)\Rightarrow(\vDash\psi)$ is the same as $\varphi\vDash\psi$. The former is the same as $(\forall \mathfrak M.\mathfrak M\vDash\varphi)\Rightarrow(\forall \mathfrak M.\mathfrak M\vDash\psi)$; the latter is $\forall\mathfrak M.\bigl[(\mathfrak M\vDash \varphi)\Rightarrow(\mathfrak M\vDash \psi)\bigr]$. The differences in how $\mathfrak M$ is quantified over are significant! $\endgroup$ – Henning Makholm Feb 20 '15 at 20:07
  • $\begingroup$ Oh, of course. I see it now, thanks for pointing it out! But that doesn't invalidate my explanation for the original question, right? I mean the part where I say $\varphi$ and $\forall x.\varphi$ are logically equivalent (given that $x$ is not free in $\varphi$, of course). $\endgroup$ – Jo Be Feb 20 '15 at 20:42
  • $\begingroup$ @JoBe: It's right that $\varphi$ and $\forall x.\varphi$ are logically equivalent when $x$ is not free in $\varphi$, but I think the exercise is expecting you to argue for that (based on your definition of $\vDash$), rather than just assert it. I might be wrong, though, for example if you have already established this equivalence explicitly. $\endgroup$ – Henning Makholm Feb 20 '15 at 20:50

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.