Interpolation property for extensions of intuitionistic provability logic (Q922543)

The provability-intuitionistic logic \(I^{\Delta}\) [see \textit{A. V. Kuznetsov} and \textit{A. Yu. Muravitskij}, Stud. Logica 45, 77-99 (1986; Zbl 0623.03027)] can be considered as a model extension of the Heyting propositional calculus by the following axioms: \(p\to \Delta p\), (\(\Delta\) \(p\to p)\to p\) and ((p\(\to q)\to p)\to (\Delta q\to p)\). The author proves that there exists a continuum of extensions of \(I^{\Delta}\) having the interpolation property, and gives an example of an extension of \(I^{\Delta}\) which does not have the interpolation property.