Погружение интуиционистской и близких логик в их фрагменты от одной-двух переменных

Известно, что интуиционистская пропозициональная логика Int PSPACE-полна, причём PSPACE-полным является даже её импликативный фрагмент (R.Statman, 1979). Чуть ранее А.В.Кузнецов высказывал предположение, что Int полиномиально финитно аппроксимируема шкалами Крипке (и, как следствие, полиномиально погружается в классическую логику Cl). Это оказалось не так, что следует как из доказательства PSPACE-трудности Int, так и из результатов М.В.Захарьящева о сложности аппроксимации Int шкалами Крипке, полученных примерно в то же время. Тем не менее, фрагмент Int от одной переменной полиномиально финитно аппроксимируем и полиномиально разрешим (благодаря т.н. лестнице Ригера–Нишимуры). А.В.Чагров высказывал гипотезу о том, что полиномиально разрешимым будет любой фрагмент Int от конечного множества переменных (заметим, что для Cl это именно так и есть). В монографии [A.Chagrov, M.Zakharyaschev. Modal Logic. 1997] сформулирована соответствующая проблема (Problem 18.4), где вопросы о полиномиальной финитной аппроксимируемости и полиномиальной разрешимости ставятся для фрагмента Int от двух переменных и фрагментов S4, Grz и других стандартных модальных логик от одной переменной. На момент публикации этой монографии сложность фрагментов от одной переменной логик K, T, S4 была установлена (E.Spaan, 1993; J.Halpern, 1995), а в отношении Int долгое время ответа не было. Ответ для Int был получен докладчиком в 2004 году. В доказательстве возникла конструкция, позволившая обосновать PSPACE-трудность фрагментов от двух переменных всех логик между Int и логикой слабого закона исключённого третьего. Много позже эта конструкция была использована в решении алгоритмических вопросов для суперинтуиционистских предикатных логик, а недавно – для модальных интуиционистских логик, таких как MIPC (известна как IK – интуиционистская K), FS (известна как IS5) и других. Некоторые из полученных результатов опубликованы в совместных работах с Д.П.Шкатовым, в частности, касающиеся модальных интуиционистских логик.
В докладе предполагается (а) представить и обсудить используемую в доказательствах конструкцию, позволяющую полиномиально погрузить всю логику в её фрагмент от одной-двух переменных, (б) представить недавно полученные совместно с Д.П.Шкатовым результаты, а также (в) рассказать о некоторых следствиях, в т.ч. полученных совместно с А.А.Оноприенко (касаются логики HC, 2024г.) и М.И.Щербаковым (касаются логики GL.2, 2025г.).