Notice: I have cross-posted this question into MathOverflow, here https://mathoverflow.net/questions/383999.
I am looking for a sketch of, or a reference to, a proof which I can't seem to find in the literature.
Craig's interpolation theorem (also known as Craig's interpolation lemma, or Craig's interpolation property) states, for propositional logic, that if $\varphi\vDash\psi$, then there exists a formula $\rho$, whose variables are variables of, simultaneously, $\varphi$ and $\psi$, such that $\varphi\vDash\rho$ and $\rho\vDash\psi$.
All well and good so far, but I am also aware that one can derive (generalizations of) Craig's interpolation theorem from the fact that the variety of algebras algebraizing a logic is ammalgamated: that is, for any algebras $A$, $B_{1}$ and $B_{2}$ in this variety, and monomorphisms $\alpha_{1}:A\rightarrow B_{1}$ and $\alpha_{2}:A\rightarrow B_{2}$, there exists a fourth algebra $C$, also on the variety, and monomorphisms $\beta_{1}:B_{1}\rightarrow C$ and $\beta_{2}:B_{2}\rightarrow C$ commuting the diagram $\require{AMScd}$ \begin{CD} A @>\alpha_{1}>> B_{1}\\ @V \alpha_{2} V V @VV \beta_{1} V\\ B_{2} @>>\beta_{2}> C \end{CD}
One example of this being done is in "Interpolation and Definability: Modal and Intuitionistic Logics" by Gabbay and Maksimova. In this book, however, they first apply this methodology to superintuitionistic logics, and never to simpler systems. In all references I found, actually, the proof by amalgamation is done to non-classical logics.
What I am looking for is the proof of Craig's interpolation theorem through the use of amalgamation for propositional logic, so I can have a better understanding (or at least I hope to have) of this style of proof for more complicated logics. It can be a sketch, a reference, or preferably both!