Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach (Q1821770)

Craig's interpolation theorem for intuitionistic predicate logic was first proved by Schütte using syntactical methods. Other syntactical proofs were given by, among others, Prawitz and Maehara. Semantical proofs were given by Gabbay, Fitting and Ono. One more such proof is given here, along the lines of the Henkin-style proof of the completeness theorem. Using a generalized notion of inseparable pair of theories, the author clarifies the relationship between interpolation and (Robinson's) consistency. As a corollary, the author also gives a new proof of the interpolation property of the seven intermediate propositional logics listed in \textit{L. L. Maksimova}'s paper in Algebra Logika 16, 643-681 (1977; Zbl 0403.03047). Warning: in reference [14], H. Ono should be replaced by K. \((=\) Katuzi) Ono, H. Ono's father.