Об $S5$-$T$-$Y$ логиках

Изучается наименьшая $S5$-$T$-$Y$ логика $L_\infty$. Язык этой логики получается добавлением к языку $S5$ связок $T$ (‘завтра’) и $Y$ (‘вчера’). К аксиоматике $S5$ в логике $L_\infty$ добавлены аксиомы $T$-$Y$ – логики (см. [2]) и аксиомы:
$$\begin{align*} &\square A\to TA\land YA,\quad TA\lor YA\to\diamond A \\ &T\square A\leftrightarrow \square A,\quad Y\square A\leftrightarrow \square A \end{align*}$$
и правило подстановки. Доказывается, что точной шкалой Крипке для $L_\infty$ является счетное объединение шкал с порядковым типом $Z$ (множества целых чисел). Используется приведение формул к совершенной дизъюнктивной нормальной форме (СДНФ).