Unification in pretabular extensions of S4 (Q2239389)

The paper is dedicated to the study of pretabular extensions of modal logic \(\mathrm{S4}\) described in [\textit{L. L. Maksimova}, Algebra Logic 14, 16--33 (1976; Zbl 0319.02019); translation from Algebra Logika 14, 28--55 (1975)]: \[ \begin{array}{l} \mathrm{PM1 := S}4.3 + \mathcal{G}rz,\\ \mathrm{PM2} := \mathcal{G}rz + \sigma_2,\\ \mathrm{PM3} := \mathcal{G}rz + [\Box r \lor \Box(\Box r \to \sigma_2)] + (\Box\Diamond p \Leftrightarrow \Diamond\Box p),\\ \mathrm{PM4 := S}4 +[\Box p \lor \Box (\Box p \to \Box q \lor \Box \Diamond \neg q)] + (\Box \Diamond p \leftrightarrow \Diamond\Box p),\\ \mathrm{PM5 := S}5, \end{array} \] where \(\mathcal{G}rz := [\Box(\Box(p \to \Box p) \to p) \to p]\)\\ and \(\sigma_2 := [\Box p \lor \Box (\Box p \to \Box q \lor \Box \Diamond \neg q)]\). It is proven that the logics \(\mathrm{PM2}\) and \(\mathrm{PM3}\) have a finitary unification type, while the logics \(\mathrm{PM1, PM4}\) and \(\mathrm{PM5}\) have a unitary unification type, and any unifiable in \(\mathrm{PM1, PM4}\) or \(\mathrm{PM5}\) formula is projective.