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...
$\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$.