# How to prove Craig's interpolation using amalgamation?

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!

• Do you know how to show that Boolean Algebras have the amalgamation property for embeddings (monomorphisms)? – Alex Kruckman Feb 4 at 23:16
• @AlexKruckman Now that you mention, I actually don't think I do... I suppose that, given embeddings $\alpha_{i}:A\rightarrow B_{i}$, one takes the Boolean algebra $B_{1}\ast B_{2}$ freely generated by $B_{1}\times B_{2}$ and embeddings $\beta_{i}:B_{i}\rightarrow B_{1}\ast B_{2}$ taking, e.g., $b\in B_{1}$ to $(b, ?)$; but I am not certain of the form of $?$ (except that it should equal $\alpha_{2}\circ\alpha_{1}^{-1}$ on $\alpha_{1}(A)$)... – GVT Feb 5 at 13:39
• @AlexKruckman Ok, I found the precise construction on the original work of Dwinger and Yaqub: I have not yet read the article fully, but from what I understood one takes the BA $B_{1}\ast B_{2}$ freely generated by $B_{1}\times B_{2}$, quotiented by the ideal $I$ generated by the symmetric differences $$(\alpha_{1}(a), 1)\Delta(1,\alpha_{2}(a)),$$ for all $a\in A$. Then, $\beta_{1}(b)=(b, 1)$ and $\beta_{2}(b')=(1, b')$, and for any $a\in A$, $\beta_{1}\circ\alpha_{1}(a)=(\alpha_{1}(a), 1)$ and $\beta_{2}\circ\alpha_{2}(a)=(1, \alpha_{2}(a))$, which are equal on $B_{1}\ast B_{2}/I$. – GVT Feb 8 at 18:10
• The thing is that a direct proof of Craig interpolation for classical propositional logic is completely trivial (if $\models\phi(\vec p,\vec q)\to\psi(\vec p,\vec r)$, then $\rho(\vec p)=\bigvee_{\vec a\in\{0,1\}^n}\phi(\vec p,\vec a)$ is an interpolant, where $n=|\vec q|$), thus there is no incentive to prove it using anything as sophisticated as amalgamation for Boolean algebras. This will make it difficult to find in the existing literature. But, frankly, I don’t understand your motivation. In the MO post, you explain that you want to apply this methodology to a propositional logic ... – Emil Jeřábek Feb 15 at 10:14
• ... that not only is non-classical, but is not even algebraizable. Surely you should first understand how it works for well-behaved (algebraizable) but nontrivial logics such as intuitionistic logic. Studying the rather degenerate case of classical logic will not help you much. – Emil Jeřábek Feb 15 at 10:17