Доклад Михаила Рыбакова на семинаре «Нестандартные логики» в Институте математики им. С.Л.Соболева СО РАН
19 сентября Михаил Рыбаков выступил с докладом «Неразрешимость QLC с двумя переменными» на семинаре «Нестандартные логики» в Институте математики им. С.Л.Соболева СО РАН в г. Новосибирске.
Аннотация.
Логика QLC получается из интуиционистской предикатной логики QInt добавлением аксиомы линейности. Семантически QLC характеризуется классом линейных шкал Крипке. Её модальный напарник -- логика QS4.3; она получается из QS4 аналогичным образом. Логика QLC содержит в себе логику QKC (логику слабого закона исключённого третьего), и в этом смысле она очень близка к классической логике предикатов QCl. Известно, что QCl неразрешима в языке с тремя переменными, но разрешима в языке с двумя. При этом и QInt, и QKC, и QS4.3 в языке с двумя переменными неразрешимы (даже при одной-двух унарных предикатных буквах). Техники, используемые в соответствующих доказательствах для фрагментов с двумя переменными, неприменимы к QLC -- ни «классическая» с разрешимостью, ни «неклассическая» с неразрешимостью, и вопрос о разрешимости фрагмента QLC с двумя переменными долгое время оставался открытым. Оказалось, имеется довольно несложная конструкция, позволяющая закодировать средствами QLC неразрешимую проблему типа «домино», при это достаточно использовать две переменные и лишь позитивные формулы. В докладе предполагается показать детали этой конструкции и извлечь из неё следствия, касающиеся как QLC, так и некоторого бесконечного класса расширений QLC -- во всех случаях будет получена неразрешимость, причём где-то Сигма-0-1-полнота, а где-то дополнительно и Пи-0-1-полнота.