5
$\begingroup$

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!

$\endgroup$
6
  • $\begingroup$ Do you know how to show that Boolean Algebras have the amalgamation property for embeddings (monomorphisms)? $\endgroup$ – Alex Kruckman Feb 4 at 23:16
  • $\begingroup$ @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)$)... $\endgroup$ – GVT Feb 5 at 13:39
  • $\begingroup$ @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$. $\endgroup$ – GVT Feb 8 at 18:10
  • $\begingroup$ 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 ... $\endgroup$ – Emil Jeřábek Feb 15 at 10:14
  • $\begingroup$ ... 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. $\endgroup$ – Emil Jeřábek Feb 15 at 10:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.