Notice: this is a cross-posting, I have asked essentially the same question on MSE (https://math.stackexchange.com/questions/4012960) but received no answers, and as this problem, although very basic, came up in my research, I think it may be reasonable to post it here as well. I use the opportunity to ask a lateral question which is probably more suited for MathOverflow anyway.
Question: it is not uncommon to prove Craig's interpolation theorem, or the related Lyndon's interpolation theorem or Robinson's joint consistency theorem, through amalgamation on the variety of algebras that algebraize the logic in question. One example of this being done is in "Interpolation and Definability: Modal and Intuitionistic Logics" by Gabbay and Maksimova, to superintuitionistic logics.
But I never found a more didactic approach to the subject, therefore my question: where such a methodology is applied to propositional logic? I assume that this would probably also be the first proof of interpolation results through amalgamation, although I may be wrong.
Lateral Question: my research problem is roughly as follows. I have a class of logics that, although not algebraizable (not even according to Blok and Pigozzi and many other more esoteric takes on algebraization), admits semantic characterizations which, with little effort, can be made into a category. This category is well-behaved, being, among other things, amalgamated: is there a known proof of interpolation for non-algebraizable logics through amalgamation?
