Семинары ИМ СО РАН

Хорошо известно (и нетрудно показать), что модальная предикатная логика, определяемая элементарным классом шкал Крипке, является рекурсивно аксиоматизируемой (поскольку она погружается в классическую логику предикатов). Кроме того, известно много примеров полных по Крипке логик, но не полных относительно элементарных классов шкал, которые имеют высокую алгоритмическую сложность. Например, логики различных классов нётеровых шкал Пи-1-1-трудны, а логики различных классов конечных (по числу миров) шкал одновременно Пи-0-1-трудны и Сигма-0-1-трудны. Возникает естественный вопрос о контрпримерах: когда полная по Крипке логика, не определимая ни одним элементарным классом шкал Крипке, всё же рекурсивно аксиоматизируема. В докладе предполагается показать, как можно строить примеры таких логик. В начале 2000-х автором были построены такие примеры в классе логик, не замкнутых по правилу усиления (правилу Гёделя), причём при ограничениях на семантику: рассматривались классы только корневых шкал с выделенным корнем (публикаций не было, были только доклады на научных семинарах). Значительно позже такие примеры были найдены и в классе нормальных логик (расширениях логики QK, замкнутых в т.ч. по правилу усиления), при этом было снято и требование о том, чтобы шкалы были только корневыми. Результаты опубликованы в работах [1] и [2]. Все необходимые определения будут даны в докладе.

[1] M. Rybakov, D. Shkatov. A recursively enumerable Kripke complete first-order logic not complete with respect to a first-order definable class of frames. Advances in Modal Logic, 12, eds. Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe, and Thomas Studer, College Publications, 2018, 531–540.

[2] M. Rybakov, D. Shkatov. Recursive enumerability and elementary frame definability in predicate modal logic. Journal of Logic and Computation, 30:2, 2020, 549–560.