# What does the negated double turnstile ($\not\models$) mean?

I understand that the expression $$\models \phi \rightarrow \psi$$ means that $$\phi \rightarrow \psi$$ is a tautology. But what does the expression $$\not\models \phi \rightarrow \psi$$ mean? Does it mean that $$\phi \rightarrow \psi$$ is not a tautology or that it is a contradiction?

To be more specific, I have a school assignment where we define a relation $$\prec$$ on the set of all propositional wffs, such that $$\phi \prec \psi$$ iff $$\models \phi \rightarrow \psi$$ and $$\not\models \psi \rightarrow \phi$$. I am trying to understand what the nature of this relation is, in order to prove the following:

If $$\phi \prec \psi$$ then there exists a wff $$\chi$$ such that $$\phi \prec \chi \prec \psi$$.

EDIT: If I understand correctly, this is a variation of Craig interpolation lemma, but I can not figure it out...

• The same thing that anything with a negation sign mean. Not the definition of the thing which is negated. In this case, take the definition of $\models$ and put a "not" before it. – Asaf Karagila Mar 12 at 11:41
• In comparison, define an order on $\Bbb N$ given by $n\prec m$ if $n\leq m$ and $m\nleq n$. What can you understand from this? – Asaf Karagila Mar 12 at 11:42

$$\not \vDash \phi$$ means that $$\phi$$ is not a tautology. Look at the definition of $$\vDash$$:

$$\Gamma \vDash \phi \text{ iff for all assignments } v \text{: If } [[\psi]]_v = true \text{ for each } \psi \in \Gamma, \text{ then } [[\phi]]_v = true.$$

i.e. each assignment that makes all of the premises true must also make the consequent true.

If $$\Gamma$$ is empty, $$\phi$$ holds without any assumptions so $$\phi$$ is a tautology. So the "if" part is dropped, and we have:

$$\vDash \phi \text{ iff for all assignments } v: [[\phi]]_v = true$$

That is, we have a universal quantification. $$\not \vDash$$ negates this universal quantification:

$$\text{ Not for all assignments } v: [[\phi]]_v = true$$

which is the same as saying

$$\text{ There is an an assignment } v: [[\phi]]_v = false$$

So $$\not \vDash \phi$$ means that $$\phi$$ is not a tautology, that there are assignments under which it is false.

That $$\phi$$ is a contradiction would be a stronger claim:

$$\text{For all assignments } v: [[\phi]]_v = false$$

or

$$\text{ There is an no assignment } v: [[\phi]]_v = true$$

This is a stronger claim than saying that not all assignments make $$\phi$$ true, and can not be directly expressed with a symbol.
In classical logic, the statement "$$\phi$$ is a contradiction" can be modelled by saying that its negation is tautological:

$$\vDash \neg \phi$$

which holds iff

$$\text{ for all assignments } v: [[\neg \phi]]_v = true$$

which, by definition of $$\neg$$, holds iff

$$\text{ for all assignments } v: [[\phi]]_v = false$$

W.r.t. to the relation $$\prec$$, the definition $$\phi \prec \psi \text{ iff } \vDash \phi \to \psi \text{ and } \not \vDash \psi \to \phi$$ means that $$\phi \to \psi$$ is tautological, so all assignments that make $$\phi$$ true also make $$\psi$$ true (by definition of $$\to$$), but $$\psi \to \phi$$ isn't, so there are assignments where $$\psi \to \phi$$ is false, which is the case only if $$\psi$$ is true and $$\phi$$ is false.

This gives you a hint on how to find $$\chi$$: $$\chi$$ is a formula such that
- under all assignments under which $$\phi$$ is true, $$\chi$$ is true ($$\vDash \phi \to \chi$$),
- there is an assignment under which $$\chi$$ is true, but $$\phi$$ is false ($$\not \vDash \chi \to \phi$$),
- under all assignments under which $$\chi$$ is true, $$\psi$$ is true ($$\vDash \chi \to \phi$$),
- there is an assignment under which $$\chi$$ is true, but $$\phi$$ is false ($$\not \vDash \psi \to \chi$$).

You need to show that this scenario can always be constructed given $$\phi \prec \psi$$.

You are right in that this is a variation of Craig's interpolation theorem, which states:

$$\text{ If } \vDash \phi \to \psi \text { then there is a formula } \chi \text{ (the interpolant) such that } \vDash \phi \to \chi \text{ and } \vDash \chi \to \psi\\ \text{ with } atoms(\chi) \subseteq atoms(\phi) \cap atoms(\psi).$$

The proof of Craig's interpolation theorem proceeds by induction on the cardinality of the set $$atoms(\phi) − atoms(ψ)$$, i.e. on the number of propositional variables that are in $$\phi$$ but not in $$\psi$$. You shoould be able to transform this proof into a proof of the "$$\prec$$ interpolation" by adapting the semantics of $$\to$$ to $$\prec$$ accordingly. So in each step of the proof you need to show not only that $$A \to B$$ holds, but also that $$B \to A$$ is non-tautological.

Intuitively, $$\prec$$ means "strictly implies": $$\phi$$ implies $$\psi$$, but the other direction does not hold in all situtions, so it is not biconditional, i.e. $$\phi \to \psi$$ and not $$\phi \leftrightarrow \psi$$.

$$\not \vDash \phi \to \psi$$ means that $$\phi \to \psi$$ is not a tautology.

More general, $$\Gamma \not \vDash \varphi$$ means that $$\varphi$$ is not a logical consequence of $$\Gamma$$

• Thanks a lot! But what does this have to do with the $\prec$ relation? Does it inform as about anything more that the fact that $\phi$ and $\psi$ can not be the same wff? – Zehanort Mar 12 at 1:56
• @Zehanort Well, that is for you to figure out ...but let me know if you need a hint – Bram28 Mar 12 at 1:59