An institution-independent proof of Craig Interpolation Property 

We formulate a general institution-independent (i.e. independent of the details of the actual logic or institution) version of the Craig Interpolation Theorem and prove it in dependence of Birkhoff-style axiomatizability properties of the actual logic.

We formalise Birkhoff-style axiomatizability within the general abstract model theoretic framework of institution theory by the novel concept of Birkhoff institution.

Our proof destills a set of conditions behind the Craig Interpolation Property, which are easily satisfied in the applications. This together with the generality of our approach leads to a wide range of applications for our result, including conventional and non-conventional logics (many of them from algebraic specification theory), such as general algebra, classical model theory, partial algebra, rewriting logic, membership algebra, etc. all of them in various versions and with various types of sentences (including infinitary ones).

In dependence of axiomatizability properties many other applications are expected for various institutions or logics.

---