CRAIG'S THEOREM IN SUPERINTUITIONISTIC LOGICS AND AMALGAMABLE VARIETIES OF PSEUDOBOOLEAN ALGEBRAS
D.M. Gabbay, L. Maksimova · Oxford University Press eBooks · 2005
This chapter contains a full description of superintuitionistic logics with Craig's interpolation property CIP. It turns out that in the continuum of intermediate logics, only seven have Craig's interpolation. All of them are finitely axiomatizable and have the finite model property. For the proof, the algebraic semantics via varieties of Heyting algebras is used, and the equivalence of CIP in a logic L to amalgamability of the corresponding variety V(L) is stated. It is also proved that the interpolation problem over the intuitionistic logic Int is decidable: for any finite set Ax of axiom schemes to determine, whether the calculus Int+Ax has CIP; also the amalgamation problem is base-decidable for varieties of Heyting algebras.