On completeness of dynamic topological logic

Классический результат о топологической семантике модальных логик, принадлежащий МакКинси и Тарскому (и часто называемый теоремой Тарского), состоит в полноте логики S4 по отношению к интерпретациям в пространстве $\mathbb R^n$ для любого $n$. В последнее время разные авторы рассматривали динамические топологические логики, которые интерпретируются в динамических пространствах (абстрактных динамических системах). Динамическое пространство – это топологическое пространство вместе с непрерывной функцией на нем. В работе Артёмова, Даворен и Нероде было дано определение бимодальной логики S4C и доказана ее полнота в классе всех динамических пространств. Различные полимодальные логики для динамических систем были рассмотрены Кремером, Минцем и Рубаковым. Ранее автором было показано, что аналог теоремы Тарского не выполняется для логики S4C; этот же результат был независимо от автора установлен П. Кремером и затем Й. ван Бентемом. В этой работе мы показываем, что определённое обобщение теоремы Тарского применимо и в динамическом случае. Мы доказываем, что для любой невыводимой (в S4C) формулы $\phi$ существует контр-модель в пространстве $\mathbb R^n$ при $n$ достаточно большом. Мы также даем верхнюю границу для размерности опровергающей модели. Открытым остается вопрос, является ли наша верхняя граница точной.