Топологические модальные логики прямой

Модальная логика изучает булевы формулы с одним или несколькими дополнительными операторами-модальностями. В зависимости от семантики, модальностям соответствуют разные операторы на структурах-моделях. Такой структурой может быть, например, топологическое пространство. Формулы, в некотором смысле соответствуют свойствам топологических пространств. В топологических пространствах чаще всего одной из модальностей соответствует оператор взятия внутренности. Но в силу бедности языка далеко не все свойства топологических пространств выразимы на языке модальной логике при данной семантике, но зато, часто множество истинных формул разрешимо и имеет хорошее описание в виде конечного списка аксиом (иногда бесконечного) и правил вывода. В докладе мы рассмотрим модальные логики, которые возникают, если в качестве топологического пространства взять действительную прямую. Это один из самых изученных объектов в математике. Мы сделаем обзор классических результатов Маккинси и Тарского 1944 года, которые доказали, что множеством всех формул истинных на действительной прямой, является известная логика S4 (определение будет дано в докладе), но базовый язык может выразить довольно мало свойств топологических пространств. Для увеличения выразительных свойств можно добавлять новые модальности и/или изменять семантику. Мы рассмотрим эти варианты и обсудим какие при этом получаются множества истинных формул. Мы покажем, что в некоторых случаях множество истинных формул оказывается не конечноаксиоматизируемым.