Strict order on propositions and interpolation We can define a strict order on the set of propositions in countably many propositional letters in the following way: $$\varphi\sqsubset\psi \iff (\models \varphi\rightarrow\psi)\,  \land (\not\models \psi\rightarrow\varphi).$$
What I want to show is that if $\varphi\sqsubset\psi$, then there is some $\sigma$ such that $\varphi\sqsubset \sigma \sqsubset\psi$.
This is what I've done:


*

*Case 1: $\varphi \sim \perp$. In this case we can take a propositional letter $P$ not ocurring in $\varphi \land \psi$, and we have $\varphi\sqsubset (\psi\land P) \sqsubset \psi$.

*Case 2: $\varphi \not \sim \perp$. This time we can suppose that the propositional letters ocurring in $\varphi$ are over $P_1,\ldots,P_n$ and $\varphi$ depends on $P_n$.$^*$ Then it's easy to see that $\varphi\sqsubset \varphi(P_n/Q\land \neg Q)\lor \varphi(P_n/Q\lor \neg Q)$ for every propositional letter $Q$. I think that a proposition of this kind should be the «interpolant» in this case (as usual), but I can't prove it. Any suggestions?



$^*$$\varphi$ would be independent of $P_n$ if for every two valuations $v,w$ that may only differ in $P_n$, $\overline{v}(\varphi)=\overline{w}(\varphi).$
 A: The 'interpolant' you are looking for is $\varphi \lor (\psi \land Q)$ (with Q not occurring in either $\varphi$ or $\psi$ of course)
No need to separate the edge cases where $\varphi \Leftrightarrow \bot$ or $\psi \Leftrightarrow \top$; this interpolant always works.
To prove this in a rigorous manner, first some definitions:
Def.1 For any valuation $v$ that sets statements to $True$ or $False$: $v \models \varphi$ iff $v(\varphi) = True$
Def.2 For any two sentences $\varphi$ and $\psi$: $\varphi \models \psi$ iff for all valuations $v$: if $v \models \varphi$ then $v \models \psi$
Def.3 For any two sentences $\varphi$ and $\psi$: $\varphi\sqsubset\psi$ iff $\varphi \models \psi$ and $\psi \not \models \varphi$
(This last definition is equivalent to yours of course, but a little easier to work with I think)
OK, here's the proof:
Suppose $\varphi\sqsubset\psi$.
That means $\varphi \models \psi$ but $\psi \not \models \varphi$
Consider an atomic statement $A$ that does not occur in either $\varphi$ or $\psi$.
We will now show that $\varphi \sqsubset \varphi \lor (\psi \land A)\sqsubset \psi$.
To show $\varphi \sqsubset \varphi \lor (\psi \land A)$, we have to show $\varphi \models \varphi \lor (\psi \land A)$ and $\varphi \lor (\psi \land A) \not \models \varphi$
$\varphi \models \varphi \lor (\psi \land A)$ is trivial
To show that $\varphi \lor (\psi \land A) \not \models \varphi$: we know that $\psi \not \models \varphi$, so there exists a valuation $v$ such that $v \models \psi$ and $v \not \models \varphi$. Since $A$ does not occur in $\varphi$ or $\psi$, we can extend the valuation $v$ to $v'$ such that $v' \models \psi$ and $v' \models A$ and $v' \not \models \varphi$. Thus, $v' \models \psi \land A$, and thus $v' \models \varphi \lor (\psi \land A)$, and $v' \not \models \varphi$. Hence, $\varphi \lor (\psi \land A) \not \models \varphi$.
To show $\varphi \lor (\psi \land A)\sqsubset \psi$, we have to show $\varphi \lor (\psi \land A)\models  \psi$ and $\psi \not \models \varphi \lor (\psi \land A)$
To show $\varphi \lor (\psi \land A)\sqsubset \psi$, take any valuation $v$ such that $v \models \varphi \lor (\psi \land A)$. This means that either $v \models \varphi$ or $v \models \psi \land A$. If $v \models \varphi$, then given that $\varphi \models \psi$, we get $v \models \psi$, and if $v \models \psi \land A$, then of course $v \models \psi$ as well, so definitely $v \models \psi$.
To show that $\psi \not \models \varphi \lor (\psi \land A)$: again, we know that $\psi \not \models \varphi$, so there exists a valuation $v$ such that $v \models \psi$ and $v \not \models \varphi$. Since $A$ does not occur in $\varphi$ or $\psi$, we can extend the valuation $v$ to $v'$ such that $v' \models \psi$, $v' \models \varphi$, and $v' \not \models A$. By $v' \not \models A$, we get $v' \not \models \psi \land A$, and since $v' \not \models \varphi$ we thus get $v' \not \models \varphi \lor (\psi \land A)$. Hence, $\psi \not \models \varphi \lor (\psi \land A)$.
QED
