L. Maksimova, “Interpolation and implicit definability in extensions of the provability logic”, LLP, vol. 17, no. 1-2, pp. 129–142, Jun. 2008.