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