Basic propositional calculus. II: Interpolation (Q5945567)

[For Part I see Math. Log. Q. 44, No. 3, 317-343 (1998; Zbl 0912.03005).] Basic propositional calculus BPC is a proper subsystem of intuitionistic propositional calculus IPC through a weakened modus ponens. Consequently the interpolation theorem permits a generalized form, and requires an original proof. If \(A\) is a formula over a language \(L\), and \(C_1\) and \(C_2\) are formulas over a language \(N\), such that \(A\&C_1\) entails \(C_2\), then there is a formula \(B\) over the intersection language of \(L\) and \(N\) such that both \(A\) entails \(B\) and \(B\&C_1\) entails \(C_2\). Additionally, if \(A\), \(C_1\), and \(C_2\) are conjunctions of implications, then \(B\) can be chosen to be a conjunction of implications.