 The second theorem refers to Craig interpolation. Several notions of interpolation are applicable to arbitrary logics. We consider only one of them. A logic \(\bL\) has the Craig interpolation property for the consequence relation if whenever \(\Gamma \vdash_{\bL } \phi\) and the set of variables of \(\phi\) has nonempty intersection with the set of variables of formulas in \(\Gamma\),  there is a finite set of formulas \(\Gamma '\) whose set of variables is included in the set of variables shared by \(\phi\) and the formulas in \(\Gamma\) such that \(\Gamma \vdash_{\bL } \Gamma '\) and \(\Gamma ' \vdash_{\bL } \phi\).