О финитной аппроксимируемости одного класса предтранзитивных логик

Модальная логика L называется предтранзитивной, если в ней выразим оператор, соответствующий рефлексивному транзитивному замыканию отношения достижимости в моделях Крипке. Данное условие равносильно тому, что для некоторого $n$ в L выводится формула
$$\Diamond^{n+1} p \to \bigvee_{k\leq n} \Diamond^k p.$$
Наиболее известными примерами предтранзитивных логик являются логики $K^m_n = K + (\Diamond^n p \to \Diamond^m p)$ при $n > m$. Финитная аппроксимируемость данных логик при $m = 1$ известна с начала 1970-х годов, при $m > 1$ вопрос остаётся открытым до сих пор.
Мы покажем, как, используя селективную фильтрацию канонической модели, усилить результат о финитной аппроксимируемости $K^1_n$, распространив его на логики вида $K + (\phi(p) \to \Diamond p)$, где $\phi(p)$ — строго позитивная формула с единственной переменной $p$, причём каждое вхождение $p$ в $\phi$ находится по крайней мере под двумя ромбами. Несмотря на то, что данный класс не содержит $K^m_n$ при $m > 1$, его исследование достаточно нетривиально. Например, уже для логики
$$ K + (\Diamond\Diamond(p \land \Diamond p) \to \Diamond p),$$
не существует однозначно определённого аналога транзитивного замыкания, что не позволяет использовать стандартные методы доказательства финитной аппроксимируемости логик $K^1_n$ для данного случая.