Uniform Lyndon interpolation property in propositional modal logics (Q781510)

The interpolation property CIP (Craig interpolation property) shown by \textit{W. Craig} [J. Symb. Log. 22, 269--285 (1957; Zbl 0079.24502)] originally for the classical first order predicate logic was strengthened by \textit{R. C. Lyndon} [Pac. J. Math. 9, 129--142 (1959; Zbl 0093.01002)] to LIP (Lyndon interpolation property) with respect to the polarity of occurrence of variable in the interpolant. Afterwords, \textit{A. M. Pitts} [J. Symb. Log. 57, No. 1, 33--52 (1992; Zbl 0763.03009)] proved for the propositional intuitionistic logic another strengthened version UIP (uniform interpolation property) enjoying certain uniformity of interpolant with respect to a given formula and finite set of propositional variables. These properties do not necessarily hold in the case of modal logics and are studied by Maksimova, Fitting, and many others particularly for propositional normal modal logics with other weaker versions as well. For example, among many other interesting observations, some extensions of S5 enjoy CIP but not LIP (by \textit{L. L. Maksimova} [in: Matematicheskaya logika i teoriya algoritmov. Sbornik rabot. Novosibirsk: Izdatel'stvo ``Nauka'' Sibirskoe Otdelenie. 45--55 (1982; Zbl 0543.03011)]), and S4 does not enjoy UIP (by \textit{S. Ghilardi} and \textit{M. Zawadowski} [Stud. Log. 55, No. 2, 259--271 (1995; Zbl 0831.03008)], while LIP of S4 is well-known). In this paper, the author introduces a new stronger version called ULIP (uniform Lyndon interpolation property) so as to cover the both LIP and UIP and shows some basic properties on ULIP in relation to LIP and UIP, which then give rise to the (affirmative or negative) results on ULIP for several cases from the known observations. Main arguments, however, are the direct proofs of ULIP for K, KB, GL, and Grz satisfying certain upper bound on the depth of modality (or, modal degree, equivalently) of uniform interpolant, which are carried out semantically by modifying the method of layered bisimulation between Kripke models applied by \textit{A. Visser} [Lect. Notes Log. 6, 139--164 (1996; Zbl 0854.03026)] in proving UIP for GL and Grz with the similar upper bound, where the upper bound given in this paper is lower than that given by Visser [loc. cit.] (with respect to UIP of GL and Grz except for some trivial cases). All the argument is developed with a propositional modal language including the falsehood. But, under a formalization of language without any propositional constant, which is also quite natural, some modifications would be necessary.