Propositional Interpolation Theorem In Fundamentals of Mathematical Logic by Hinman, page 40, there is the following exercise, rewritten in my own notation:

Let $S$ be the set of all propositions. For $\phi \in S$, let $P_\phi$ be the set of all atomic propositions occurring in $\phi$.
Now suppose that $\phi, \psi \in S$ are such that:

*

*$\psi$ is a tautological consequence of $\phi$

*Neither $\neg\phi$ nor $\psi$ is a tautology (so that $\psi$ is a tautological consequence of $\phi$ does not hold for trivial reasons)

Show there exists $\gamma \in S$ such that:

*

*$P_\gamma \subseteq P_\phi \cap P_\psi$

*$\gamma$ is a tautological consequence of $\phi$

*$\psi$ is a tautological consequence of $\gamma$
$\textbf{Hint:}$ Show first that $P_\phi \cap P_\psi \neq \emptyset$.

Now it's easy to see that if $P_\phi \cap P_\psi = \emptyset$, it would contradict the hypothesis given.
However, having shown that the intersection is nonempty, I'm unsure of how to proceed. The book says that only techniques of the section are required.
What was covered in the section were:

*

*variable substitution

*tautological equivalence

*conjunctive and disjunctive normal forms (and their strict versions)

I have a hunch that the normal forms may be necessary, but I'm unsure as to how to use them in this case.
Minimal hints would be greatly appreciated.
 A: I shall sketch a proof as follows:
As given, neither $\neg\phi$ nor $\psi$ is a tautology. Hence, neither $\phi$ nor $\psi$ is a tautology and each one is tautologically equivalent to a proposition in strictly conjunctive normal form by the corollary 1.3.11.
Suppose  $\phi$ and $\psi$ have the identical sets of atomic propositions, $P_{at}(\phi) = P_{at}(\psi)$.
Then, $$\phi\models\phi$$ and $$\phi\models\psi$$
Thus, $\phi$ is trivially the interpolant proposition $\gamma$.
We can take the foregoing case as the basis clause and carry out an induction on the number of atomic propositions that occur in $\phi$ but not in $\psi$. Because, suppose that $\phi$ and $\psi$ differ by one atomic proposition $p_{0}$: If $p_{0}\in P_{at}(\psi)$, then the given tautological consequence would not hold, for we could assign $\bot$ to $p_{0}$ if $\top$ makes the tautological consequence hold, and vice versa if otherwise. Therefore,  in case that $P_{at}(\phi)$ and $P_{at}(\psi)$ differs, $P_{at}(\phi)\cap P_{at}(\psi)\neq\emptyset$ and $P_{at}(\psi)\subset P_{at}(\phi)$.
As the inductive hypothesis, we assume that we have obtained an interpolant formula $\gamma$ for all cases of the number of differing atomic propositions up to $n$, and construct an interpolant proposition $\gamma$ for the case that $\phi$ and $\psi$ differ by $n+1$ atomic propositions.
We shall call on a weakening theorem of propositional calculus:
$$p\rightarrow (p\vee q)$$
This theorem may be interpreted as stating that $p$ is a stronger proposition than $p\vee q$. If we assign $\top$ to $q$, we get $p\rightarrow\top$. If we assign  $\bot$ to $q$, we get $p\rightarrow p$.
Similarly, we shall compose a proposition $\phi'$ from $\phi$. We shall uniformly substitute $\top$ and $\bot$ for an arbitrary atomic proposition, except for the condition that $p_{0}\in P_{at}(\phi)$ and $p_{0}\notin P_{at}(\psi)$, as the disjuncts of $\phi'$:
$$\phi'\leftrightarrow\phi(\top/p_{0})\vee\phi(\top/p_{0})$$
Notice that $\phi'$ thus obtained and $\psi$ differ by $n$ atomic propositions, so we are allowed to employ the inductive hypothesis.
We see that $$\phi\rightarrow\phi'$$ and also $$\phi'\rightarrow\psi$$
By the hypothesis, there is an interpolant proposition $\gamma$ between $\phi'$ and $\psi$:
$$\phi'\models\gamma$$ and $$\gamma\models\psi$$
Since $$\phi\models\gamma$$ the existence of a proposition with the given conditions is shown.
